### Nuprl Lemma : quot_ring_wf

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

Proof

Definitions occuring in Statement :  quot_ring: `r / 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: `P `` Q` member: `t ∈ T` apply: `f a`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` ideal: `Ideal(r){i}` crng: `CRng` rng: `Rng` all: `∀x:A. B[x]` guard: `{T}` detach_fun: `detach_fun(T;A)` prop: `ℙ` iff: `P `⇐⇒` Q` and: `P ∧ Q` subtype_rel: `A ⊆r B` rev_implies: `P `` Q` ring_p: `IsRing(T;plus;zero;neg;times;one)` quot_ring: `r / 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: `x f 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: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` ideal_p: `S Ideal of R` subgrp_p: `s 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

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