### Nuprl Lemma : ideal_defines_eqv

`∀r:CRng. ∀[a:|r| ⟶ ℙ]. (a Ideal of r `` EquivRel(|r|;u,v.a (u +r (-r v))))`

Proof

Definitions occuring in Statement :  ideal_p: `S Ideal of R` crng: `CRng` rng_minus: `-r` rng_plus: `+r` rng_car: `|r|` equiv_rel: `EquivRel(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` infix_ap: `x f y` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` implies: `P `` Q` ideal_p: `S Ideal of R` and: `P ∧ Q` equiv_rel: `EquivRel(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])` member: `t ∈ T` crng: `CRng` rng: `Rng` prop: `ℙ` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` subgrp_p: `s SubGrp of g` add_grp_of_rng: `r↓+gp` grp_id: `e` pi2: `snd(t)` pi1: `fst(t)` sym: `Sym(T;x,y.E[x; y])` infix_ap: `x f y` trans: `Trans(T;x,y.E[x; y])` grp_car: `|g|` grp_op: `*`
Lemmas referenced :  rng_car_wf ideal_p_wf crng_wf rng_plus_inv iff_weakening_equal rng_plus_wf rng_minus_wf rng_one_wf rng_plus_comm rng_times_over_plus rng_times_over_minus rng_times_one rng_minus_minus rng_plus_assoc rng_plus_ac_1 rng_plus_inv_assoc
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation sqequalHypSubstitution productElimination thin independent_pairFormation cut lemma_by_obid isectElimination setElimination rename hypothesisEquality hypothesis functionEquality cumulativity universeEquality applyEquality lambdaEquality sqequalRule equalityTransitivity equalitySymmetry independent_isectElimination independent_functionElimination dependent_functionElimination because_Cache

Latex:
\mforall{}r:CRng.  \mforall{}[a:|r|  {}\mrightarrow{}  \mBbbP{}].  (a  Ideal  of  r  {}\mRightarrow{}  EquivRel(|r|;u,v.a  (u  +r  (-r  v))))

Date html generated: 2016_05_15-PM-00_23_17
Last ObjectModification: 2015_12_27-AM-00_01_00

Theory : rings_1

Home Index