Nuprl Lemma : quot_ring_car_elim_b
∀r:CRng. ∀a:Ideal(r){i}. ∀d:detach_fun(|r|;a).
((∀w:|r|. SqStable(a w)) ⇒ (∀u,v:|r|. ([u]{|r / d|} = [v]{|r / d|} ∈ |r / d| ⇐⇒ a (u +r (-r v)))))
Proof
Definitions occuring in Statement :
quot_ring: r / d,
ideal: Ideal(r){i},
crng: CRng,
rng_minus: -r,
rng_plus: +r,
rng_car: |r|,
detach_fun: detach_fun(T;A),
type_inj: [x]{T},
sq_stable: SqStable(P),
infix_ap: x f y,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
apply: f a,
equal: s = t ∈ T
Definitions unfolded in proof :
type_inj: [x]{T}
Lemmas referenced :
quot_ring_car_elim_a
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lemma_by_obid
Latex:
\mforall{}r:CRng. \mforall{}a:Ideal(r)\{i\}. \mforall{}d:detach\_fun(|r|;a).
((\mforall{}w:|r|. SqStable(a w)) {}\mRightarrow{} (\mforall{}u,v:|r|. ([u]\{|r / d|\} = [v]\{|r / d|\} \mLeftarrow{}{}\mRightarrow{} a (u +r (-r v)))))
Date html generated:
2016_05_15-PM-00_24_31
Last ObjectModification:
2015_12_27-AM-00_00_24
Theory : rings_1
Home
Index