Nuprl Lemma : one_ideal_wf

[r:CRng]. ((1r) ∈ Ideal(r){i})


Definitions occuring in Statement :  one_ideal: (1r) ideal: Ideal(r){i} crng: CRng uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  one_ideal: (1r) ideal: Ideal(r){i} uall: [x:A]. B[x] member: t ∈ T crng: CRng rng: Rng ideal_p: Ideal of R and: P ∧ Q cand: c∧ B all: x:A. B[x] implies:  Q true: True prop: subgrp_p: SubGrp of g add_grp_of_rng: r↓+gp grp_car: |g| pi1: fst(t)
Lemmas referenced :  crng_wf true_wf rng_car_wf ideal_p_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution hypothesis axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid dependent_set_memberEquality lambdaEquality isectElimination thin setElimination rename hypothesisEquality independent_pairFormation lambdaFormation natural_numberEquality because_Cache

\mforall{}[r:CRng].  ((1r)  \mmember{}  Ideal(r)\{i\})

Date html generated: 2016_05_15-PM-00_23_05
Last ObjectModification: 2015_12_27-AM-00_01_03

Theory : rings_1

Home Index