### Nuprl Lemma : quot_ring_sig

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

Proof

Definitions occuring in Statement :  quot_ring: `r / d` ideal: `Ideal(r){i}` crng: `CRng` rng_car: `|r|` rng_sig: `RngSig` 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: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` and: `P ∧ Q` quot_ring: `r / d` rng_sig: `RngSig` quot_ring_car: `Carrier(r/d)` quotient: `x,y:A//B[x; y]` infix_ap: `x f y` uimplies: `b supposing a` equiv_rel: `EquivRel(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` sym: `Sym(T;x,y.E[x; y])` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` ideal_p: `S Ideal of R` subgrp_p: `s SubGrp of g` subtype_rel: `A ⊆r B` add_grp_of_rng: `r↓+gp` grp_car: `|g|` pi1: `fst(t)` grp_op: `*` pi2: `snd(t)`
Lemmas referenced :  detach_fun_properties rng_car_wf quot_ring_car_wf ideal_p_wf all_wf iff_wf assert_wf unit_wf2 bool_wf detach_fun_wf sq_stable_wf ideal_wf crng_wf rng_plus_wf rng_minus_wf equal_wf equal-wf-base iff_imp_equal_bool ideal-detach-equiv btrue_wf quotient-member-eq rng_plus_assoc iff_weakening_equal infix_ap_wf rng_minus_over_plus rng_plus_comm rng_plus_ac_1 rng_zero_wf quot_ring_car_subtype rng_one_wf rng_minus_minus rng_times_over_plus rng_times_over_minus rng_times_one rng_times_wf crng_times_comm rng_plus_inv_assoc it_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution setElimination thin rename extract_by_obid isectElimination hypothesisEquality hypothesis independent_functionElimination dependent_functionElimination dependent_set_memberEquality because_Cache functionExtensionality applyEquality sqequalRule lambdaEquality dependent_pairEquality functionEquality unionEquality productEquality cumulativity axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality pointwiseFunctionalityForEquality pertypeElimination productElimination independent_isectElimination independent_pairFormation allFunctionality promote_hyp universeEquality inrEquality

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{}  RngSig)))

Date html generated: 2017_10_01-AM-08_17_54
Last ObjectModification: 2017_02_28-PM-02_03_58

Theory : rings_1

Home Index