Nuprl Lemma : all_rng_quot_elim
∀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]))))
Proof
Definitions occuring in Statement :
quot_ring: r / d,
ideal: Ideal(r){i},
crng: CRng,
rng_car: |r|,
detach_fun: detach_fun(T;A),
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 :
all: ∀x:A. B[x],
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
member: t ∈ T,
crng: CRng,
rng: Rng,
prop: ℙ,
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a,
so_lambda: λ2x.t[x],
so_apply: x[s],
rev_implies: P ⇐ Q,
sq_stable: SqStable(P),
ideal: Ideal(r){i},
detach_fun: detach_fun(T;A),
quot_ring: r / d,
rng_car: |r|,
pi1: fst(t),
quot_ring_car: Carrier(r/d),
quotient: x,y:A//B[x; y],
squash: ↓T,
infix_ap: x f y
Lemmas referenced :
rng_car_wf,
all_wf,
quot_ring_wf,
rng_subtype_rng_sig,
crng_subtype_rng,
subtype_rel_transitivity,
crng_wf,
rng_wf,
rng_sig_wf,
detach_fun_properties,
squash_wf,
equal-wf-base,
assert_wf,
rng_plus_wf,
rng_minus_wf,
quot_ring_car_subtype,
sq_stable_wf,
detach_fun_wf,
ideal_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
independent_pairFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
setElimination,
rename,
hypothesisEquality,
hypothesis,
independent_functionElimination,
applyEquality,
instantiate,
independent_isectElimination,
sqequalRule,
lambdaEquality,
because_Cache,
dependent_functionElimination,
pointwiseFunctionalityForEquality,
pertypeElimination,
productElimination,
equalityTransitivity,
equalitySymmetry,
imageMemberEquality,
baseClosed,
productEquality,
functionEquality,
cumulativity,
universeEquality
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]))))
Date html generated:
2018_05_21-PM-03_14_41
Last ObjectModification:
2018_05_19-AM-08_07_56
Theory : rings_1
Home
Index