Nuprl Lemma : all_rng_quot_elim_a
∀r:CRng. ∀p:Ideal(r){i}.
((∀x:|r|. SqStable(p x))
⇒ (∀d:detach_fun(|r|;p)
∀[F:|r / d| ⟶ ℙ]. ((∀w:|r / d|. SqStable(F[w])) ⇒ (∀w:|r / d|. F[w] ⇐⇒ ∀w:|r|. F[[w]{|r / d|}]))))
Proof
Definitions occuring in Statement :
quot_ring: r / d,
ideal: Ideal(r){i},
crng: CRng,
rng_car: |r|,
detach_fun: detach_fun(T;A),
type_inj: [x]{T},
sq_stable: SqStable(P),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
type_inj: [x]{T}
Lemmas referenced :
all_rng_quot_elim
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}r:CRng. \mforall{}p:Ideal(r)\{i\}.
((\mforall{}x:|r|. SqStable(p x))
{}\mRightarrow{} (\mforall{}d:detach\_fun(|r|;p)
\mforall{}[F:|r / d| {}\mrightarrow{} \mBbbP{}]
((\mforall{}w:|r / d|. SqStable(F[w])) {}\mRightarrow{} (\mforall{}w:|r / d|. F[w] \mLeftarrow{}{}\mRightarrow{} \mforall{}w:|r|. F[[w]\{|r / d|\}]))))
Date html generated:
2016_05_15-PM-00_24_36
Last ObjectModification:
2015_12_27-AM-00_00_20
Theory : rings_1
Home
Index