### Nuprl Lemma : det_ideal_defines_eqv

`∀[r:CRng]. ∀[a:Ideal(r){i}]. ∀[d:detach_fun(|r|;a)].  ((∀w:|r|. SqStable(a w)) `` EquivRel(|r|;u,v.↑(d (u +r (-r v)))))`

Proof

Definitions occuring in Statement :  ideal: `Ideal(r){i}` crng: `CRng` rng_minus: `-r` rng_plus: `+r` rng_car: `|r|` detach_fun: `detach_fun(T;A)` equiv_rel: `EquivRel(T;x,y.E[x; y])` assert: `↑b` sq_stable: `SqStable(P)` uall: `∀[x:A]. B[x]` infix_ap: `x f y` 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` prop: `ℙ` crng: `CRng` rng: `Rng` so_lambda: `λ2x.t[x]` ideal: `Ideal(r){i}` so_apply: `x[s]` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` all: `∀x:A. B[x]` detach_fun: `detach_fun(T;A)` infix_ap: `x f y` sym: `Sym(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` guard: `{T}` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` sq_stable: `SqStable(P)` squash: `↓T`
Lemmas referenced :  sq_stable__ideal_p ideal_defines_eqv equiv_rel_functionality_wrt_iff detach_fun_properties crng_wf ideal_wf detach_fun_wf assert_wf rng_minus_wf rng_plus_wf assert_witness sq_stable_wf rng_car_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis sqequalRule lambdaEquality applyEquality dependent_functionElimination productElimination independent_pairEquality independent_functionElimination isect_memberEquality because_Cache independent_isectElimination independent_pairFormation imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}[r:CRng].  \mforall{}[a:Ideal(r)\{i\}].  \mforall{}[d:detach\_fun(|r|;a)].
((\mforall{}w:|r|.  SqStable(a  w))  {}\mRightarrow{}  EquivRel(|r|;u,v.\muparrow{}(d  (u  +r  (-r  v)))))

Date html generated: 2016_05_15-PM-00_23_23
Last ObjectModification: 2016_01_15-AM-08_51_39

Theory : rings_1

Home Index