Nuprl Lemma : implies-iso-vs-quotient
∀[K:CRng]. ∀[A:VectorSpace(K)].
∀B:VectorSpace(K)
((∃f:A ⟶ B. Surj(Point(A);Point(B);f)) ⇒ (∃P:Point(A) ⟶ ℙ. (vs-subspace(K;A;z.P[z]) ∧ B ≅ A//z.P[z])))
Proof
Definitions occuring in Statement :
vs-quotient: vs//z.P[z],
vs-iso: A ≅ B,
vs-map: A ⟶ B,
vs-subspace: vs-subspace(K;vs;x.P[x]),
vector-space: VectorSpace(K),
vs-point: Point(vs),
surject: Surj(A;B;f),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
crng: CRng
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
exists: ∃x:A. B[x],
member: t ∈ T,
crng: CRng,
rng: Rng,
vs-map: A ⟶ B,
and: P ∧ Q,
cand: A c∧ B,
so_apply: x[s],
surject: Surj(A;B;f),
vs-iso: A ≅ B,
so_lambda: λ2x.t[x],
uimplies: b supposing a,
subtype_rel: A ⊆r B,
prop: ℙ,
pi1: fst(t),
vs-map-kernel: a ∈ Ker(f),
vs-quotient: vs//z.P[z],
vs-add: x + y,
vs-point: Point(vs),
vs-mul: a * x,
mk-vs: mk-vs,
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
bfalse: ff,
btrue: tt,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
eq-mod-subspace: x = y mod (z.P[z]),
vs-neg: -(x),
vs-subtract: (x - y),
squash: ↓T,
true: True,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
quotient: x,y:A//B[x; y]
Lemmas referenced :
vs-map-kernel_wf,
vs-point_wf,
vs-map-kernel-is-subspace,
vs-map-quotient-kernel,
vs-quotient_wf,
subtype-vs-quotient,
vs-map_wf,
vs-subspace_wf,
vs-iso_wf,
surject_wf,
vector-space_wf,
crng_wf,
eq-mod-subspace-equiv,
rec_select_update_lemma,
quotient-member-eq,
eq-mod-subspace_wf,
vs-add_wf,
equal_wf,
squash_wf,
true_wf,
istype-universe,
vs-map-subtract,
vs-0_wf,
iff_weakening_equal,
equal-iff-vs-subtract-is-0,
vs-mul_wf,
rng_car_wf,
subtype_rel_self,
rng_sig_wf,
quotient_wf,
vs-subtract_wf,
vs-subtract-self
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
sqequalHypSubstitution,
productElimination,
thin,
dependent_pairFormation_alt,
lambdaEquality_alt,
cut,
introduction,
extract_by_obid,
isectElimination,
setElimination,
rename,
because_Cache,
hypothesis,
hypothesisEquality,
universeIsType,
sqequalRule,
independent_pairFormation,
promote_hyp,
independent_isectElimination,
productIsType,
functionIsType,
equalityIstype,
applyEquality,
inhabitedIsType,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
functionExtensionality,
independent_functionElimination,
dependent_set_memberEquality_alt,
Error :memTop,
imageElimination,
instantiate,
natural_numberEquality,
imageMemberEquality,
baseClosed,
universeEquality,
pointwiseFunctionalityForEquality,
pertypeElimination,
sqequalBase
Latex:
\mforall{}[K:CRng]. \mforall{}[A:VectorSpace(K)].
\mforall{}B:VectorSpace(K)
((\mexists{}f:A {}\mrightarrow{} B. Surj(Point(A);Point(B);f))
{}\mRightarrow{} (\mexists{}P:Point(A) {}\mrightarrow{} \mBbbP{}. (vs-subspace(K;A;z.P[z]) \mwedge{} B \mcong{} A//z.P[z])))
Date html generated:
2020_05_20-PM-01_18_18
Last ObjectModification:
2020_01_03-AM-00_42_14
Theory : linear!algebra
Home
Index