Nuprl Lemma : princ_ideal_wf

[r:Rng]. ∀[a:|r|].  ((a)r ∈ Ideal(r){i})


Definitions occuring in Statement :  princ_ideal: (a)r ideal: Ideal(r){i} rng: Rng rng_car: |r| uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rng: Rng ideal: Ideal(r){i} so_apply: x[s] infix_ap: y so_lambda: λ2x.t[x] princ_ideal: (a)r prop: exists: x:A. B[x] implies:  Q all: x:A. B[x] cand: c∧ B and: P ∧ Q grp_op: * grp_inv: ~ grp_car: |g| pi1: fst(t) pi2: snd(t) grp_id: e add_grp_of_rng: r↓+gp subgrp_p: SubGrp of g ideal_p: Ideal of R rev_implies:  Q iff: ⇐⇒ Q guard: {T} uimplies: supposing a subtype_rel: A ⊆B true: True squash: T
Lemmas referenced :  rng_car_wf rng_wf rng_times_wf equal_wf exists_wf rng_times_zero rng_zero_wf rng_times_over_minus iff_weakening_equal infix_ap_wf true_wf squash_wf rng_minus_wf rng_times_over_plus rng_plus_wf rng_times_assoc subgrp_p_wf add_grp_of_rng_wf subtype_rel_self
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry universeIsType extract_by_obid isectElimination thin setElimination rename hypothesisEquality isect_memberEquality_alt because_Cache dependent_set_memberEquality_alt applyEquality lambdaEquality productElimination lambdaFormation independent_pairFormation dependent_pairFormation independent_functionElimination independent_isectElimination baseClosed imageMemberEquality natural_numberEquality levelHypothesis equalityUniverse universeEquality imageElimination cumulativity functionEquality productIsType functionIsType inhabitedIsType instantiate

\mforall{}[r:Rng].  \mforall{}[a:|r|].    ((a)r  \mmember{}  Ideal(r)\{i\})

Date html generated: 2019_10_15-AM-10_33_28
Last ObjectModification: 2018_10_08-AM-09_08_21

Theory : rings_1

Home Index