Nuprl Lemma : ideal_defines_eqv

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


Definitions occuring in Statement :  ideal_p: 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: y all: x:A. B[x] implies:  Q apply: a function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] implies:  Q ideal_p: 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 ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q subgrp_p: 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: 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

\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