### Nuprl Lemma : princ_ideal_wf

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

Proof

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: `x f y` so_lambda: `λ2x.t[x]` princ_ideal: `(a)r` prop: `ℙ` exists: `∃x:A. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` cand: `A 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: `s SubGrp of g` ideal_p: `S Ideal of R` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` guard: `{T}` uimplies: `b supposing a` subtype_rel: `A ⊆r 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

Latex:
\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