### Nuprl Lemma : quot_ring_car_elim

`∀[r:CRng]. ∀[a:Ideal(r){i}].`
`  ((∀x:|r|. SqStable(a x)) `` (∀[d:detach_fun(|r|;a)]. ∀[u,v:|r|].  uiff(u = v ∈ Carrier(r/d);↑(d (u +r (-r v))))))`

Proof

Definitions occuring in Statement :  quot_ring_car: `Carrier(r/d)` ideal: `Ideal(r){i}` crng: `CRng` rng_minus: `-r` rng_plus: `+r` rng_car: `|r|` detach_fun: `detach_fun(T;A)` assert: `↑b` sq_stable: `SqStable(P)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` infix_ap: `x f y` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` detach_fun: `detach_fun(T;A)` infix_ap: `x f y` crng: `CRng` rng: `Rng` prop: `ℙ` subtype_rel: `A ⊆r B` ideal: `Ideal(r){i}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` quot_ring_car: `Carrier(r/d)` quotient: `x,y:A//B[x; y]` sq_type: `SQType(T)` guard: `{T}` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` true: `True` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  assert_witness rng_plus_wf rng_minus_wf equal_wf quot_ring_car_wf quot_ring_car_subtype assert_wf rng_car_wf detach_fun_wf all_wf sq_stable_wf ideal_wf crng_wf assert_elim subtype_base_sq bool_wf bool_subtype_base and_wf member_wf quotient-member-eq det_ideal_defines_eqv
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation independent_pairFormation lemma_by_obid sqequalHypSubstitution isectElimination thin applyEquality setElimination rename hypothesisEquality hypothesis independent_functionElimination sqequalRule productElimination independent_pairEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry axiomEquality lambdaEquality dependent_functionElimination pertypeElimination independent_isectElimination instantiate cumulativity natural_numberEquality

Latex:
\mforall{}[r:CRng].  \mforall{}[a:Ideal(r)\{i\}].
((\mforall{}x:|r|.  SqStable(a  x))  {}\mRightarrow{}  (\mforall{}[d:detach\_fun(|r|;a)].  \mforall{}[u,v:|r|].    uiff(u  =  v;\muparrow{}(d  (u  +r  (-r  v))))))

Date html generated: 2016_05_15-PM-00_24_25
Last ObjectModification: 2015_12_27-AM-00_00_32

Theory : rings_1

Home Index