### Nuprl Lemma : quot_ring_car_subtype

[r:CRng]. ∀[a:Ideal(r){i}].  ((∀x:|r|. SqStable(a x))  (∀[d:detach_fun(|r|;a)]. (|r| ⊆Carrier(r/d))))

Proof

Definitions occuring in Statement :  quot_ring_car: Carrier(r/d) ideal: Ideal(r){i} crng: CRng rng_car: |r| detach_fun: detach_fun(T;A) sq_stable: SqStable(P) subtype_rel: A ⊆B uall: [x:A]. B[x] all: x:A. B[x] implies:  Q apply: a
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q subtype_rel: A ⊆B crng: CRng rng: Rng ideal: Ideal(r){i} prop: so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] quot_ring_car: Carrier(r/d) guard: {T} detach_fun: detach_fun(T;A) infix_ap: y so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a iff: ⇐⇒ Q rev_implies:  Q and: P ∧ Q sq_stable: SqStable(P) squash: T ideal_p: Ideal of R subgrp_p: SubGrp of g add_grp_of_rng: r↓+gp grp_id: e pi2: snd(t) pi1: fst(t)
Lemmas referenced :  rng_zero_wf iff_weakening_equal rng_plus_inv iff_wf ideal-detach-equiv quotient-member-eq rng_minus_wf rng_plus_wf assert_wf detach_fun_properties crng_wf ideal_wf sq_stable_wf all_wf detach_fun_wf rng_car_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis sqequalRule axiomEquality applyEquality dependent_functionElimination isect_memberEquality because_Cache independent_functionElimination independent_isectElimination dependent_set_memberEquality productElimination independent_pairFormation universeEquality equalityTransitivity equalitySymmetry imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}[r:CRng].  \mforall{}[a:Ideal(r)\{i\}].
((\mforall{}x:|r|.  SqStable(a  x))  {}\mRightarrow{}  (\mforall{}[d:detach\_fun(|r|;a)].  (|r|  \msubseteq{}r  Carrier(r/d))))

Date html generated: 2016_05_15-PM-00_23_40
Last ObjectModification: 2016_01_15-AM-08_51_42

Theory : rings_1

Home Index