Nuprl Lemma : mk-vs_wf
∀[K:RngSig]. ∀[V:Type]. ∀[z:V]. ∀[+:V ⟶ V ⟶ V]. ∀[*:|K| ⟶ V ⟶ V].
Point= V
zero= z
x+y= +[x;y]
a*u= *[a;u] ∈ VectorSpace(K)
supposing (∀x,y,z:V. (+[x;+[y;z]] = +[+[x;y];z] ∈ V))
∧ (∀x,y:V. (+[x;y] = +[y;x] ∈ V))
∧ (∀a:|K|. ∀x,y:V. (*[a;+[x;y]] = +[*[a;x];*[a;y]] ∈ V))
∧ (∀x:V. (*[1;x] = x ∈ V))
∧ (∀x:V. (*[0;x] = z ∈ V))
∧ (∀x:V. ∀a,b:|K|. (*[a;*[b;x]] = *[a * b;x] ∈ V))
∧ (∀x:V. ∀a,b:|K|. (*[a +K b;x] = +[*[a;x];*[b;x]] ∈ V))
Proof
Definitions occuring in Statement :
mk-vs: mk-vs,
vector-space: VectorSpace(K),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
infix_ap: x f y,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
and: P ∧ Q,
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T,
rng_one: 1,
rng_times: *,
rng_zero: 0,
rng_plus: +r,
rng_car: |r|,
rng_sig: RngSig
Definitions unfolded in proof :
infix_ap: x f y,
true: True,
squash: ↓T,
so_apply: x[s],
so_lambda: λ2x.t[x],
cand: A c∧ B,
so_apply: x[s1;s2],
vs-point: Point(vs),
rev_implies: P ⇐ Q,
prop: ℙ,
not: ¬A,
iff: P ⇐⇒ Q,
bfalse: ff,
eq_atom: x =a y,
top: Top,
record-select: r.x,
guard: {T},
sq_type: SQType(T),
ifthenelse: if b then t else f fi ,
uiff: uiff(P;Q),
subtype_rel: A ⊆r B,
btrue: tt,
it: ⋅,
unit: Unit,
bool: 𝔹,
implies: P ⇒ Q,
all: ∀x:A. B[x],
record: record(x.T[x]),
record-update: r[x := v],
record+: record+,
vector-space: VectorSpace(K),
mk-vs: mk-vs,
and: P ∧ Q,
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
rng_sig_wf,
rng_plus_wf,
rng_zero_wf,
rng_one_wf,
rng_times_wf,
infix_ap_wf,
iff_weakening_equal,
true_wf,
squash_wf,
rng_car_wf,
all_wf,
equal_wf,
assert_of_bnot,
eqff_to_assert,
iff_weakening_uiff,
not_wf,
bnot_wf,
iff_transitivity,
rec_select_update_lemma,
subtype_base_sq,
assert_of_eq_atom,
eqtt_to_assert,
atom_subtype_base,
assert_wf,
bool_wf,
equal-wf-base,
uiff_transitivity,
eq_atom_wf
Rules used in proof :
functionEquality,
axiomEquality,
imageMemberEquality,
natural_numberEquality,
universeEquality,
imageElimination,
productEquality,
lambdaEquality,
dependent_set_memberEquality,
impliesFunctionality,
independent_pairFormation,
voidEquality,
voidElimination,
isect_memberEquality,
equalitySymmetry,
equalityTransitivity,
dependent_functionElimination,
cumulativity,
instantiate,
independent_isectElimination,
independent_functionElimination,
atomEquality,
applyEquality,
baseClosed,
closedConclusion,
baseApply,
equalityElimination,
unionElimination,
lambdaFormation,
hypothesis,
tokenEquality,
hypothesisEquality,
isectElimination,
extract_by_obid,
functionExtensionality,
because_Cache,
dependentIntersection_memberEquality,
sqequalRule,
thin,
productElimination,
sqequalHypSubstitution,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[K:RngSig]. \mforall{}[V:Type]. \mforall{}[z:V]. \mforall{}[+:V {}\mrightarrow{} V {}\mrightarrow{} V]. \mforall{}[*:|K| {}\mrightarrow{} V {}\mrightarrow{} V].
Point= V
zero= z
x+y= +[x;y]
a*u= *[a;u] \mmember{} VectorSpace(K)
supposing (\mforall{}x,y,z:V. (+[x;+[y;z]] = +[+[x;y];z]))
\mwedge{} (\mforall{}x,y:V. (+[x;y] = +[y;x]))
\mwedge{} (\mforall{}a:|K|. \mforall{}x,y:V. (*[a;+[x;y]] = +[*[a;x];*[a;y]]))
\mwedge{} (\mforall{}x:V. (*[1;x] = x))
\mwedge{} (\mforall{}x:V. (*[0;x] = z))
\mwedge{} (\mforall{}x:V. \mforall{}a,b:|K|. (*[a;*[b;x]] = *[a * b;x]))
\mwedge{} (\mforall{}x:V. \mforall{}a,b:|K|. (*[a +K b;x] = +[*[a;x];*[b;x]]))
Date html generated:
2018_05_22-PM-09_41_46
Last ObjectModification:
2018_01_09-PM-01_03_32
Theory : linear!algebra
Home
Index