Nuprl Lemma : quot_ring_sig

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


Definitions occuring in Statement :  quot_ring: 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:  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: so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q rev_implies:  Q and: P ∧ Q quot_ring: d rng_sig: RngSig quot_ring_car: Carrier(r/d) quotient: x,y:A//B[x; y] infix_ap: y uimplies: 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: λ2y.t[x; y] so_apply: x[s1;s2] ideal_p: Ideal of R subgrp_p: SubGrp of g subtype_rel: A ⊆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

\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