### Nuprl Lemma : quot_ring_car_qinc

`∀[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` quot_ring_car: `Carrier(r/d)` crng: `CRng` rng: `Rng` so_lambda: `λ2x y.t[x; y]` detach_fun: `detach_fun(T;A)` infix_ap: `x f y` so_apply: `x[s1;s2]` uimplies: `b supposing a` subtype_rel: `A ⊆r B` ideal: `Ideal(r){i}` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]`
Lemmas referenced :  subtype_quotient rng_car_wf assert_wf rng_plus_wf rng_minus_wf detach_fun_wf all_wf sq_stable_wf ideal_wf crng_wf ideal-detach-equiv
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis lambdaEquality applyEquality because_Cache independent_isectElimination axiomEquality dependent_functionElimination isect_memberEquality independent_functionElimination

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: 2019_10_15-AM-10_33_31
Last ObjectModification: 2018_09_17-PM-06_20_49

Theory : rings_1

Home Index