Nuprl Lemma : nsgrp_of_ideal_wf

[r:CRng]. ∀[a:Ideal(r){i}].  (a↓+nsgp ∈ NormSubGrp{i}(r↓+gp))


Definitions occuring in Statement :  nsgrp_of_ideal: a↓+nsgp ideal: Ideal(r){i} add_grp_of_rng: r↓+gp crng: CRng norm_subgrp: NormSubGrp{i}(g) uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T ideal: Ideal(r){i} norm_subgrp: NormSubGrp{i}(g) nsgrp_of_ideal: a↓+nsgp add_grp_of_rng: r↓+gp grp_car: |g| pi1: fst(t) and: P ∧ Q cand: c∧ B crng: CRng rng: Rng prop: subgrp_p: SubGrp of g grp_id: e pi2: snd(t) grp_inv: ~ grp_op: * all: x:A. B[x] implies:  Q guard: {T} ideal_p: Ideal of R norm_subset_p: norm_subset_p(g;s) infix_ap: y subtype_rel: A ⊆B uimplies: supposing a iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  subgrp_p_wf add_grp_of_rng_wf norm_subset_p_wf ideal_wf crng_wf rng_car_wf rng_plus_wf rng_minus_wf rng_plus_comm rng_plus_ac_1 rng_plus_inv_assoc iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality sqequalRule hypothesisEquality independent_pairFormation hypothesis productEquality lemma_by_obid isectElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache lambdaFormation applyEquality productElimination dependent_functionElimination independent_functionElimination lambdaEquality universeEquality independent_isectElimination

\mforall{}[r:CRng].  \mforall{}[a:Ideal(r)\{i\}].    (a\mdownarrow{}+nsgp  \mmember{}  NormSubGrp\{i\}(r\mdownarrow{}+gp))

Date html generated: 2016_05_15-PM-00_23_27
Last ObjectModification: 2015_12_27-AM-00_00_44

Theory : rings_1

Home Index