:: Linear Combinations in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, REAL_1, STRUCT_0, FUNCT_1,
XBOOLE_0, ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3, ORDINAL4,
XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1, FUNCT_2, FINSET_1,
FUNCOP_1, VALUED_1, RLSUB_1, QC_LANG1, BINOP_1, ZFMISC_1, RLVECT_2,
LATTICES, VECTSP_1, PRE_POLY, FUNCT_7;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, XREAL_0, FINSET_1, FINSEQ_1, RELAT_1, FUNCT_1,
RELSET_1, PRE_POLY, PARTFUN1, FUNCT_2, FUNCOP_1, DOMAIN_1, VALUED_1,
FINSEQ_4, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, REAL_1,
RLSUB_1, NAT_1, BINOP_1, XXREAL_0;
constructors PARTFUN1, BINOP_1, DOMAIN_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1,
FINSEQ_4, RLSUB_1, VALUED_1, RELSET_1, VECTSP_1, PRE_POLY, RLVECT_1,
NUMBERS, GROUP_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, RLVECT_1, RLSUB_1, VALUED_1, VALUED_0, MEMBERED,
FINSEQ_1, CARD_1, VECTSP_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FUNCT_1, RLSUB_1, TARSKI, XBOOLE_0, RLVECT_1, FUNCT_2, ALGSTR_0;
equalities XBOOLE_0, BINOP_1, RLVECT_1, RELAT_1, STRUCT_0, ALGSTR_0;
expansions FUNCT_1, RLSUB_1, TARSKI, XBOOLE_0, BINOP_1, FUNCT_2, STRUCT_0;
theorems CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4,
FUNCT_1, FUNCT_2, NAT_1, RLSUB_1, RLSUB_2, RLVECT_1, TARSKI, ZFMISC_1,
RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0,
ORDINAL1, PARTFUN1, VALUED_1, XREAL_0, VECTSP_1, PRE_POLY;
schemes BINOP_1, FINSEQ_1, FUNCT_2, NAT_1, XBOOLE_0;
begin
reserve x,y,y1,y2 for set,
p for FinSequence,
i,k,l,n for Nat,
V for RealLinearSpace,
u,v,v1,v2,v3,w for VECTOR of V,
a,b for Real,
F,G,H1,H2 for FinSequence of V,
A,B for Subset of V,
f for Function of the carrier of V, REAL;
definition
let S be 1-sorted;
let x;
assume
A1: x in S;
func vector(S,x) -> Element of S equals
:Def1:
x;
coherence by A1;
end;
theorem
for S being non empty 1-sorted,v being Element of S holds vector(S,v) = v
by Def1,RLVECT_1:1;
theorem Th2:
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, F,G,H being FinSequence of the
carrier of V st len F = len G & len F = len H & for k st k in dom F holds H.k =
F/.k + G/.k holds Sum(H) = Sum(F) + Sum(G)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr;
defpred P[Nat] means
for F,G,H be FinSequence of the carrier of V
st len F = $1 & len F = len G & len F = len H & (for k st k in dom F holds H.k
= F/.k + G/.k) holds Sum(H) = Sum(F) + Sum(G);
now
let k;
assume
A1: for F,G,H be FinSequence of the carrier of V st len F = k & len F
= len G & len F = len H & (for k st k in dom F holds H.k = F/.k + G/.k) holds
Sum(H) = Sum(F) + Sum(G);
let F,G,H be FinSequence of the carrier of V;
assume that
A2: len F = k + 1 and
A3: len F = len G and
A4: len F = len H and
A5: for k st k in dom F holds H.k = F/.k + G/.k;
reconsider f = F | Seg k,g = G | Seg k,h = H | Seg k as FinSequence of the
carrier of V by FINSEQ_1:18;
A6: len h = k by A2,A4,FINSEQ_3:53;
A7: k + 1 in Seg(k + 1) by FINSEQ_1:4;
then
A8: k + 1 in dom G by A2,A3,FINSEQ_1:def 3;
then
A9: G.(k + 1) in rng G by FUNCT_1:def 3;
k + 1 in dom H by A2,A4,A7,FINSEQ_1:def 3;
then
A10: H.(k + 1) in rng H by FUNCT_1:def 3;
A11: k + 1 in dom F by A2,A7,FINSEQ_1:def 3;
then F.(k + 1) in rng F by FUNCT_1:def 3;
then reconsider
v = F.(k + 1),u = G.(k + 1),w = H.(k + 1) as Element of V by A9,A10;
A12: w = F/.(k + 1) + G/.(k + 1) by A5,A11
.= v + G/.(k + 1) by A11,PARTFUN1:def 6
.= v + u by A8,PARTFUN1:def 6;
G = g ^ <* u *> by A2,A3,FINSEQ_3:55;
then
A13: Sum(G) = Sum(g) + Sum<* u *> by RLVECT_1:41;
A14: Sum<* v *> = v by RLVECT_1:44;
A15: len f = k by A2,FINSEQ_3:53;
A16: len g = k by A2,A3,FINSEQ_3:53;
now
let i;
assume
A17: i in dom f;
then
A18: F.i = f.i by FUNCT_1:47;
len f <= len F by A2,A15,NAT_1:12;
then
A19: dom f c= dom F by FINSEQ_3:30;
then i in dom F by A17;
then i in dom G by A3,FINSEQ_3:29;
then
A20: G/.i = G.i by PARTFUN1:def 6;
i in dom h by A15,A6,A17,FINSEQ_3:29;
then
A21: H.i = h.i by FUNCT_1:47;
F/.i = F.i by A17,A19,PARTFUN1:def 6;
then
A22: f/.i = F/.i by A17,A18,PARTFUN1:def 6;
A23: i in dom g by A15,A16,A17,FINSEQ_3:29;
then G.i = g.i by FUNCT_1:47;
then g/.i = G/.i by A23,A20,PARTFUN1:def 6;
hence h.i = f/.i + g/.i by A5,A17,A21,A19,A22;
end;
then
A24: Sum(h) = Sum(f) + Sum(g) by A1,A15,A16,A6;
F = f ^ <* v *> by A2,FINSEQ_3:55;
then
A25: Sum(F) = Sum(f) + Sum<* v *> by RLVECT_1:41;
A26: Sum<* u *> = u by RLVECT_1:44;
H = h ^ <* w *> by A2,A4,FINSEQ_3:55;
hence Sum(H) = Sum(h) + Sum<* w *> by RLVECT_1:41
.= Sum(f) + Sum(g) + (v + u) by A24,A12,RLVECT_1:44
.= Sum(f) + Sum(g) + v + u by RLVECT_1:def 3
.= Sum(F) + Sum(g) + u by A25,A14,RLVECT_1:def 3
.= Sum(F) + Sum(G) by A13,A26,RLVECT_1:def 3;
end;
then
A27: for k st P[k] holds P[k+1];
A28: P[0]
proof
let F,G,H be FinSequence of the carrier of V;
assume that
A29: len F = 0 and
A30: len F = len G and
A31: len F = len H;
A32: Sum(H) = 0.V by A29,A31,RLVECT_1:75;
Sum(F) = 0.V & Sum(G) = 0.V by A29,A30,RLVECT_1:75;
hence thesis by A32;
end;
for k holds P[k] from NAT_1:sch 2(A28,A27);
hence thesis;
end;
theorem
len F = len G & (for k st k in dom F holds G.k = a * F/.k) implies Sum
(G) = a * Sum(F)
proof
assume that
A1: len F = len G and
A2: for k st k in dom F holds G.k = a * F/.k;
A3: dom F = Seg len F & dom G = Seg len G by FINSEQ_1:def 3;
now
let k be Nat,v;
assume that
A4: k in dom G and
A5: v = F.k;
v = F/.k by A1,A3,A4,A5,PARTFUN1:def 6;
hence G.k = a * v by A1,A2,A3,A4;
end;
hence thesis by A1,RLVECT_1:39;
end;
theorem Th4:
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, F,G being FinSequence of the
carrier of V st len F = len G & (for k st k in dom F holds G.k = - F/.k) holds
Sum(G) = - Sum(F)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, F,G be FinSequence of the carrier of V;
assume that
A1: len F = len G and
A2: for k st k in dom F holds G.k = - F/.k;
now
let k be Nat;
let v be Element of V;
assume that
A3: k in dom G and
A4: v = F.k;
A5: dom G = Seg len G & dom F = Seg len F by FINSEQ_1:def 3;
then v = F/.k by A1,A3,A4,PARTFUN1:def 6;
hence G.k = - v by A1,A2,A3,A5;
end;
hence thesis by A1,RLVECT_1:40;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, F,G,H being FinSequence of the carrier of V st len F =
len G & len F = len H & (for k st k in dom F holds H.k = F/.k - G/.k) holds Sum
(H) = Sum(F) - Sum(G)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, F,G,H be FinSequence of the carrier of V;
assume that
A1: len F = len G and
A2: len F = len H and
A3: for k st k in dom F holds H.k = F/.k - G/.k;
deffunc Q(set)= - G/.$1;
consider I being FinSequence such that
A4: len I = len G and
A5: for k be Nat st k in dom I holds I.k = Q(k) from FINSEQ_1:sch 2;
dom I = Seg len G by A4,FINSEQ_1:def 3;
then
A6: dom G = Seg len G & for k st k in Seg len G holds I.k = Q(k) by A5,
FINSEQ_1:def 3;
rng I c= the carrier of V
proof
let x be object;
assume x in rng I;
then consider y being object such that
A7: y in dom I and
A8: I.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A7;
x = - G/.y by A5,A7,A8;
then reconsider v = x as Element of V;
v in V;
hence thesis;
end;
then reconsider I as FinSequence of the carrier of V by FINSEQ_1:def 4;
A9: now
let k;
assume
A10: k in dom F;
A11: dom F = Seg len F & dom I = Seg len I by FINSEQ_1:def 3;
then
A12: I.k = I/.k by A1,A4,A10,PARTFUN1:def 6;
thus H.k = F/.k - G/.k by A3,A10
.= F/.k + I/.k by A1,A4,A5,A11,A10,A12;
end;
Sum(I) = - Sum(G) by A4,A6,Th4;
hence thesis by A1,A2,A4,A9,Th2;
end;
theorem Th6:
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, F,G being FinSequence of the
carrier of V for f being Permutation of dom F st len F = len G & (for i st i in
dom G holds G.i = F.(f.i)) holds Sum(F) = Sum(G)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, F,G be FinSequence of the carrier of V;
let f be Permutation of dom F;
defpred P[Nat] means
for H1,H2 be FinSequence of the carrier of V
st len H1 = $1 & len H1 = len H2 for f being Permutation of dom H1 st (for i st
i in dom H2 holds H2.i = H1.(f.i)) holds Sum(H1) = Sum(H2);
now
let k;
assume
A1: for H1,H2 be FinSequence of the carrier of V st len H1 = k & len
H1 = len H2 for f being Permutation of dom H1 st (for i st i in dom H2 holds H2
.i = H1.(f.i)) holds Sum(H1) = Sum(H2);
let H1,H2 be FinSequence of the carrier of V;
assume that
A2: len H1 = k + 1 and
A3: len H1 = len H2;
reconsider p = H2 | (Seg k) as FinSequence of the carrier of V by
FINSEQ_1:18;
let f be Permutation of dom H1;
A4: dom H1 = Seg(k + 1) by A2,FINSEQ_1:def 3;
then
A5: rng f = Seg(k + 1) by FUNCT_2:def 3;
A6: now
let n;
assume n in dom f;
then f.n in Seg(k + 1) by A5,FUNCT_1:def 3;
hence f.n is Element of NAT;
end;
A7: dom H2 = Seg(k + 1) by A2,A3,FINSEQ_1:def 3;
then reconsider v = H2.(k + 1) as Element of V by FINSEQ_1:4,FUNCT_1:102;
A8: dom p = Seg len p by FINSEQ_1:def 3;
Seg(k + 1) = {} implies Seg(k + 1) = {};
then
A9: dom f = Seg(k + 1) by A4,FUNCT_2:def 1;
A10: k + 1 in Seg(k + 1) by FINSEQ_1:4;
then
A11: f.(k + 1) in Seg(k + 1) by A9,A5,FUNCT_1:def 3;
then reconsider n = f.(k + 1) as Element of NAT;
A12: n <= k + 1 by A11,FINSEQ_1:1;
then consider m2 being Nat such that
A13: n + m2 = k + 1 by NAT_1:10;
defpred P[Nat,object] means $2 = H1.(n + $1);
1 <= n by A11,FINSEQ_1:1;
then consider m1 being Nat such that
A14: 1 + m1 = n by NAT_1:10;
reconsider m1,m2 as Element of NAT by ORDINAL1:def 12;
A15: for j be Nat st j in Seg m2 ex x being object st P[j,x];
consider q2 being FinSequence such that
A16: dom q2 = Seg m2 and
A17: for k be Nat st k in Seg m2 holds P[k,q2.k] from FINSEQ_1:sch 1 (
A15);
rng q2 c= the carrier of V
proof
let x be object;
assume x in rng q2;
then consider y being object such that
A18: y in dom q2 and
A19: x = q2.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A18;
1 <= y by A16,A18,FINSEQ_1:1;
then
A20: 1 <= n + y by NAT_1:12;
y <= m2 by A16,A18,FINSEQ_1:1;
then n + y <= len H1 by A2,A13,XREAL_1:7;
then n + y in dom H1 by A20,FINSEQ_3:25;
then reconsider xx = H1.(n + y) as Element of V by FUNCT_1:102;
xx in the carrier of V;
hence thesis by A16,A17,A18,A19;
end;
then reconsider q2 as FinSequence of the carrier of V by FINSEQ_1:def 4;
reconsider q1 = H1 | (Seg m1) as FinSequence of the carrier of V by
FINSEQ_1:18;
defpred P[set,object] means
(f.$1 in dom q1 implies $2 = f.$1) & (not f.$1 in
dom q1 implies for l st l = f.$1 holds $2 = l - 1);
A21: k <= k + 1 by NAT_1:12;
then
A22: Seg k c= Seg(k + 1) by FINSEQ_1:5;
A23: for i be Nat st i in Seg k ex y being object st P[i,y]
proof
let i be Nat;
assume
A24: i in Seg k;
now
f.i in Seg(k + 1) by A9,A5,A22,A24,FUNCT_1:def 3;
then reconsider j = f.i as Element of NAT;
assume
A25: not f.i in dom q1;
take y = j - 1;
thus f.i in dom q1 implies y = f.i by A25;
assume not f.i in dom q1;
let t be Nat;
assume t = f.i;
hence y = t - 1;
end;
hence thesis;
end;
consider g being FinSequence such that
A26: dom g = Seg k and
A27: for i be Nat st i in Seg k holds P[i,g.i] from FINSEQ_1:sch 1(A23
);
A28: dom p = Seg k by A2,A3,A21,FINSEQ_1:17;
m1 <= n by A14,NAT_1:11;
then
A29: m1 <= k + 1 by A12,XXREAL_0:2;
then
A30: dom q1 = Seg m1 by A2,FINSEQ_1:17;
A31: now
let i,l;
assume that
A32: l = f.i and
A33: not f.i in dom q1 and
A34: i in dom g;
A35: l < 1 or m1 < l by A30,A32,A33,FINSEQ_1:1;
A36: now
assume m1 + 1 = l;
then k + 1 = i by A10,A9,A14,A22,A26,A32,A34,FUNCT_1:def 4;
then k + 1 <= k + 0 by A26,A34,FINSEQ_1:1;
hence contradiction by XREAL_1:6;
end;
f.i in rng f by A9,A22,A26,A34,FUNCT_1:def 3;
then m1 + 1 <= l by A4,A32,A35,FINSEQ_1:1,NAT_1:13;
then m1 + 1 < l by A36,XXREAL_0:1;
then m1 + 1 + 1 <= l by NAT_1:13;
hence m1 + 2 <= l;
end;
A37: len q1 = m1 by A2,A29,FINSEQ_1:17;
A38: now
let j be Nat;
assume
A39: j in dom q2;
len(q1 ^ <* v *>) = m1 + len<* v *> by A37,FINSEQ_1:22
.= n by A14,FINSEQ_1:39;
hence H1.(len(q1 ^ <* v *>) + j) = q2.j by A16,A17,A39;
end;
1 + k = 1 + (m1 + m2) by A14,A13;
then
A40: m1 <= k by NAT_1:11;
A41: rng g c= dom p
proof
let y be object;
assume y in rng g;
then consider x being object such that
A42: x in dom g and
A43: g.x = y by FUNCT_1:def 3;
reconsider x as Element of NAT by A42;
now
per cases;
suppose
A44: f.x in dom q1;
A45: dom q1 c= dom p by A40,A30,A28,FINSEQ_1:5;
f.x = g.x by A26,A27,A42,A44;
hence thesis by A43,A44,A45;
end;
suppose
A46: not f.x in dom q1;
reconsider j = f.x as Element of NAT by A9,A22,A6,A26,A42;
A47: f.x in Seg(k + 1) by A9,A5,A22,A26,A42,FUNCT_1:def 3;
j < 1 or m1 < j by A30,A46,FINSEQ_1:1;
then reconsider l = j - 1 as Element of NAT by A47,FINSEQ_1:1
,NAT_1:20;
j <= k + 1 by A47,FINSEQ_1:1;
then
A48: l <= (k + 1) - 1 by XREAL_1:9;
m1 + 2 <= j by A31,A42,A46;
then
A49: m1 + 2 - 1 <= l by XREAL_1:9;
1 <= m1 + 1 by NAT_1:12;
then
A50: 1 <= l by A49,XXREAL_0:2;
g.x = j - 1 by A26,A27,A42,A46;
hence thesis by A28,A43,A50,A48,FINSEQ_1:1;
end;
end;
hence thesis;
end;
set q = q1 ^ q2;
A51: len q2 = m2 by A16,FINSEQ_1:def 3;
then
A52: len q = m1 + m2 by A37,FINSEQ_1:22;
then
A53: dom q = Seg k by A14,A13,FINSEQ_1:def 3;
then reconsider g as Function of dom q, dom q by A28,A26,A41,FUNCT_2:2;
A54: len p = k by A2,A3,A21,FINSEQ_1:17;
A55: rng g = dom q
proof
thus rng g c= dom q;
let y be object;
assume
A56: y in dom q;
then reconsider j = y as Element of NAT;
consider x being object such that
A57: x in dom f and
A58: f.x = y by A5,A22,A53,A56,FUNCT_1:def 3;
reconsider x as Element of NAT by A9,A57;
now
per cases;
suppose
A59: x in dom g;
now
per cases;
suppose
f.x in dom q1;
then g.x = f.x by A26,A27,A59;
hence thesis by A58,A59,FUNCT_1:def 3;
end;
suppose
A60: not f.x in dom q1;
j <= k by A53,A56,FINSEQ_1:1;
then 1 <= j + 1 & j + 1 <= k + 1 by NAT_1:12,XREAL_1:7;
then j + 1 in rng f by A5,FINSEQ_1:1;
then consider x1 being object such that
A61: x1 in dom f and
A62: f.x1 = j + 1 by FUNCT_1:def 3;
A63: now
assume not x1 in dom g;
then x1 in Seg(k + 1) \ Seg k by A4,A26,A61,XBOOLE_0:def 5;
then x1 in {k + 1} by FINSEQ_3:15;
then
A64: j + 1 = m1 +1 by A14,A62,TARSKI:def 1;
1 <= j by A53,A56,FINSEQ_1:1;
hence contradiction by A30,A58,A60,A64,FINSEQ_1:1;
end;
j < 1 or m1 < j by A30,A58,A60,FINSEQ_1:1;
then not j + 1 <= m1 by A53,A56,FINSEQ_1:1,NAT_1:13;
then not f.x1 in dom q1 by A30,A62,FINSEQ_1:1;
then g.x1 = j + 1 - 1 by A26,A27,A62,A63
.= y;
hence thesis by A63,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
suppose
A65: not x in dom g;
j <= k by A53,A56,FINSEQ_1:1;
then 1 <= j + 1 & j + 1 <= k + 1 by NAT_1:12,XREAL_1:7;
then j + 1 in rng f by A5,FINSEQ_1:1;
then consider x1 being object such that
A66: x1 in dom f and
A67: f.x1 = j + 1 by FUNCT_1:def 3;
x in Seg(k + 1) \ Seg k by A4,A26,A57,A65,XBOOLE_0:def 5;
then x in {k + 1} by FINSEQ_3:15;
then
A68: x = k + 1 by TARSKI:def 1;
A69: now
assume not x1 in dom g;
then x1 in Seg(k + 1) \ Seg k by A4,A26,A66,XBOOLE_0:def 5;
then x1 in {k + 1} by FINSEQ_3:15;
then j + 1 = j + 0 by A58,A68,A67,TARSKI:def 1;
hence contradiction;
end;
m1 <= j by A14,A58,A68,XREAL_1:29;
then not j + 1 <= m1 by NAT_1:13;
then not f.x1 in dom q1 by A30,A67,FINSEQ_1:1;
then g.x1 = j + 1 - 1 by A26,A27,A67,A69
.= y;
hence thesis by A69,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
assume
A70: for i st i in dom H2 holds H2.i = H1.(f.i);
then
A71: H2.(k + 1) = H1.(f.(k + 1)) by A7,FINSEQ_1:4;
A72: now
let j be Nat;
assume
A73: j in dom(q1 ^ <* v *>);
A74: now
assume j in Seg m1;
then
A75: j in dom q1 by A2,A29,FINSEQ_1:17;
then q1.j = H1.j by FUNCT_1:47;
hence H1.j = (q1 ^ <* v *>).j by A75,FINSEQ_1:def 7;
end;
A76: now
1 in Seg 1 & len<* v *> = 1 by FINSEQ_1:1,39;
then 1 in dom <* v *> by FINSEQ_1:def 3;
then
A77: (q1 ^ <* v *>).(len q1 + 1) = <* v *>.1 by FINSEQ_1:def 7;
assume j in {n};
then j = n by TARSKI:def 1;
hence (q1 ^ <* v *>).j = H1.j by A71,A14,A37,A77;
end;
len(q1 ^ <* v *>) = m1 + len <* v *> by A37,FINSEQ_1:22
.= m1 + 1 by FINSEQ_1:40;
then j in Seg(m1 + 1) by A73,FINSEQ_1:def 3;
then j in Seg m1 \/ {n} by A14,FINSEQ_1:9;
hence H1.j = (q1 ^ <* v *>).j by A74,A76,XBOOLE_0:def 3;
end;
g is one-to-one
proof
let y1,y2 be object;
assume that
A78: y1 in dom g and
A79: y2 in dom g and
A80: g.y1 = g.y2;
reconsider j1 = y1, j2 = y2 as Element of NAT by A26,A78,A79;
A81: f.y2 in Seg(k + 1) by A9,A5,A22,A26,A79,FUNCT_1:def 3;
A82: f.y1 in Seg(k + 1) by A9,A5,A22,A26,A78,FUNCT_1:def 3;
then reconsider a = f.y1, b = f.y2 as Element of NAT by A81;
now
per cases;
suppose
f.y1 in dom q1 & f.y2 in dom q1;
then g.j1 = f.y1 & g.j2 = f.y2 by A26,A27,A78,A79;
hence thesis by A9,A22,A26,A78,A79,A80,FUNCT_1:def 4;
end;
suppose
A83: f.y1 in dom q1 & not f.y2 in dom q1;
then
A84: a <= m1 by A30,FINSEQ_1:1;
g.j1 = a & g.j2 = b - 1 by A26,A27,A78,A79,A83;
then
A85: (b - 1) + 1 <= m1 + 1 by A80,A84,XREAL_1:6;
1 <= b by A81,FINSEQ_1:1;
then
A86: b in Seg(m1 + 1) by A85,FINSEQ_1:1;
not b in Seg m1 by A2,A29,A83,FINSEQ_1:17;
then b in Seg(m1 + 1) \ Seg m1 by A86,XBOOLE_0:def 5;
then b in {m1 + 1} by FINSEQ_3:15;
then b = m1 + 1 by TARSKI:def 1;
then y2 = k + 1 by A10,A9,A14,A22,A26,A79,FUNCT_1:def 4;
hence thesis by A26,A79,FINSEQ_3:8;
end;
suppose
A87: not f.y1 in dom q1 & f.y2 in dom q1;
then
A88: b <= m1 by A30,FINSEQ_1:1;
g.j1 = a - 1 & g.j2 = b by A26,A27,A78,A79,A87;
then
A89: (a - 1) + 1 <= m1 + 1 by A80,A88,XREAL_1:6;
1 <= a by A82,FINSEQ_1:1;
then
A90: a in Seg(m1 + 1) by A89,FINSEQ_1:1;
not a in Seg m1 by A2,A29,A87,FINSEQ_1:17;
then a in Seg(m1 + 1) \ Seg m1 by A90,XBOOLE_0:def 5;
then a in {m1 + 1} by FINSEQ_3:15;
then a = m1 + 1 by TARSKI:def 1;
then y1 = k + 1 by A10,A9,A14,A22,A26,A78,FUNCT_1:def 4;
hence thesis by A26,A78,FINSEQ_3:8;
end;
suppose
A91: not f.y1 in dom q1 & not f.y2 in dom q1;
then g.j2 = b - 1 by A26,A27,A79;
then
A92: g.y2 = b + (- 1);
g.j1 = a - 1 by A26,A27,A78,A91;
then g.j1 = a + (- 1);
then a = b by A80,A92,XCMPLX_1:2;
hence thesis by A9,A22,A26,A78,A79,FUNCT_1:def 4;
end;
end;
hence thesis;
end;
then reconsider g as Permutation of dom q by A55,FUNCT_2:57;
len(q1 ^ <* v *>) + len q2 = len q1 + len<* v *> + m2 by A51,FINSEQ_1:22
.= k + 1 by A14,A13,A37,FINSEQ_1:40;
then dom H1 = Seg(len(q1 ^ <* v *>) + len q2) by A2,FINSEQ_1:def 3;
then
A93: H1 = q1 ^ <* v *> ^ q2 by A72,A38,FINSEQ_1:def 7;
now
let i;
assume
A94: i in dom p;
then f.i in rng f by A9,A22,A28,FUNCT_1:def 3;
then reconsider j = f.i as Element of NAT by A5;
now
per cases;
suppose
A95: f.i in dom q1;
then
A96: f.i = g.i & H1.(j) = q1.(j) by A28,A27,A94,FUNCT_1:47;
H2.i = p.i & H2.i = H1.(f.i) by A70,A7,A22,A28,A94,FUNCT_1:47;
hence p.i = q.(g.i) by A95,A96,FINSEQ_1:def 7;
end;
suppose
A97: not f.i in dom q1;
then m1 + 2 <= j by A28,A26,A31,A94;
then
A98: m1 + 2 - 1 <= j - 1 by XREAL_1:9;
m1 < m1 + 1 by XREAL_1:29;
then
A99: m1 < j - 1 by A98,XXREAL_0:2;
then m1 < j by XREAL_1:146,XXREAL_0:2;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:20;
A100: not j1 in dom q1 by A30,A99,FINSEQ_1:1;
A101: g.i = j - 1 by A28,A27,A94,A97;
then j - 1 in dom q by A28,A26,A55,A94,FUNCT_1:def 3;
then consider a being Nat such that
A102: a in dom q2 and
A103: j1 = len q1 + a by A100,FINSEQ_1:25;
A104: len<* v *> = 1 by FINSEQ_1:39;
A105: H2.i = p.i & H2.i = H1.(f.i) by A70,A7,A22,A28,A94,FUNCT_1:47;
A106: H1 = q1 ^ (<* v *> ^ q2) by A93,FINSEQ_1:32;
j in dom H1 by A4,A9,A5,A22,A28,A94,FUNCT_1:def 3;
then consider b being Nat such that
A107: b in dom(<* v *> ^ q2) and
A108: j = len q1 + b by A97,A106,FINSEQ_1:25;
A109: H1.j = (<* v *> ^ q2).b by A106,A107,A108,FINSEQ_1:def 7;
A110: b = 1 + a by A103,A108;
q.(j - 1) = q2.a by A102,A103,FINSEQ_1:def 7;
hence p.i = q.(g.i) by A101,A105,A102,A109,A110,A104,FINSEQ_1:def 7;
end;
end;
hence p.i = q.(g.i);
end;
then Sum(p) = Sum(q) by A1,A14,A13,A54,A52;
then Sum(H2) = Sum(q) + Sum<* v *> by A2,A3,A54,A8,RLVECT_1:38,44
.= Sum(q1) + Sum(q2) + Sum<* v *> by RLVECT_1:41
.= Sum(q1) + (Sum<* v *> + Sum(q2)) by RLVECT_1:def 3
.= Sum(q1) + Sum(<* v *> ^ q2) by RLVECT_1:41
.= Sum(q1 ^ (<* v *> ^ q2)) by RLVECT_1:41
.= Sum(H1) by A93,FINSEQ_1:32;
hence Sum(H1) = Sum(H2);
end;
then
A111: for k st P[k] holds P[k+1];
A112: P[0]
proof
let H1,H2 be FinSequence of the carrier of V;
assume that
A113: len H1 = 0 and
A114: len H1 = len H2;
Sum(H1) = 0.V by A113,RLVECT_1:75;
hence thesis by A113,A114,RLVECT_1:75;
end;
for k holds P[k] from NAT_1:sch 2(A112,A111);
hence thesis;
end;
theorem
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, F,G being FinSequence of the carrier of V for f being
Permutation of dom F st G = F * f holds Sum(F) = Sum(G)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, F,G be FinSequence of the carrier of V;
let f be Permutation of dom F;
assume G = F * f;
then len F = len G & for i st i in dom G holds G.i = F.(f.i) by FINSEQ_2:44
,FUNCT_1:12;
hence thesis by Th6;
end;
definition
let V be non empty addLoopStr, T be finite Subset of V;
assume
A1: V is Abelian add-associative right_zeroed;
func Sum(T) -> Element of V means
:Def2:
ex F be FinSequence of the carrier of V st rng F = T & F is one-to-one &
it = Sum(F);
existence
proof
consider p such that
A2: rng p = T and
A3: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of the carrier of V by A2,FINSEQ_1:def 4;
take Sum(p);
take p;
thus thesis by A2,A3;
end;
uniqueness by A1,RLVECT_1:42;
end;
theorem Th8:
for V be Abelian add-associative right_zeroed non empty
addLoopStr holds Sum({}V) = 0.V
proof
let V be Abelian add-associative right_zeroed non empty addLoopStr;
Sum(<*>(the carrier of V)) = 0.V by RLVECT_1:43;
hence thesis by Def2,RELAT_1:38;
end;
theorem
for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v be Element of V holds Sum{v} = v
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v be Element of V;
A1: Sum<* v *> = v by RLVECT_1:44;
rng<* v *> = {v} & <* v *> is one-to-one by FINSEQ_1:39,FINSEQ_3:93;
hence thesis by A1,Def2;
end;
theorem
for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v1,v2 be Element of V holds v1 <> v2 implies Sum{v1,v2}
= v1 + v2
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v1,v2 be Element of V;
assume v1 <> v2;
then
A1: <* v1,v2 *> is one-to-one by FINSEQ_3:94;
rng<* v1,v2 *> = {v1,v2} & Sum<* v1,v2 *> = v1 + v2 by FINSEQ_2:127
,RLVECT_1:45;
hence thesis by A1,Def2;
end;
theorem
for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v1,v2,v3 be Element of V holds v1 <> v2 & v2 <> v3 & v1
<> v3 implies Sum{v1,v2,v3} = v1 + v2 + v3
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, v1,v2,v3 be Element of V;
assume v1 <> v2 & v2 <> v3 & v1 <> v3;
then
A1: <* v1,v2,v3 *> is one-to-one by FINSEQ_3:95;
rng<* v1,v2,v3 *> = {v1,v2,v3} & Sum<* v1,v2,v3 *> = v1 + v2 + v3 by
FINSEQ_2:128,RLVECT_1:46;
hence thesis by A1,Def2;
end;
theorem Th12:
for V be Abelian add-associative right_zeroed non empty
addLoopStr, S,T be finite Subset of V holds T misses S implies Sum(T \/ S) =
Sum(T) + Sum(S)
proof
let V be Abelian add-associative right_zeroed non empty addLoopStr, S,T be
finite Subset of V;
consider F be FinSequence of the carrier of V such that
A1: rng F = T \/ S and
A2: F is one-to-one & Sum(T \/ S) = Sum(F) by Def2;
consider G be FinSequence of the carrier of V such that
A3: rng G = T and
A4: G is one-to-one and
A5: Sum(T) = Sum(G) by Def2;
consider H be FinSequence of the carrier of V such that
A6: rng H = S and
A7: H is one-to-one and
A8: Sum(S) = Sum(H) by Def2;
set I = G ^ H;
assume T misses S;
then
A9: I is one-to-one by A3,A4,A6,A7,FINSEQ_3:91;
rng I = rng F by A1,A3,A6,FINSEQ_1:31;
hence Sum(T \/ S) = Sum(I) by A2,A9,RLVECT_1:42
.= Sum(T) + Sum(S) by A5,A8,RLVECT_1:41;
end;
theorem Th13:
for V be Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, S,T be finite Subset of V holds
Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, S,T be finite Subset of V;
set A = S \ T;
set B = T \ S;
set Z = A \/ B;
set I = T /\ S;
A1: A \/ I = S by XBOOLE_1:51;
A2: B \/ I = T by XBOOLE_1:51;
A3: Z = T \+\ S;
then Z \/ I = T \/ S by XBOOLE_1:93;
then Sum(T \/ S) + Sum(I) = Sum(Z) + Sum(I) + Sum(I) by A3,Th12,XBOOLE_1:103
.= Sum(A) + Sum(B) + Sum(I) + Sum(I) by Th12,XBOOLE_1:82
.= Sum(A) + (Sum(I) + Sum(B)) + Sum(I) by RLVECT_1:def 3
.= (Sum(A) + Sum(I)) + (Sum(B) + Sum(I)) by RLVECT_1:def 3
.= Sum(S) + (Sum(B) + Sum(I)) by A1,Th12,XBOOLE_1:89
.= Sum(T) + Sum(S) by A2,Th12,XBOOLE_1:89;
hence thesis by RLSUB_2:61;
end;
theorem
for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, S,T be finite Subset of V holds Sum(T /\ S) = Sum(T) +
Sum(S) - Sum(T \/ S)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, S,T be finite Subset of V;
Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S) by Th13;
then Sum(T) + Sum(S) = Sum(T /\ S) + Sum(T \/ S) by RLSUB_2:61;
hence thesis by RLSUB_2:61;
end;
theorem Th15:
for V be Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, S,T be finite Subset of V holds
Sum(T \ S) = Sum(T \/ S) - Sum(S)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, S,T be finite Subset of V;
(T \ S) misses S by XBOOLE_1:79;
then
A1: (T \ S) /\ S = {}V;
(T \ S) \/ S = T \/ S by XBOOLE_1:39;
then Sum(T \/ S) = Sum(T \ S) + Sum(S) - Sum((T \ S) /\ S) by Th13;
then Sum(T \/ S) = Sum(T \ S) + Sum(S) - 0.V by A1,Th8
.= Sum(T \ S) + Sum(S);
hence thesis by RLSUB_2:61;
end;
theorem Th16:
for V be Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, S,T be finite Subset of V holds
Sum(T \ S) = Sum(T) - Sum(T /\ S)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, S,T be finite Subset of V;
T \ (T /\ S) = T \ S by XBOOLE_1:47;
then Sum(T \ S) = Sum(T \/ (T /\ S)) - Sum(T /\ S) by Th15;
hence thesis by XBOOLE_1:22;
end;
theorem
for V be Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, S,T be finite Subset of V holds Sum(T \+\ S) = Sum(T \/
S) - Sum(T /\ S)
proof
let V be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr, S,T be finite Subset of V;
T \+\ S = (T \/ S) \ (T /\ S) by XBOOLE_1:101;
hence Sum(T \+\ S) = Sum(T \/ S) - Sum((T \/ S) /\ (T /\ S)) by Th16
.= Sum(T \/ S) - Sum((T \/ S) /\ T /\ S) by XBOOLE_1:16
.= Sum(T \/ S) - Sum(T /\ S) by XBOOLE_1:21;
end;
theorem
for V be Abelian add-associative right_zeroed non empty addLoopStr,
S,T be finite Subset of V holds Sum(T \+\ S) = Sum(T \ S) + Sum(S \ T) by Th12,
XBOOLE_1:82;
reconsider zz=0 as Element of REAL by XREAL_0:def 1;
definition
let V be non empty ZeroStr;
mode Linear_Combination of V -> Element of Funcs(the carrier of V, REAL)
means
:Def3:
ex T being finite Subset of V st for v being Element of V st not v in T
holds it.v = 0;
existence
proof
reconsider f = (the carrier of V) --> zz as
Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
take f,{}V;
thus thesis by FUNCOP_1:7;
end;
end;
reserve K,L,L1,L2,L3 for Linear_Combination of V;
notation
let V be non empty addLoopStr, L be Element of Funcs(the carrier of V, REAL);
synonym Carrier L for support L;
end;
Lm1: now
let V be non empty addLoopStr, L be Element of Funcs(the carrier of V, REAL);
A1: support L c= dom L by PRE_POLY:37;
thus Carrier L c= the carrier of V
proof
let x be object;
assume x in support L;
then x in dom L by A1;
hence thesis;
end;
end;
definition
let V be non empty addLoopStr, L be Element of Funcs(the carrier of V, REAL);
redefine func Carrier(L) -> Subset of V equals :: redefines Carrier (RLVECT_2, synonym) → support (PRE_POLY, definition)
{v where v is Element of V : L.v <> 0};
coherence by Lm1;
compatibility
proof
let X be Subset of V;
set A = Carrier L;
set B = {v where v is Element of V : L.v <> 0};
thus X = A implies X = B
proof
assume
A1: X = A;
thus X c= B
proof
let x be object;
assume
A2: x in X;
then L.x <> 0 by A1,PRE_POLY:def 7;
hence thesis by A2;
end;
let x be object;
assume x in B;
then ex v be Element of V st x = v & L.v <> 0;
hence thesis by A1,PRE_POLY:def 7;
end;
assume
A3: X = B;
thus X c= A
proof
let x be object;
assume x in X;
then ex v be Element of V st x = v & L.v <> 0 by A3;
hence thesis by PRE_POLY:def 7;
end;
let x be object;
assume
A4: x in A;
then
A5: L.x <> 0 by PRE_POLY:def 7;
Carrier L c= the carrier of V by Lm1;
hence thesis by A3,A4,A5;
end;
end;
registration
let V be non empty addLoopStr, L be Linear_Combination of V;
cluster Carrier(L) -> finite;
coherence
proof
set A = Carrier L;
consider T being finite Subset of V such that
A1: for v being Element of V st not v in T holds L.v = 0 by Def3;
A c= T
proof
let x be object;
assume x in A;
then ex v being Element of V st x = v & L.v <> 0;
hence thesis by A1;
end;
hence thesis;
end;
end;
theorem
for V be non empty addLoopStr, L be Linear_Combination of V, v be
Element of V holds L.v = 0 iff not v in Carrier(L)
proof
let V be non empty addLoopStr, L be Linear_Combination of V, v be Element of
V;
thus L.v = 0 implies not v in Carrier(L)
proof
assume
A1: L.v = 0;
assume not thesis;
then ex u be Element of V st u = v & L.u <> 0;
hence thesis by A1;
end;
thus thesis;
end;
definition
let V be non empty addLoopStr;
func ZeroLC(V) -> Linear_Combination of V means
:Def5:
Carrier (it) = {};
existence
proof
reconsider f = (the carrier of V) --> zz as Function of the carrier of V,
REAL;
reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
f is Linear_Combination of V
proof
reconsider T = {}V as empty finite Subset of V;
take T;
thus thesis by FUNCOP_1:7;
end;
then reconsider f as Linear_Combination of V;
take f;
set C = {v where v is Element of V : f.v <> 0};
now
set x = the Element of C;
assume C <> {};
then x in C;
then ex v being Element of V st x = v & f.v <> 0;
hence contradiction by FUNCOP_1:7;
end;
hence thesis;
end;
uniqueness
proof
let L,L9 be Linear_Combination of V;
assume that
A1: Carrier(L) = {} and
A2: Carrier(L9) = {};
now
let x be object;
assume x in the carrier of V;
then reconsider v = x as Element of V;
A3: now
assume L9.v <> 0;
then v in {u where u is Element of V : L9.u <> 0};
hence contradiction by A2;
end;
now
assume L.v <> 0;
then v in {u where u is Element of V : L.u <> 0};
hence contradiction by A1;
end;
hence L.x = L9.x by A3;
end;
hence L = L9;
end;
end;
theorem Th20:
for V be non empty addLoopStr, v be Element of V holds ZeroLC(V) .v = 0
proof
let V be non empty addLoopStr, v be Element of V;
Carrier (ZeroLC(V)) = {} & not v in {} by Def5;
hence thesis;
end;
definition
let V be non empty addLoopStr;
let A be Subset of V;
mode Linear_Combination of A -> Linear_Combination of V means
:Def6:
Carrier (it) c= A;
existence
proof
take L = ZeroLC(V);
Carrier (L) = {} by Def5;
hence thesis;
end;
end;
reserve l,l1,l2 for Linear_Combination of A;
theorem
A c= B implies l is Linear_Combination of B
proof
assume
A1: A c= B;
Carrier(l) c= A by Def6;
then Carrier(l) c= B by A1;
hence thesis by Def6;
end;
theorem Th22:
ZeroLC(V) is Linear_Combination of A
proof
Carrier(ZeroLC(V)) = {} & {} c= A by Def5;
hence thesis by Def6;
end;
theorem Th23:
for l being Linear_Combination of {}the carrier of V holds l = ZeroLC(V)
proof
let l be Linear_Combination of {}(the carrier of V);
Carrier(l) c= {} by Def6;
then Carrier(l) = {};
hence thesis by Def5;
end;
definition
let V;
let F;
let f;
func f (#) F -> FinSequence of the carrier of V means
:Def7:
len it = len F & for i st i in dom it holds it.i = f.(F/.i) * F/.i;
existence
proof
deffunc Q(set)= f.(F/.$1) * F/.$1;
consider G being FinSequence such that
A1: len G = len F and
A2: for n be Nat st n in dom G holds G.n = Q(n) from FINSEQ_1:sch 2;
rng G c= the carrier of V
proof
let x be object;
assume x in rng G;
then consider y being object such that
A3: y in dom G and
A4: G.y = x by FUNCT_1:def 3;
y in Seg(len F) by A1,A3,FINSEQ_1:def 3;
then reconsider y as Element of NAT;
G.y = f.(F/.y) * F/.y by A2,A3;
hence thesis by A4;
end;
then reconsider G as FinSequence of the carrier of V by FINSEQ_1:def 4;
take G;
thus thesis by A1,A2;
end;
uniqueness
proof
let H1,H2;
assume that
A5: len H1 = len F and
A6: for i st i in dom H1 holds H1.i = f.(F/.i) * F/.i and
A7: len H2 = len F and
A8: for i st i in dom H2 holds H2.i = f.(F/.i) * F/.i;
now
let k be Nat;
assume 1 <= k & k <= len H1;
then
A9: k in Seg(len H1) by FINSEQ_1:1;
then k in dom H1 by FINSEQ_1:def 3;
then
A10: H1.k = f.(F/.k) * F/.k by A6;
k in dom H2 by A5,A7,A9,FINSEQ_1:def 3;
hence H1.k = H2.k by A8,A10;
end;
hence thesis by A5,A7,FINSEQ_1:14;
end;
end;
theorem Th24:
i in dom F & v = F.i implies (f (#) F).i = f.v * v
proof
assume that
A1: i in dom F and
A2: v = F.i;
A3: F/.i = F.i by A1,PARTFUN1:def 6;
len(f (#) F) = len F by Def7;
then i in dom(f (#) F) by A1,FINSEQ_3:29;
hence thesis by A2,A3,Def7;
end;
theorem
f (#) <*>(the carrier of V) = <*>(the carrier of V)
proof
len(f (#) <*>(the carrier of V)) = len(<*>(the carrier of V)) by Def7
.= 0;
hence thesis;
end;
theorem Th26:
f (#) <* v *> = <* f.v * v *>
proof
A1: 1 in {1} by TARSKI:def 1;
A2: len(f (#) <* v *>) = len<* v *> by Def7
.= 1 by FINSEQ_1:40;
then dom(f (#) <* v *>) = {1} by FINSEQ_1:2,def 3;
then (f (#) <* v *>).1 = f.(<* v *>/.1) * <* v *>/.1 by A1,Def7
.= f.(<* v *>/.1) * v by FINSEQ_4:16
.= f.v * v by FINSEQ_4:16;
hence thesis by A2,FINSEQ_1:40;
end;
theorem Th27:
f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>
proof
A1: len(f (#) <* v1,v2 *>) = len<* v1,v2 *> by Def7
.= 2 by FINSEQ_1:44;
then
A2: dom(f (#) <* v1,v2 *>) = {1,2} by FINSEQ_1:2,def 3;
2 in {1,2} by TARSKI:def 2;
then
A3: (f (#) <* v1,v2 *>).2 = f.(<* v1,v2 *>/.2) * <* v1,v2 *>/.2 by A2,Def7
.= f.(<* v1,v2 *>/.2) * v2 by FINSEQ_4:17
.= f.v2 * v2 by FINSEQ_4:17;
1 in {1,2} by TARSKI:def 2;
then (f (#) <* v1,v2 *>).1 = f.(<* v1,v2 *>/.1) * <* v1,v2 *>/.1 by A2,Def7
.= f.(<* v1,v2 *>/.1) * v1 by FINSEQ_4:17
.= f.v1 * v1 by FINSEQ_4:17;
hence thesis by A1,A3,FINSEQ_1:44;
end;
theorem
f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *>
proof
A1: len(f (#) <* v1,v2,v3 *>) = len<* v1,v2,v3 *> by Def7
.= 3 by FINSEQ_1:45;
then
A2: dom(f (#) <* v1,v2,v3 *>) = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
3 in {1,2,3} by ENUMSET1:def 1;
then
A3: (f (#) <* v1,v2,v3 *>).3 = f.(<* v1,v2,v3 *>/.3) * <* v1,v2,v3 *>/.3 by A2
,Def7
.= f.(<* v1,v2,v3 *>/.3) * v3 by FINSEQ_4:18
.= f.v3 * v3 by FINSEQ_4:18;
2 in {1,2,3} by ENUMSET1:def 1;
then
A4: (f (#) <* v1,v2,v3 *>).2 = f.(<* v1,v2,v3 *>/.2) * <* v1,v2,v3 *>/.2 by A2
,Def7
.= f.(<* v1,v2,v3 *>/.2) * v2 by FINSEQ_4:18
.= f.v2 * v2 by FINSEQ_4:18;
1 in {1,2,3} by ENUMSET1:def 1;
then
(f (#) <* v1,v2,v3 *>).1 = f.(<* v1,v2,v3 *>/.1) * <* v1,v2,v3 *>/.1 by A2
,Def7
.= f.(<* v1,v2,v3 *>/.1) * v1 by FINSEQ_4:18
.= f.v1 * v1 by FINSEQ_4:18;
hence thesis by A1,A4,A3,FINSEQ_1:45;
end;
definition
let V;
let L;
func Sum(L) -> Element of V means
:Def8:
ex F st F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
existence
proof
consider F being FinSequence such that
A1: rng F = Carrier(L) and
A2: F is one-to-one by FINSEQ_4:58;
reconsider F as FinSequence of the carrier of V by A1,FINSEQ_1:def 4;
take Sum(L (#) F);
take F;
thus F is one-to-one & rng F = Carrier(L) by A1,A2;
thus thesis;
end;
uniqueness
proof
let v1,v2 be Element of V;
given F1 being FinSequence of the carrier of V such that
A3: F1 is one-to-one and
A4: rng F1 = Carrier(L) and
A5: v1 = Sum(L (#) F1);
given F2 being FinSequence of the carrier of V such that
A6: F2 is one-to-one and
A7: rng F2 = Carrier(L) and
A8: v2 = Sum(L (#) F2);
defpred P[object,object] means {$2} = F1 " {F2.$1};
A9: dom F2 = Seg(len F2) by FINSEQ_1:def 3;
A10: dom F1 = Seg(len F1) by FINSEQ_1:def 3;
A11: len F1 = len F2 by A3,A4,A6,A7,FINSEQ_1:48;
A12: for x being object st x in dom F1
ex y being object st y in dom F1 & P[x,y]
proof
let x be object;
assume x in dom F1;
then F2.x in rng F1 by A4,A7,A11,A10,A9,FUNCT_1:def 3;
then consider y being object such that
A13: F1 " {F2.x} = {y} by A3,FUNCT_1:74;
take y;
y in F1 " {F2.x} by A13,TARSKI:def 1;
hence y in dom F1 by FUNCT_1:def 7;
thus thesis by A13;
end;
consider f being Function of dom F1, dom F1 such that
A14: for x being object st x in dom F1 holds P[x,f.x] from FUNCT_2:sch 1(A12);
A15: f is one-to-one
proof
let y1,y2 be object;
assume that
A16: y1 in dom f and
A17: y2 in dom f and
A18: f.y1 = f.y2;
F2.y1 in rng F1 by A4,A7,A11,A10,A9,A16,FUNCT_1:def 3;
then
A19: {F2.y1} c= rng F1 by ZFMISC_1:31;
F2.y2 in rng F1 by A4,A7,A11,A10,A9,A17,FUNCT_1:def 3;
then
A20: {F2.y2} c= rng F1 by ZFMISC_1:31;
F1 " {F2.y1} = {f.y1} & F1 " {F2.y2} = {f.y2} by A14,A16,A17;
then {F2.y1} = {F2.y2} by A18,A19,A20,FUNCT_1:91;
then F2.y1 = F2.y2 by ZFMISC_1:3;
hence thesis by A6,A11,A10,A9,A16,A17;
end;
set G1 = L (#) F1;
A21: len G1 = len F1 by Def7;
A22: rng f = dom F1
proof
thus rng f c= dom F1;
let y be object;
assume
A23: y in dom F1;
then F1.y in rng F2 by A4,A7,FUNCT_1:def 3;
then consider x being object such that
A24: x in dom F2 and
A25: F2.x = F1.y by FUNCT_1:def 3;
F1 " {F2.x} = F1 " Im(F1,y) by A23,A25,FUNCT_1:59;
then F1 " {F2.x} c= {y} by A3,FUNCT_1:82;
then {f.x} c= {y} by A11,A10,A9,A14,A24;
then
A26: f.x = y by ZFMISC_1:18;
x in dom f by A11,A10,A9,A24,FUNCT_2:def 1;
hence thesis by A26,FUNCT_1:def 3;
end;
then reconsider f as Permutation of dom F1 by A15,FUNCT_2:57;
dom F1 = Seg(len F1) & dom G1 = Seg(len G1) by FINSEQ_1:def 3;
then reconsider f as Permutation of dom G1 by A21;
set G2 = L (#) F2;
A27: dom G2 = Seg(len G2) by FINSEQ_1:def 3;
A28: len G2 = len F2 by Def7;
A29: dom(G1) = Seg(len G1) by FINSEQ_1:def 3;
now
let i;
assume
A30: i in dom G2;
then reconsider u = F2.i as VECTOR of V by A28,A9,A27,FUNCT_1:102;
A31: G2.i = L.(F2/.i) * F2/.i & F2.i = F2/.i by A28,A9,A27,A30,Def7,
PARTFUN1:def 6;
i in dom f by A11,A21,A28,A29,A27,A30,FUNCT_2:def 1;
then
A32: f.i in dom F1 by A22,FUNCT_1:def 3;
then reconsider m = f.i as Element of NAT;
reconsider v = F1.m as VECTOR of V by A32,FUNCT_1:102;
{F1.(f.i)} = Im(F1,f.i) by A32,FUNCT_1:59
.= F1 .: (F1 " {F2.i}) by A11,A28,A10,A27,A14,A30;
then
A33: u = v by FUNCT_1:75,ZFMISC_1:18;
F1.m = F1/.m by A32,PARTFUN1:def 6;
hence G2.i = G1.(f.i) by A21,A10,A29,A32,A33,A31,Def7;
end;
hence thesis by A3,A4,A5,A6,A7,A8,A21,A28,Th6,FINSEQ_1:48;
end;
end;
Lm2: Sum(ZeroLC(V)) = 0.V
proof
consider F such that
F is one-to-one and
A1: rng F = Carrier(ZeroLC(V)) and
A2: Sum(ZeroLC(V)) = Sum(ZeroLC(V) (#) F) by Def8;
Carrier(ZeroLC(V)) = {} by Def5;
then F = {} by A1,RELAT_1:41;
then len F = 0;
then len(ZeroLC(V) (#) F) = 0 by Def7;
hence thesis by A2,RLVECT_1:75;
end;
theorem
A <> {} & A is linearly-closed iff for l holds Sum(l) in A
proof
thus A <> {} & A is linearly-closed implies for l holds Sum(l) in A
proof
defpred P[Nat] means
for l st card(Carrier(l)) = $1 holds Sum (l) in A;
assume that
A1: A <> {} and
A2: A is linearly-closed;
now
let l;
assume card(Carrier(l)) = 0;
then Carrier(l) = {};
then l = ZeroLC(V) by Def5;
then Sum(l) = 0.V by Lm2;
hence Sum(l) in A by A1,A2,RLSUB_1:1;
end;
then
A3: P[0];
now
let k;
assume
A4: for l st card(Carrier(l)) = k holds Sum(l) in A;
let l;
deffunc F(Element of V)= l.$1;
consider F such that
A5: F is one-to-one and
A6: rng F = Carrier(l) and
A7: Sum(l) = Sum(l (#) F) by Def8;
reconsider G = F | Seg k as FinSequence of the carrier of V by
FINSEQ_1:18;
assume
A8: card(Carrier(l)) = k + 1;
then
A9: len F = k + 1 by A5,A6,FINSEQ_4:62;
then
A10: len(l (#) F) = k + 1 by Def7;
A11: k + 1 in Seg(k + 1) by FINSEQ_1:4;
then
A12: k + 1 in dom F by A9,FINSEQ_1:def 3;
k+1 in dom F by A9,A11,FINSEQ_1:def 3;
then reconsider v = F.(k + 1) as VECTOR of V by FUNCT_1:102;
consider f being Function of the carrier of V, REAL such that
A13: f.v = In(0,REAL) and
A14: for u being Element of V st u <> v holds f.u = F(u) from
FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
A15: v in Carrier(l) by A6,A12,FUNCT_1:def 3;
now
let u;
assume
A16: not u in Carrier(l);
hence f.u = l.u by A15,A14
.= 0 by A16;
end;
then reconsider f as Linear_Combination of V by Def3;
A17: A \ {v} c= A by XBOOLE_1:36;
A18: Carrier(l) c= A by Def6;
then
A19: l.v * v in A by A2,A15;
A20: Carrier(f) = Carrier(l) \ {v}
proof
thus Carrier(f) c= Carrier(l) \ {v}
proof
let x be object;
assume x in Carrier(f);
then consider u such that
A21: u = x and
A22: f.u <> 0;
f.u = l.u by A13,A14,A22;
then
A23: x in Carrier(l) by A21,A22;
not x in {v} by A13,A21,A22,TARSKI:def 1;
hence thesis by A23,XBOOLE_0:def 5;
end;
let x be object;
assume
A24: x in Carrier(l) \ {v};
then x in Carrier(l) by XBOOLE_0:def 5;
then consider u such that
A25: x = u and
A26: l.u <> 0;
not x in {v} by A24,XBOOLE_0:def 5;
then x <> v by TARSKI:def 1;
then l.u = f.u by A14,A25;
hence thesis by A25,A26;
end;
then Carrier(f) c= A \ {v} by A18,XBOOLE_1:33;
then Carrier(f) c= A by A17;
then reconsider f as Linear_Combination of A by Def6;
A27: len G = k by A9,FINSEQ_3:53;
then
A28: len (f (#) G) = k by Def7;
A29: rng G = Carrier(f)
proof
thus rng G c= Carrier(f)
proof
let x be object;
assume x in rng G;
then consider y being object such that
A30: y in dom G and
A31: G.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A30;
A32: dom G c= dom F & G.y = F.y by A30,FUNCT_1:47,RELAT_1:60;
now
assume x = v;
then
A33: k + 1 = y by A5,A12,A30,A31,A32;
y <= k by A27,A30,FINSEQ_3:25;
hence contradiction by A33,XREAL_1:29;
end;
then
A34: not x in {v} by TARSKI:def 1;
x in rng F by A30,A31,A32,FUNCT_1:def 3;
hence thesis by A6,A20,A34,XBOOLE_0:def 5;
end;
let x be object;
assume
A35: x in Carrier(f);
then x in rng F by A6,A20,XBOOLE_0:def 5;
then consider y being object such that
A36: y in dom F and
A37: F.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A36;
now
assume not y in Seg k;
then y in dom F \ Seg k by A36,XBOOLE_0:def 5;
then y in Seg(k + 1) \ Seg k by A9,FINSEQ_1:def 3;
then y in {k + 1} by FINSEQ_3:15;
then y = k + 1 by TARSKI:def 1;
then not v in {v} by A20,A35,A37,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
then y in dom F /\ Seg k by A36,XBOOLE_0:def 4;
then
A38: y in dom G by RELAT_1:61;
then G.y = F.y by FUNCT_1:47;
hence thesis by A37,A38,FUNCT_1:def 3;
end;
Seg(k + 1) /\ Seg k = Seg k by FINSEQ_1:7,NAT_1:12
.= dom(f (#) G) by A28,FINSEQ_1:def 3;
then
A39: dom(f (#) G) = dom(l (#) F) /\ Seg k by A10,FINSEQ_1:def 3;
now
let x be object;
assume
A40: x in dom(f (#) G);
then reconsider n = x as Element of NAT;
n in dom(l (#) F) by A39,A40,XBOOLE_0:def 4;
then
A41: n in dom F by A9,A10,FINSEQ_3:29;
then F.n in rng F by FUNCT_1:def 3;
then reconsider w = F.n as VECTOR of V;
A42: n in dom G by A27,A28,A40,FINSEQ_3:29;
then
A43: G.n in rng G by FUNCT_1:def 3;
then reconsider u = G.n as VECTOR of V;
not u in {v} by A20,A29,A43,XBOOLE_0:def 5;
then
A44: u <> v by TARSKI:def 1;
A45: (f (#) G).n = f.u * u by A42,Th24
.= l.u * u by A14,A44;
w = u by A42,FUNCT_1:47;
hence (f (#) G).x = (l (#) F).x by A45,A41,Th24;
end;
then
A46: f (#) G = (l (#) F) | Seg k by A39,FUNCT_1:46;
v in rng F by A12,FUNCT_1:def 3;
then {v} c= Carrier(l) by A6,ZFMISC_1:31;
then card(Carrier(f)) = k + 1 - card{v} by A8,A20,CARD_2:44
.= k + 1 - 1 by CARD_1:30
.= k;
then
A47: Sum(f) in A by A4;
G is one-to-one by A5,FUNCT_1:52;
then
A48: Sum(f (#) G) = Sum(f) by A29,Def8;
dom(f (#) G) = Seg len (f (#) G) & (l (#) F).(len F) = l.v * v by A9,A12
,Th24,FINSEQ_1:def 3;
then Sum(l (#) F) = Sum (f (#) G) + l.v * v by A9,A10,A28,A46,RLVECT_1:38
;
hence Sum(l) in A by A2,A7,A19,A48,A47;
end;
then
A49: for k st P[k] holds P[k+1];
let l;
A50: card(Carrier(l)) = card(Carrier(l));
for k holds P[k] from NAT_1:sch 2(A3,A49);
hence thesis by A50;
end;
assume
A51: for l holds Sum(l) in A;
hence A <> {};
ZeroLC(V) is Linear_Combination of A & Sum(ZeroLC(V)) = 0.V by Lm2,Th22;
then
A52: 0.V in A by A51;
A53: for a,v st v in A holds a * v in A
proof
let a,v;
assume
A54: v in A;
now
per cases;
suppose
a = 0;
hence thesis by A52,RLVECT_1:10;
end;
suppose
A55: a <> 0;
deffunc F(Element of V) = zz;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
consider f such that
A56: f.v = aa and
A57: for u being Element of V st u <> v holds f.u = F(u) from
FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
now
let u;
assume not u in {v};
then u <> v by TARSKI:def 1;
hence f.u = 0 by A57;
end;
then reconsider f as Linear_Combination of V by Def3;
A58: Carrier(f) = {v}
proof
thus Carrier(f) c= {v}
proof
let x be object;
assume x in Carrier(f);
then consider u such that
A59: x = u and
A60: f.u <> 0;
u = v by A57,A60;
hence thesis by A59,TARSKI:def 1;
end;
let x be object;
assume x in {v};
then x = v by TARSKI:def 1;
hence thesis by A55,A56;
end;
{v} c= A by A54,ZFMISC_1:31;
then reconsider f as Linear_Combination of A by A58,Def6;
consider F such that
A61: F is one-to-one & rng F = Carrier(f) and
A62: Sum(f (#) F) = Sum(f) by Def8;
F = <* v *> by A58,A61,FINSEQ_3:97;
then f (#) F = <* f.v * v *> by Th26;
then Sum(f) = a * v by A56,A62,RLVECT_1:44;
hence thesis by A51;
end;
end;
hence thesis;
end;
thus for v,u st v in A & u in A holds v + u in A
proof
let v,u;
assume that
A63: v in A and
A64: u in A;
now
per cases;
suppose
u = v;
then v + u = 1 * v + v by RLVECT_1:def 8
.= 1 * v + 1 * v by RLVECT_1:def 8
.= (1 + 1) * v by RLVECT_1:def 6
.= 2 * v;
hence thesis by A53,A63;
end;
suppose
A65: v <> u;
deffunc F(Element of V)=zz;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
consider f such that
A66: f.v = jj & f.u = jj and
A67: for w being Element of V st w <> v & w <> u holds f.w = F(w)
from FUNCT_2:sch 7(A65);
reconsider f as Element of Funcs(the carrier of V, REAL) by FUNCT_2:8;
now
let w;
assume not w in {v,u};
then w <> v & w <> u by TARSKI:def 2;
hence f.w = 0 by A67;
end;
then reconsider f as Linear_Combination of V by Def3;
A68: Carrier(f) = {v,u}
proof
thus Carrier(f) c= {v,u}
proof
let x be object;
assume x in Carrier(f);
then ex w st x = w & f.w <> 0;
then x = v or x = u by A67;
hence thesis by TARSKI:def 2;
end;
let x be object;
assume x in {v,u};
then x = v or x = u by TARSKI:def 2;
hence thesis by A66;
end;
then
A69: Carrier(f) c= A by A63,A64,ZFMISC_1:32;
A70: 1 * u = u & 1 * v = v by RLVECT_1:def 8;
reconsider f as Linear_Combination of A by A69,Def6;
consider F such that
A71: F is one-to-one & rng F = Carrier(f) and
A72: Sum(f (#) F) = Sum(f) by Def8;
F = <* v,u *> or F = <* u,v *> by A65,A68,A71,FINSEQ_3:99;
then f (#) F = <* 1 * v, 1 * u *> or f (#) F = <* 1 * u, 1* v *> by A66
,Th27;
then Sum(f) = v + u by A72,A70,RLVECT_1:45;
hence thesis by A51;
end;
end;
hence thesis;
end;
thus thesis by A53;
end;
theorem
Sum(ZeroLC(V)) = 0.V by Lm2;
theorem
for l being Linear_Combination of {}(the carrier of V) holds Sum(l) = 0.V
proof
let l be Linear_Combination of {}(the carrier of V);
l = ZeroLC(V) by Th23;
hence thesis by Lm2;
end;
theorem Th32:
for l being Linear_Combination of {v} holds Sum(l) = l.v * v
proof
let l be Linear_Combination of {v};
A1: Carrier(l) c= {v} by Def6;
now
per cases by A1,ZFMISC_1:33;
suppose
Carrier(l) = {};
then
A2: l = ZeroLC(V) by Def5;
hence Sum(l) = 0.V by Lm2
.= 0 * v by RLVECT_1:10
.= l.v * v by A2,Th20;
end;
suppose
Carrier(l) = {v};
then consider F such that
A3: F is one-to-one & rng F = {v} and
A4: Sum(l) = Sum(l (#) F) by Def8;
F = <* v *> by A3,FINSEQ_3:97;
then l (#) F = <* l.v * v *> by Th26;
hence thesis by A4,RLVECT_1:44;
end;
end;
hence thesis;
end;
theorem Th33:
v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds
Sum(l) = l.v1 * v1 + l.v2 * v2
proof
assume
A1: v1 <> v2;
let l be Linear_Combination of {v1,v2};
A2: Carrier(l) c= {v1,v2} by Def6;
now
per cases by A2,ZFMISC_1:36;
suppose
Carrier(l) = {};
then
A3: l = ZeroLC(V) by Def5;
hence Sum(l) = 0.V by Lm2
.= 0.V + 0.V
.= 0 * v1 + 0.V by RLVECT_1:10
.= 0 * v1 + 0 * v2 by RLVECT_1:10
.= l.v1 * v1 + 0 * v2 by A3,Th20
.= l.v1 * v1 + l.v2 * v2 by A3,Th20;
end;
suppose
A4: Carrier(l) = {v1};
then reconsider L = l as Linear_Combination of {v1} by Def6;
A5: not v2 in Carrier(l) by A1,A4,TARSKI:def 1;
thus Sum(l) = Sum(L) .= l.v1 * v1 by Th32
.= l.v1 * v1 + 0.V
.= l.v1 * v1 + 0 * v2 by RLVECT_1:10
.= l.v1 * v1 + l.v2 * v2 by A5;
end;
suppose
A6: Carrier(l) = {v2};
then reconsider L = l as Linear_Combination of {v2} by Def6;
A7: not v1 in Carrier(l) by A1,A6,TARSKI:def 1;
thus Sum(l) = Sum(L) .= l.v2 * v2 by Th32
.= 0.V + l.v2 * v2
.= 0 * v1 + l.v2 * v2 by RLVECT_1:10
.= l.v1 * v1 + l.v2 * v2 by A7;
end;
suppose
Carrier(l) = {v1,v2};
then consider F such that
A8: F is one-to-one & rng F = {v1,v2} and
A9: Sum(l) = Sum(l (#) F) by Def8;
F = <* v1,v2 *> or F = <* v2,v1 *> by A1,A8,FINSEQ_3:99;
then l (#) F = <* l.v1 * v1, l.v2 * v2 *> or l (#) F = <* l.v2 * v2, l.
v1 * v1 *> by Th27;
hence thesis by A9,RLVECT_1:45;
end;
end;
hence thesis;
end;
theorem
Carrier(L) = {} implies Sum(L) = 0.V
proof
assume Carrier(L) = {};
then L = ZeroLC(V) by Def5;
hence thesis by Lm2;
end;
theorem
Carrier(L) = {v} implies Sum(L) = L.v * v
proof
assume Carrier(L) = {v};
then L is Linear_Combination of {v} by Def6;
hence thesis by Th32;
end;
theorem
Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = L.v1 * v1 + L.v2 * v2
proof
assume that
A1: Carrier(L) = {v1,v2} and
A2: v1 <> v2;
L is Linear_Combination of {v1,v2} by A1,Def6;
hence thesis by A2,Th33;
end;
definition
let V be non empty addLoopStr;
let L1,L2 be Linear_Combination of V;
redefine pred L1 = L2 means :: redefines = (FUNCT_1, redefinition) → = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
for v being Element of V holds L1.v = L2.v;
compatibility;
end;
definition
let V be non empty addLoopStr;
let L1,L2 be Linear_Combination of V;
redefine func L1 + L2 -> Linear_Combination of V means :: redefines + (VALUED_1, definition)
:Def10:
for v being Element of V holds it.v = L1.v + L2.v;
coherence
proof
reconsider f = L1+L2 as Element of Funcs(the carrier of V,REAL)
by FUNCT_2:8;
now
let v be Element of V;
assume
A1: not v in Carrier(L1) \/ Carrier(L2);
then not v in Carrier(L2) by XBOOLE_0:def 3;
then
A2: L2.v = 0;
not v in Carrier(L1) by A1,XBOOLE_0:def 3;
then L1.v = 0;
hence f.v = 0 + 0 by A2,VALUED_1:1
.= 0;
end;
hence thesis by Def3;
end;
compatibility
proof
let f be Linear_Combination of V;
thus f=L1+L2 implies for v being Element of V holds f.v = L1.v + L2.v by
VALUED_1:1;
assume
A3: for v being Element of V holds f.v = L1.v + L2.v;
thus f = L1+L2
proof
let v be Element of the carrier of V;
thus f.v = L1.v+L2.v by A3
.= (L1+L2).v by VALUED_1:1;
end;
end;
end;
theorem Th37:
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2)
proof
let x be object;
assume x in Carrier(L1 + L2);
then consider u such that
A1: x = u and
A2: (L1 + L2).u <> 0;
(L1 + L2).u = L1.u + L2.u by Def10;
then L1.u <> 0 or L2.u <> 0 by A2;
then x in {v1 : L1.v1 <> 0} or x in {v2 : L2.v2 <> 0} by A1;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th38:
L1 is Linear_Combination of A & L2 is Linear_Combination of A
implies L1 + L2 is Linear_Combination of A
proof
assume L1 is Linear_Combination of A & L2 is Linear_Combination of A;
then Carrier(L1) c= A & Carrier(L2) c= A by Def6;
then
A1: Carrier(L1) \/ Carrier(L2) c= A by XBOOLE_1:8;
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2) by Th37;
hence Carrier(L1 + L2) c= A by A1;
end;
theorem
for V be non empty addLoopStr, L1,L2 be Linear_Combination of V holds
L1 + L2 = L2 + L1;
theorem Th40:
L1 + (L2 + L3) = L1 + L2 + L3
proof
let v;
thus (L1 + (L2 + L3)).v = L1.v + (L2 + L3).v by Def10
.= L1.v + (L2.v + L3.v) by Def10
.= L1.v + L2.v + L3.v
.= (L1 + L2).v + L3.v by Def10
.= (L1 + L2 + L3).v by Def10;
end;
theorem Th41:
L + ZeroLC(V) = L & ZeroLC(V) + L = L
proof
thus L + ZeroLC(V) = L
proof
let v;
thus (L + ZeroLC(V)).v = L.v + ZeroLC(V).v by Def10
.= L.v + 0 by Th20
.= L.v;
end;
hence thesis;
end;
definition
let V;
let a be Real;
let L;
func a * L -> Linear_Combination of V means
:Def11:
for v holds it.v = a * L.v;
existence
proof
deffunc F(Element of V)=In(a * L.$1,REAL);
consider f being Function of the carrier of V, REAL such that
A1: for v being Element of V holds f.v = F(v) from FUNCT_2:sch 4;
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
now
let v;
assume not v in Carrier(L);
then
A2: L.v = 0;
thus f.v = F(v) by A1
.= a * 0 by A2
.= 0;
end;
then reconsider f as Linear_Combination of V by Def3;
take f;
let v;
f.v = F(v) by A1;
hence thesis;
end;
uniqueness
proof
let L1,L2;
assume
A3: for v holds L1.v = a * L.v;
assume
A4: for v holds L2.v = a * L.v;
let v;
thus L1.v = a * L.v by A3
.= L2.v by A4;
end;
end;
theorem Th42:
a <> 0 implies Carrier(a * L) = Carrier(L)
proof
set T = {u : (a * L).u <> 0};
set S = {v : L.v <> 0};
assume
A1: a <> 0;
T = S
proof
thus T c= S
proof
let x be object;
assume x in T;
then consider u such that
A2: x = u and
A3: (a * L).u <> 0;
(a * L).u = a * L.u by Def11;
then L.u <> 0 by A3;
hence thesis by A2;
end;
let x be object;
assume x in S;
then consider v such that
A4: x = v and
A5: L.v <> 0;
(a * L).v = a * L.v by Def11;
then (a * L).v <> 0 by A1,A5,XCMPLX_1:6;
hence thesis by A4;
end;
hence thesis;
end;
theorem Th43:
0 * L = ZeroLC(V)
proof
let v;
thus (0 * L).v = 0 * L.v by Def11
.= ZeroLC(V).v by Th20;
end;
theorem Th44:
L is Linear_Combination of A implies a * L is Linear_Combination of A
proof
assume
A1: L is Linear_Combination of A;
now
per cases;
suppose
a = 0;
then a * L = ZeroLC(V) by Th43;
hence thesis by Th22;
end;
suppose
a <> 0;
then Carrier(a * L) = Carrier(L) by Th42;
hence thesis by A1,Def6;
end;
end;
hence thesis;
end;
theorem Th45:
(a + b) * L = a * L + b * L
proof
let v;
thus ((a + b) * L).v = (a + b) * L.v by Def11
.= a * L.v + b * L.v
.= (a * L).v + b * L.v by Def11
.= (a * L).v + (b * L). v by Def11
.= ((a * L) + (b * L)).v by Def10;
end;
theorem Th46:
a * (L1 + L2) = a * L1 + a * L2
proof
let v;
thus (a * (L1 + L2)).v = a * (L1 + L2).v by Def11
.= a * (L1.v + L2.v) by Def10
.= a * L1.v + a * L2.v
.= (a * L1).v + a * L2.v by Def11
.= (a * L1).v + (a * L2). v by Def11
.= ((a * L1) + (a * L2)).v by Def10;
end;
theorem Th47:
a * (b * L) = (a * b) * L
proof
let v;
thus (a * (b * L)).v = a * (b * L).v by Def11
.= a * (b * L.v) by Def11
.= a * b * L.v
.= ((a * b) * L).v by Def11;
end;
theorem Th48:
1 * L = L
proof
let v;
thus (1 * L).v = 1 * L.v by Def11
.= L.v;
end;
definition
let V,L;
func - L -> Linear_Combination of V equals
(- 1) * L;
correctness;
end;
theorem Th49:
(- L).v = - L.v
proof
thus (- L).v = (- 1) * L.v by Def11
.= - L.v;
end;
theorem
L1 + L2 = ZeroLC(V) implies L2 = - L1
proof
assume
A1: L1 + L2 = ZeroLC(V);
let v;
L1.v + L2.v = ZeroLC(V).v by A1,Def10
.= 0 by Th20;
hence L2.v = - L1.v .= (- L1).v by Th49;
end;
theorem
Carrier(- L) = Carrier(L) by Th42;
theorem
L is Linear_Combination of A implies - L is Linear_Combination of A by Th44;
theorem
- (- L) = L
proof
let v;
thus (- (- L)).v = ((- 1) * (- 1) * L).v by Th47
.= 1 * L.v by Def11
.= L.v;
end;
definition
let V;
let L1,L2;
func L1 - L2 -> Linear_Combination of V equals
L1 + (- L2);
correctness;
end;
theorem Th54:
(L1 - L2).v = L1.v - L2.v
proof
thus (L1 - L2).v = L1.v + (- L2).v by Def10
.= L1.v + (- L2.v) by Th49
.= L1.v - L2.v;
end;
theorem
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2)
proof
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(- L2) by Th37;
hence thesis by Th42;
end;
theorem
L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
L1 - L2 is Linear_Combination of A
proof
assume that
A1: L1 is Linear_Combination of A and
A2: L2 is Linear_Combination of A;
- L2 is Linear_Combination of A by A2,Th44;
hence thesis by A1,Th38;
end;
theorem Th57:
L - L = ZeroLC(V)
proof
let v;
thus (L - L).v = L.v - L.v by Th54
.= ZeroLC(V).v by Th20;
end;
definition
let V;
func LinComb(V) -> set means
:Def14:
x in it iff x is Linear_Combination of V;
existence
proof
defpred P[object] means $1 is Linear_Combination of V;
consider A being set such that
A1: for x being object holds
x in A iff x in Funcs(the carrier of V, REAL) & P[x]
from XBOOLE_0:sch 1;
take A;
let x;
thus x in A implies x is Linear_Combination of V by A1;
assume x is Linear_Combination of V;
hence thesis by A1;
end;
uniqueness
proof
let D1,D2 be set;
assume
A2: for x holds x in D1 iff x is Linear_Combination of V;
assume
A3: for x holds x in D2 iff x is Linear_Combination of V;
thus D1 c= D2
proof
let x be object;
assume x in D1;
then x is Linear_Combination of V by A2;
hence thesis by A3;
end;
let x be object;
assume x in D2;
then x is Linear_Combination of V by A3;
hence thesis by A2;
end;
end;
registration
let V;
cluster LinComb(V) -> non empty;
coherence
proof
set x = the Linear_Combination of V;
x in LinComb V by Def14;
hence thesis;
end;
end;
reserve e,e1,e2 for Element of LinComb(V);
definition
let V;
let e;
func @e -> Linear_Combination of V equals
e;
coherence by Def14;
end;
definition
let V;
let L;
func @L -> Element of LinComb(V) equals
L;
coherence by Def14;
end;
definition
let V;
func LCAdd(V) -> BinOp of LinComb(V) means
:Def17:
for e1,e2 holds it.(e1,e2 ) = @e1 + @e2;
existence
proof
deffunc F(Element of LinComb(V),Element of LinComb(V))=@(@$1 + @$2);
consider o being BinOp of LinComb(V) such that
A1: for e1,e2 holds o.(e1,e2) = F(e1,e2) from BINOP_1:sch 4;
take o;
let e1,e2;
thus o.(e1,e2) = @(@e1 + @e2) by A1
.= @e1 + @e2;
end;
uniqueness
proof
let o1,o2 be BinOp of LinComb(V);
assume
A2: for e1,e2 holds o1.(e1,e2) = @e1 + @e2;
assume
A3: for e1,e2 holds o2.(e1,e2) = @e1 + @e2;
now
let e1,e2;
thus o1.(e1,e2) = @e1 + @e2 by A2
.= o2.(e1,e2) by A3;
end;
hence thesis;
end;
end;
definition
let V;
func LCMult(V) -> Function of [:REAL,LinComb(V):], LinComb(V) means
:Def18:
for a,e holds it.[a,e] = a * @e;
existence
proof
defpred P[Real,Element of LinComb(V),set]
means ex a st a = $1 & $3 = a * @$2;
A1: for x being Element of REAL, e1 ex e2 st P[x,e1,e2]
proof
let x be Element of REAL, e1;
take @(x * @e1);
take x;
thus thesis;
end;
consider g being Function of [:REAL,LinComb(V):], LinComb(V) such that
A2: for x being Element of REAL, e holds P[x,e,g.(x,e)]
from BINOP_1:sch 3 (A1);
take g;
let a,e;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
ex b st b = aa & g.(aa,e) = b * @e by A2;
hence thesis;
end;
uniqueness
proof
let g1,g2 be Function of [:REAL,LinComb(V):], LinComb(V);
assume
A3: for a,e holds g1.[a,e] = a * @e;
assume
A4: for a,e holds g2.[a,e] = a * @e;
now
let x be Element of REAL, e;
thus g1.(x,e) = x * @e by A3
.= g2.(x,e) by A4;
end;
hence thesis;
end;
end;
definition
let V;
func LC_RLSpace V -> RLSStruct equals
RLSStruct (# LinComb(V), @ZeroLC(V),
LCAdd(V), LCMult(V) #);
coherence;
end;
registration
let V;
cluster LC_RLSpace V -> strict non empty;
coherence;
end;
registration
let V;
cluster LC_RLSpace V -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence
proof
set S = LC_RLSpace V;
A1: now
let v,u be (VECTOR of S), K,L;
A2: @@K = K & @@L = L;
assume v = K & u = L;
hence v + u = K + L by A2,Def17;
end;
thus S is Abelian
proof
let u,v be Element of S;
reconsider K = u, L = v as Linear_Combination of V by Def14;
thus u + v = L + K by A1
.= v + u by A1;
end;
thus S is add-associative
proof
let u,v,w be Element of S;
reconsider L = u, K = v, M = w as Linear_Combination of V by Def14;
A3: v + w = K + M by A1;
u + v = L + K by A1;
hence (u + v) + w = L + K + M by A1
.= L + (K + M) by Th40
.= u + (v + w) by A1,A3;
end;
thus S is right_zeroed
proof
let v be Element of S;
reconsider K = v as Linear_Combination of V by Def14;
thus v + 0.S = K + ZeroLC V by A1
.= v by Th41;
end;
thus S is right_complementable
proof
let v be Element of S;
reconsider K = v as Linear_Combination of V by Def14;
- K in the carrier of S by Def14;
then - K in S;
then - K = vector(S,- K) by Def1;
then v + vector(S,- K) = K - K by A1
.= 0.S by Th57;
hence ex w being VECTOR of S st v + w = 0.S;
end;
A4: now
let v be (VECTOR of S), L,a;
A5: @@L = L;
assume v = L;
hence a * v = a * L by A5,Def18;
end;
thus for a being Real for v,w being VECTOR of S holds a * (v + w) =
a * v + a * w
proof
let a be Real;
let v,w be VECTOR of S;
reconsider K = v, M = w as Linear_Combination of V by Def14;
reconsider a as Real;
A6: a * v = a * K & a * w = a * M by A4;
v + w = K + M by A1;
then a * (v + w) = a * (K + M) by A4
.= a * K + a * M by Th46
.= a * v + a * w by A1,A6;
hence thesis;
end;
thus for a,b being Real for v being VECTOR of S holds (a + b) * v =
a * v + b * v
proof
let a,b be Real;
let v be VECTOR of S;
reconsider K = v as Linear_Combination of V by Def14;
reconsider a,b as Real;
A7: a * v = a * K & b * v = b * K by A4;
(a + b) * v = (a + b) * K by A4
.= a * K + b * K by Th45
.= a * v + b * v by A1,A7;
hence thesis;
end;
thus for a,b being Real for v being VECTOR of S holds (a * b) * v =
a * (b * v)
proof
let a,b be Real;
let v be VECTOR of S;
reconsider K = v as Linear_Combination of V by Def14;
reconsider a,b as Real;
A8: b * v = b * K by A4;
(a * b) * v = (a * b) * K by A4
.= a * (b * K) by Th47
.= a * (b * v) by A4,A8;
hence thesis;
end;
let v be VECTOR of S;
reconsider K = v as Linear_Combination of V by Def14;
thus 1 * v = 1 * K by A4
.= v by Th48;
end;
end;
theorem
the carrier of LC_RLSpace(V) = LinComb(V);
theorem
0.LC_RLSpace(V) = ZeroLC(V);
theorem
the addF of LC_RLSpace(V) = LCAdd(V);
theorem
the Mult of LC_RLSpace(V) = LCMult(V);
theorem Th62:
vector(LC_RLSpace(V),L1) + vector(LC_RLSpace(V),L2) = L1 + L2
proof
set v2 = vector(LC_RLSpace(V),L2);
A1: L1 = @@L1 & L2 = @@L2;
L2 in the carrier of LC_RLSpace(V) by Def14;
then
A2: L2 in LC_RLSpace(V);
L1 in the carrier of LC_RLSpace(V) by Def14;
then L1 in LC_RLSpace(V);
hence vector(LC_RLSpace(V),L1) + vector(LC_RLSpace(V),L2) = LCAdd(V).[L1,v2]
by Def1
.= LCAdd(V).(@L1,@L2) by A2,Def1
.= L1 + L2 by A1,Def17;
end;
theorem Th63:
a * vector(LC_RLSpace(V),L) = a * L
proof
A1: @@L = L;
L in the carrier of LC_RLSpace(V) by Def14;
then L in LC_RLSpace(V);
hence a * vector(LC_RLSpace(V),L) = LCMult(V).[a,@L] by Def1
.= a * L by A1,Def18;
end;
theorem Th64:
- vector(LC_RLSpace(V),L) = - L
proof
thus - vector(LC_RLSpace(V),L) = (- 1) * (vector(LC_RLSpace(V),L)) by
RLVECT_1:16
.= - L by Th63;
end;
theorem
vector(LC_RLSpace(V),L1) - vector(LC_RLSpace(V),L2) = L1 - L2
proof
- L2 in LinComb(V) by Def14;
then
A1: - L2 in LC_RLSpace(V);
- vector(LC_RLSpace(V),L2) = - L2 by Th64
.= vector(LC_RLSpace(V),- L2) by A1,Def1;
hence thesis by Th62;
end;
definition
let V;
let A;
func LC_RLSpace(A) -> strict Subspace of LC_RLSpace(V) means
the carrier of it = the set of all l ;
existence
proof
set X = the set of all l ;
X c= the carrier of LC_RLSpace(V)
proof
let x be object;
assume x in X;
then ex l st x = l;
hence thesis by Def14;
end;
then reconsider X as Subset of LC_RLSpace(V);
A1: X is linearly-closed
proof
thus for v,u being VECTOR of LC_RLSpace(V) st v in X & u in X holds v +
u in X
proof
let v,u be VECTOR of LC_RLSpace(V);
assume that
A2: v in X and
A3: u in X;
consider l1 such that
A4: v = l1 by A2;
consider l2 such that
A5: u = l2 by A3;
A6: u = vector(LC_RLSpace(V),l2) by A5,Def1,RLVECT_1:1;
v = vector(LC_RLSpace(V),l1) by A4,Def1,RLVECT_1:1;
then v + u = l1 + l2 by A6,Th62;
then v + u is Linear_Combination of A by Th38;
hence thesis;
end;
let a be Real;
let v be VECTOR of LC_RLSpace(V);
assume v in X;
then consider l such that
A7: v = l;
a * v = a * vector(LC_RLSpace(V),l) by A7,Def1,RLVECT_1:1
.= a * l by Th63;
then a * v is Linear_Combination of A by Th44;
hence thesis;
end;
ZeroLC(V) is Linear_Combination of A by Th22;
then ZeroLC(V) in X;
hence thesis by A1,RLSUB_1:35;
end;
uniqueness by RLSUB_1:30;
end;
reserve x,y for set,
k,n for Nat;
theorem Th66:
for R being add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr,
a being
Element of R for V being Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over R, F,G being
FinSequence of V st len F = len G & for k for v being Element of
V st k in dom F & v = G.k holds F.k = a * v holds Sum(F) = a * Sum(G)
proof
let R be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr,
a be Element of R;
let V be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R, F,G be FinSequence of V;
defpred P[Nat] means
for H,I being FinSequence of
V st len H = len I & len H = $1 & (for k for v be Element of V st k in dom H &
v = I.k holds H.k = a * v) holds Sum(H) = a * Sum(I);
A1: P[n] implies P[n+1]
proof
assume
A2: for H,I being FinSequence of V st len H = len I &
len H = n & for k for v being Element of V st k in dom H & v = I.k holds H.k =
a * v holds Sum(H) = a * Sum(I);
let H,I be FinSequence of V;
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k for v being Element of V st k in dom H & v = I.k holds H.k = a * v;
reconsider p = H | (Seg n),q = I | (Seg n) as FinSequence of V
by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
then
A7: q = I | (dom q) by A3,A4,FINSEQ_1:17;
A8: len p = n by A4,A6,FINSEQ_1:17;
A9: len q = n by A3,A4,A6,FINSEQ_1:17;
A10: now
A11: dom p c= dom H by A4,A6,A8,FINSEQ_3:30;
let k;
let v be Element of V;
assume that
A12: k in dom p and
A13: v = q.k;
dom q = dom p by A8,A9,FINSEQ_3:29;
then I.k = q.k by A12,FUNCT_1:47;
then H.k = a * v by A5,A12,A13,A11;
hence p.k = a * v by A12,FUNCT_1:47;
end;
n + 1 in Seg(n + 1) by FINSEQ_1:4;
then
A14: n + 1 in dom H by A4,FINSEQ_1:def 3;
dom H = dom I by A3,FINSEQ_3:29;
then reconsider v1 = H.(n + 1),v2 = I.(n + 1) as Element of V by A14,
FINSEQ_2:11;
A15: v1 = a * v2 by A5,A14;
p = H | (dom p) by A4,A6,FINSEQ_1:17;
hence Sum(H) = Sum(p) + v1 by A4,A8,RLVECT_1:38
.= a * Sum(q) + a * v2 by A2,A8,A9,A10,A15
.= a * (Sum(q) + v2) by VECTSP_1:def 14
.= a * Sum(I) by A3,A4,A9,A7,RLVECT_1:38;
end;
A16: P[0]
proof
let H,I be FinSequence of V;
assume that
A17: len H = len I and
A18: len H = 0 and
for k for v being Element of V st k in dom H & v = I.k holds H.k = a * v;
H = <*>(the carrier of V) by A18;
then
A19: Sum(H) = 0.V by RLVECT_1:43;
I = <*>(the carrier of V) by A17,A18;
then Sum(I) = 0.V by RLVECT_1:43;
hence thesis by A19,VECTSP_1:14;
end;
for n holds P[n] from NAT_1:sch 2(A16,A1);
hence thesis;
end;
theorem
for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, a being Element
of R for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R, F,G being FinSequence of V
st len F = len G & for k st k in dom F holds G.k = a * F/.k holds Sum(G) =
a * Sum(F)
proof
let R be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr,
a be Element of R;
let V be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R, F,G be FinSequence of V;
assume that
A1: len F = len G and
A2: for k st k in dom F holds G.k = a * F/.k;
now
let k;
let v be Element of V;
assume that
A3: k in dom G and
A4: v = F.k;
A5: k in dom F by A1,A3,FINSEQ_3:29;
then v = F/.k by A4,PARTFUN1:def 6;
hence G.k = a * v by A2,A5;
end;
hence thesis by A1,Th66;
end;
theorem
for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr for V being
Abelian add-associative right_zeroed right_complementable non empty ModuleStr
over R, F,G,H being FinSequence of V st len F = len G & len F =
len H & for k st k in dom F holds H.k = F/.k - G/.k holds Sum(H) = Sum(F) - Sum
(G)
proof
let R be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be Abelian add-associative right_zeroed right_complementable non
empty ModuleStr over R, F,G,H be FinSequence of V;
assume that
A1: len F = len G and
A2: len F = len H and
A3: for k st k in dom F holds H.k = F/.k - G/.k;
deffunc F(Nat) = - G/.$1;
consider I being FinSequence such that
A4: len I = len G and
A5: for k be Nat st k in dom I holds I.k = F(k) from FINSEQ_1:sch 2;
A6: dom I = Seg len G by A4,FINSEQ_1:def 3;
then
A7: for k st k in Seg(len G) holds I.k = F(k) by A5;
rng I c= the carrier of V
proof
let x be object;
assume x in rng I;
then consider y being object such that
A8: y in dom I and
A9: I.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A8;
x = - G/.y by A5,A8,A9;
then reconsider v = x as Element of V;
v in V;
hence thesis;
end;
then reconsider I as FinSequence of V by FINSEQ_1:def 4;
A10: Seg len G = dom G by FINSEQ_1:def 3;
now
let k;
A11: dom F = dom G by A1,FINSEQ_3:29;
assume
A12: k in dom F;
then k in dom I by A1,A4,FINSEQ_3:29;
then
A13: I.k = I/.k by PARTFUN1:def 6;
thus H.k = F/.k - G/.k by A3,A12
.= F/.k + - G/.k
.= F/.k + I/.k by A5,A6,A10,A12,A13,A11;
end;
then
A14: Sum(H) = Sum(F) + Sum(I) by A1,A2,A4,Th2;
Sum(I) = - Sum(G) by A4,A7,A10,Th4;
hence thesis by A14;
end;
theorem
for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, a being Element
of R for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R holds a * Sum(<*>(the carrier of V)) =
0.V
proof
let R be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, a be Element of
R;
let V be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R;
thus a * Sum(<*>(the carrier of V)) = a * 0.V by RLVECT_1:43
.= 0.V by VECTSP_1:14;
end;
theorem
for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr,
a being Element of R
for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R, v,u being Element of V holds a * Sum
<* v,u *> = a * v + a * u
proof
let R be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr,
a be Element of R;
let V be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R, v,u be Element of V;
thus a * Sum<* v,u *> = a * (v + u) by RLVECT_1:45
.= a * v + a * u by VECTSP_1:def 14;
end;
theorem
for R being add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, a being Element
of R for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R, v,u,w being Element of V holds a *
Sum<* v,u,w *> = a * v + a * u + a * w
proof
let R be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, a be Element of
R;
let V be Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over R, v,u,w be Element of V;
thus a * Sum<* v,u,w *> = a * (v + u + w) by RLVECT_1:46
.= a * (v + u) + a * w by VECTSP_1:def 14
.= a * v + a * u + a * w by VECTSP_1:def 14;
end;