Nuprl Lemma : det_ideal_ap_elim
∀r:CRng. ∀a:Ideal(r){i}. ∀d:detach_fun(|r|;a). ((∀w:|r|. SqStable(a w)) ⇒ (∀v:|r|. (↑(d v) ⇐⇒ a v)))
Proof
Definitions occuring in Statement :
ideal: Ideal(r){i},
crng: CRng,
rng_car: |r|,
detach_fun: detach_fun(T;A),
assert: ↑b,
sq_stable: SqStable(P),
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
apply: f a
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
uall: ∀[x:A]. B[x],
member: t ∈ T,
ideal: Ideal(r){i},
guard: {T},
detach_fun: detach_fun(T;A),
prop: ℙ,
rev_implies: P ⇐ Q,
crng: CRng,
rng: Rng,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
detach_fun_properties,
assert_wf,
rng_car_wf,
all_wf,
sq_stable_wf,
detach_fun_wf,
ideal_wf,
crng_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
independent_pairFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
because_Cache,
setElimination,
rename,
hypothesisEquality,
independent_functionElimination,
hypothesis,
dependent_functionElimination,
applyEquality,
sqequalRule,
lambdaEquality,
productElimination
Latex:
\mforall{}r:CRng. \mforall{}a:Ideal(r)\{i\}. \mforall{}d:detach\_fun(|r|;a).
((\mforall{}w:|r|. SqStable(a w)) {}\mRightarrow{} (\mforall{}v:|r|. (\muparrow{}(d v) \mLeftarrow{}{}\mRightarrow{} a v)))
Date html generated:
2016_05_15-PM-00_23_20
Last ObjectModification:
2015_12_27-AM-00_00_51
Theory : rings_1
Home
Index