Nuprl Lemma : quot_ring_wf

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


Definitions occuring in Statement :  quot_ring: d ideal: Ideal(r){i} crng: CRng rng_car: |r| detach_fun: detach_fun(T;A) sq_stable: SqStable(P) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q member: t ∈ T apply: a
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q ideal: Ideal(r){i} crng: CRng rng: Rng all: x:A. B[x] guard: {T} detach_fun: detach_fun(T;A) prop: iff: ⇐⇒ Q and: P ∧ Q subtype_rel: A ⊆B rev_implies:  Q ring_p: IsRing(T;plus;zero;neg;times;one) quot_ring: d rng_car: |r| pi1: fst(t) rng_plus: +r pi2: snd(t) rng_zero: 0 rng_minus: -r rng_times: * rng_one: 1 bilinear: BiLinear(T;pl;tm) monoid_p: IsMonoid(T;op;id) group_p: IsGroup(T;op;id;inv) infix_ap: y ident: Ident(T;op;id) assoc: Assoc(T;op) inverse: Inverse(T;op;id;inv) quot_ring_car: Carrier(r/d) quotient: x,y:A//B[x; y] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a ideal_p: Ideal of R subgrp_p: SubGrp of g add_grp_of_rng: r↓+gp grp_car: |g| grp_op: * grp_id: e comm: Comm(T;op)
Lemmas referenced :  detach_fun_properties rng_car_wf quot_ring_car_wf ideal_p_wf subtype_rel_self istype-assert quot_ring_sig detach_fun_wf sq_stable_wf ideal_wf crng_wf comm_wf rng_times_wf ring_p_wf rng_plus_wf rng_zero_wf rng_minus_wf rng_one_wf quotient-member-eq assert_wf ideal-detach-equiv rng_times_assoc iff_weakening_equal rng_times_one sq_stable_functionality rng_minus_over_plus rng_plus_assoc rng_plus_ac_1 rng_plus_comm rng_plus_zero rng_minus_zero rng_plus_inv rng_times_over_plus rng_times_over_minus crng_times_ac_1 crng_times_comm rng_plus_inv_assoc grp_car_wf add_grp_of_rng_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut lambdaFormation_alt sqequalHypSubstitution setElimination thin rename extract_by_obid isectElimination hypothesisEquality hypothesis independent_functionElimination dependent_functionElimination dependent_set_memberEquality_alt because_Cache universeIsType sqequalRule functionIsType productIsType applyEquality instantiate universeEquality axiomEquality equalityTransitivity equalitySymmetry lambdaEquality_alt isect_memberEquality_alt isectIsTypeImplies inhabitedIsType functionIsTypeImplies independent_pairFormation pointwiseFunctionalityForEquality pertypeElimination promote_hyp productElimination independent_isectElimination equalityIstype sqequalBase independent_pairEquality

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

Date html generated: 2019_10_15-AM-10_33_46
Last ObjectModification: 2019_06_20-PM-06_43_59

Theory : rings_1

Home Index