Nuprl Lemma : zero_ideal_wf

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


Definitions occuring in Statement :  zero_ideal: (0r) ideal: Ideal(r){i} crng: CRng uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  zero_ideal: (0r) 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 prop: subgrp_p: SubGrp of g add_grp_of_rng: r↓+gp grp_id: e pi2: snd(t) pi1: fst(t) grp_car: |g| grp_inv: ~ grp_op: * squash: T true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q infix_ap: y
Lemmas referenced :  crng_wf equal_wf rng_car_wf rng_zero_wf squash_wf true_wf rng_minus_zero iff_weakening_equal rng_minus_wf rng_plus_zero rng_plus_wf member_wf rng_times_zero rng_times_wf ideal_p_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution hypothesis axiomEquality equalityTransitivity equalitySymmetry extract_by_obid dependent_set_memberEquality lambdaEquality isectElimination thin setElimination rename hypothesisEquality because_Cache independent_pairFormation lambdaFormation applyEquality imageElimination universeEquality equalityUniverse levelHypothesis natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination hyp_replacement applyLambdaEquality instantiate functionExtensionality

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

Date html generated: 2017_10_01-AM-08_17_42
Last ObjectModification: 2017_02_28-PM-02_03_01

Theory : rings_1

Home Index