### Nuprl Lemma : quot_ring_car_subtype

`∀[r:CRng]. ∀[a:Ideal(r){i}].  ((∀x:|r|. SqStable(a x)) `` (∀[d:detach_fun(|r|;a)]. (|r| ⊆r Carrier(r/d))))`

Proof

Definitions occuring in Statement :  quot_ring_car: `Carrier(r/d)` ideal: `Ideal(r){i}` crng: `CRng` rng_car: `|r|` detach_fun: `detach_fun(T;A)` sq_stable: `SqStable(P)` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` subtype_rel: `A ⊆r B` crng: `CRng` rng: `Rng` ideal: `Ideal(r){i}` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` quot_ring_car: `Carrier(r/d)` guard: `{T}` detach_fun: `detach_fun(T;A)` infix_ap: `x f y` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` and: `P ∧ Q` sq_stable: `SqStable(P)` squash: `↓T` ideal_p: `S Ideal of R` subgrp_p: `s SubGrp of g` add_grp_of_rng: `r↓+gp` grp_id: `e` pi2: `snd(t)` pi1: `fst(t)`
Lemmas referenced :  rng_zero_wf iff_weakening_equal rng_plus_inv iff_wf ideal-detach-equiv quotient-member-eq rng_minus_wf rng_plus_wf assert_wf detach_fun_properties crng_wf ideal_wf sq_stable_wf all_wf detach_fun_wf rng_car_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis sqequalRule axiomEquality applyEquality dependent_functionElimination isect_memberEquality because_Cache independent_functionElimination independent_isectElimination dependent_set_memberEquality productElimination independent_pairFormation universeEquality equalityTransitivity equalitySymmetry imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}[r:CRng].  \mforall{}[a:Ideal(r)\{i\}].
((\mforall{}x:|r|.  SqStable(a  x))  {}\mRightarrow{}  (\mforall{}[d:detach\_fun(|r|;a)].  (|r|  \msubseteq{}r  Carrier(r/d))))

Date html generated: 2016_05_15-PM-00_23_40
Last ObjectModification: 2016_01_15-AM-08_51_42

Theory : rings_1

Home Index