:: Linear Combinations in Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 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, ALGSTR_0, BINOP_1,
VECTSP_1, LATTICES, XBOOLE_0, STRUCT_0, FUNCT_1, RLVECT_2, FUNCT_2,
FINSET_1, SUPINF_2, FUNCOP_1, TARSKI, VALUED_1, NAT_1, RELAT_1, PARTFUN1,
XXREAL_0, CARD_1, ORDINAL4, ARYTM_3, CARD_3, MESFUNC1, RLSUB_1, ARYTM_1,
FINSEQ_4;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, FINSET_1, PARTFUN1, FINSEQ_1, RELAT_1, FUNCT_1,
FUNCT_2, FUNCOP_1, NAT_1, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1,
GROUP_1, VECTSP_1, FINSEQ_4, VFUNCT_1, VECTSP_4;
constructors PARTFUN1, DOMAIN_1, FUNCOP_1, XXREAL_0, NAT_1, MEMBERED,
FINSEQ_4, VECTSP_4, RELSET_1, VFUNCT_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, MEMBERED, STRUCT_0,
VECTSP_1, XXREAL_0, CARD_1, FINSEQ_1, XCMPLX_0;
requirements NUMERALS, REAL, BOOLE, SUBSET;
definitions FUNCT_1, TARSKI, VECTSP_4, XBOOLE_0;
equalities XBOOLE_0, RELAT_1;
expansions FUNCT_1, TARSKI, VECTSP_4, XBOOLE_0;
theorems CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4,
FUNCT_1, FUNCT_2, RLVECT_1, RLVECT_2, TARSKI, VECTSP_1, VFUNCT_1,
VECTSP_4, ZFMISC_1, NAT_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1,
GROUP_1, FUNCOP_1, XREAL_1, PARTFUN1, ORDINAL1;
schemes FINSEQ_1, FUNCT_2, NAT_1;
begin
reserve p,q,r for FinSequence,
x,y,y1,y2 for set,
i,k for Element of NAT,
GF for add-associative right_zeroed right_complementable Abelian associative
well-unital distributive non empty doubleLoopStr,
V for Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over GF,
u,v,v1,v2,v3,w for Element of V,
a,b for Element of GF,
F,G ,H for FinSequence of V,
A,B for Subset of V,
f for Function of V, GF;
definition
let GF be non empty ZeroStr;
let V be non empty ModuleStr over GF;
mode Linear_Combination of V ->
Element of Funcs(the carrier of V, the carrier of GF) means
:Def1:
ex T being finite Subset of V st
for v being Element of V st not v in T holds it.v = 0.GF;
existence
proof
reconsider f = (the carrier of V) --> 0.GF as Function of the carrier of V
, the carrier of GF;
reconsider f as Element of Funcs(the carrier of V, the carrier of GF) by
FUNCT_2:8;
take f, {}V;
thus thesis by FUNCOP_1:7;
end;
end;
reserve L,L1,L2,L3 for Linear_Combination of V;
definition
let GF be non empty ZeroStr;
let V be non empty ModuleStr over GF;
let L be Linear_Combination of V;
func Carrier(L) -> finite Subset of V equals
{v where v is Element of V: L.v <> 0.GF};
coherence
proof
set A = {v where v is Element of V: L.v <> 0.GF};
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.GF by Def1;
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.GF;
hence thesis by A1;
end;
hence thesis by XBOOLE_1:1;
end;
end;
theorem
x in Carrier(L) iff ex v st x = v & L.v <> 0.GF;
theorem
L.v = 0.GF iff not v in Carrier(L)
proof
thus L.v = 0.GF implies not v in Carrier(L)
proof
assume
A1: L.v = 0.GF;
assume not thesis;
then ex u st u = v & L.u <> 0.GF;
hence thesis by A1;
end;
assume not v in Carrier(L);
hence thesis;
end;
definition
let GF be non empty ZeroStr;
let V be non empty ModuleStr over GF;
func ZeroLC(V) -> Linear_Combination of V means
:Def3:
Carrier(it) = {};
existence
proof
reconsider f = (the carrier of V) --> 0.GF as Function of the carrier of V
, the carrier of GF;
reconsider f as Element of Funcs(the carrier of V, the carrier of GF) 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.GF};
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.GF;
hence contradiction by FUNCOP_1:7;
end;
hence thesis;
end;
uniqueness
proof
let L,L9 be Linear_Combination of V;
reconsider K=L,K9=L9 as Function of the carrier of V, the carrier of GF;
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.GF;
then v in {u where u is Element of V: L9.u <> 0.GF};
hence contradiction by A2;
end;
now
assume L.v <> 0.GF;
then v in {u where u is Element of V: L.u <> 0.GF};
hence contradiction by A1;
end;
hence K.x = K9.x by A3;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th3:
ZeroLC(V).v = 0.GF
proof
Carrier(ZeroLC(V)) = {} & not v in {} by Def3;
hence thesis;
end;
definition
let GF be non empty ZeroStr;
let V be non empty ModuleStr over GF;
let A be Subset of V;
mode Linear_Combination of A -> Linear_Combination of V means
:Def4:
Carrier (it) c= A;
existence
proof
take L = ZeroLC(V);
Carrier(L) = {} by Def3;
hence thesis;
end;
end;
reserve l 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 Def4;
then Carrier(l) c= B by A1;
hence thesis by Def4;
end;
theorem Th5:
ZeroLC(V) is Linear_Combination of A
proof
Carrier(ZeroLC(V)) = {} & {} c= A by Def3;
hence thesis by Def4;
end;
theorem Th6:
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 Def4;
then Carrier(l) = {};
hence thesis by Def3;
end;
theorem
L is Linear_Combination of Carrier(L) by Def4;
definition
let GF be non empty addLoopStr;
let V be non empty ModuleStr over GF;
let F be FinSequence of the carrier of V;
let f be Function of V, GF;
func f (#) F -> FinSequence of V means
:Def5:
len it = len F & for i be Nat st i in dom it holds it.i = f.(F/.i) * F/.i;
existence
proof
deffunc G(Nat) = 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 = G(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 be FinSequence of the carrier of V;
assume that
A5: len H1 = len F and
A6: for i be Nat st i in dom H1 holds H1.i = f.(F/.i) * F/.i and
A7: len H2 = len F and
A8: for i be Nat 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 Th8:
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 Def5;
then i in dom(f (#) F) by A1,FINSEQ_3:29;
hence thesis by A2,A3,Def5;
end;
theorem
f (#) <*>(the carrier of V) = <*>(the carrier of V)
proof
len(f (#) <*>(the carrier of V)) = len(<*>(the carrier of V)) by Def5
.= 0;
hence thesis;
end;
theorem Th10:
f (#) <* v *> = <* f.v * v *>
proof
A1: 1 in {1} by TARSKI:def 1;
A2: len(f (#) <* v *>) = len<* v *> by Def5
.= 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,Def5
.= f.(<* v *>/.1) * v by FINSEQ_4:16
.= f.v * v by FINSEQ_4:16;
hence thesis by A2,FINSEQ_1:40;
end;
theorem Th11:
f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>
proof
A1: len(f (#) <* v1,v2 *>) = len<* v1,v2 *> by Def5
.= 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,Def5
.= 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,Def5
.= 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 Def5
.= 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
,Def5
.= 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
,Def5
.= 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
,Def5
.= 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;
theorem Th13:
f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
proof
set H = (f (#) F) ^ (f (#) G);
set I = F ^ G;
A1: len F = len(f (#) F) by Def5;
A2: len H = len(f (#) F) + len(f (#) G) by FINSEQ_1:22
.= len F + len(f (#) G) by Def5
.= len F + len G by Def5
.= len I by FINSEQ_1:22;
A3: len G = len(f (#) G) by Def5;
now
let k be Nat;
assume
A4: k in dom H;
now
per cases by A4,FINSEQ_1:25;
suppose
A5: k in dom(f (#) F);
then
A6: k in dom F by A1,FINSEQ_3:29;
then
A7: k in dom(F ^ G) by FINSEQ_3:22;
A8: F/.k = F.k by A6,PARTFUN1:def 6
.= (F ^ G).k by A6,FINSEQ_1:def 7
.= (F ^ G)/.k by A7,PARTFUN1:def 6;
thus H.k = (f (#) F).k by A5,FINSEQ_1:def 7
.= f.(I/.k) * I/.k by A5,A8,Def5;
end;
suppose
A9: ex n be Nat st n in dom(f (#) G) & k = len(f (#) F) + n;
A10: k in dom I by A2,A4,FINSEQ_3:29;
consider n be Nat such that
A11: n in dom(f (#) G) and
A12: k = len(f (#) F) + n by A9;
A13: n in dom G by A3,A11,FINSEQ_3:29;
then
A14: G/.n = G.n by PARTFUN1:def 6
.= (F ^ G).k by A1,A12,A13,FINSEQ_1:def 7
.= (F ^ G)/.k by A10,PARTFUN1:def 6;
thus H.k = (f (#) G).n by A11,A12,FINSEQ_1:def 7
.= f.(I/.k) * I/.k by A11,A14,Def5;
end;
end;
hence H.k = f.(I/.k) * I/.k;
end;
hence thesis by A2,Def5;
end;
definition
let GF be non empty addLoopStr;
let V be non empty ModuleStr over GF;
let L be Linear_Combination of V;
assume
A1: V is Abelian add-associative right_zeroed right_complementable;
func Sum(L) -> Element of V means
:Def6:
ex F being FinSequence of the carrier of V st
F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
existence
proof
consider F being FinSequence such that
A2: rng F = Carrier(L) and
A3: F is one-to-one by FINSEQ_4:58;
reconsider F as FinSequence of the carrier of V by A2,FINSEQ_1:def 4;
take Sum(L (#) F), F;
thus F is one-to-one & rng F = Carrier(L) by A2,A3;
thus thesis;
end;
uniqueness
proof
let v1,v2 be Element of V;
given F1 being FinSequence of the carrier of V such that
A4: F1 is one-to-one and
A5: rng F1 = Carrier(L) and
A6: v1 = Sum(L (#) F1);
given F2 being FinSequence of the carrier of V such that
A7: F2 is one-to-one and
A8: rng F2 = Carrier(L) and
A9: v2 = Sum(L (#) F2);
defpred P[object, object] means {$2} = F1 " {F2.$1};
A10: len F1 = len F2 by A4,A5,A7,A8,FINSEQ_1:48;
A11: dom F1 = Seg(len F1) by FINSEQ_1:def 3;
A12: dom F2 = Seg(len F2) by FINSEQ_1:def 3;
A13: 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 A5,A8,A10,A11,A12,FUNCT_1:def 3;
then consider y being object such that
A14: F1 " {F2.x} = {y} by A4,FUNCT_1:74;
take y;
y in F1 " {F2.x} by A14,TARSKI:def 1;
hence y in dom F1 by FUNCT_1:def 7;
thus thesis by A14;
end;
consider f being Function of dom F1, dom F1 such that
A15: for x being object st x in dom F1 holds P[x,f.x] from FUNCT_2:sch 1(A13);
A16: rng f = dom F1
proof
thus rng f c= dom F1 by RELAT_1:def 19;
let y be object;
assume
A17: y in dom F1;
then F1.y in rng F2 by A5,A8,FUNCT_1:def 3;
then consider x being object such that
A18: x in dom F2 and
A19: F2.x = F1.y by FUNCT_1:def 3;
F1 " {F2.x} = F1 " Im(F1,y) by A17,A19,FUNCT_1:59;
then F1 " {F2.x} c= {y} by A4,FUNCT_1:82;
then {f.x} c= {y} by A10,A11,A12,A15,A18;
then
A20: f.x = y by ZFMISC_1:18;
x in dom f by A10,A11,A12,A18,FUNCT_2:def 1;
hence thesis by A20,FUNCT_1:def 3;
end;
reconsider G1 = L (#) F1 as FinSequence of V;
A21: len G1 = len F1 by Def5;
A22: f is one-to-one
proof
let y1,y2 be object;
assume that
A23: y1 in dom f and
A24: y2 in dom f and
A25: f.y1 = f.y2;
dom F1 = dom f by FUNCT_2:52;
then
A26: dom F1 <> {} by A23;
A27: y2 in dom F1 by A26,A24,FUNCT_2:def 1;
then
A28: F1 " {F2.y2} = {f.y2} by A15;
A29: y1 in dom F1 by A26,A23,FUNCT_2:def 1;
then F2.y1 in rng F1 by A5,A8,A10,A11,A12,FUNCT_1:def 3;
then
A30: {F2.y1} c= rng F1 by ZFMISC_1:31;
F2.y2 in rng F1 by A5,A8,A10,A11,A12,A27,FUNCT_1:def 3;
then
A31: {F2.y2} c= rng F1 by ZFMISC_1:31;
F1 " {F2.y1} = {f.y1} by A15,A29;
then {F2.y1} = {F2.y2} by A25,A28,A30,A31,FUNCT_1:91;
then
A32: F2.y1 = F2.y2 by ZFMISC_1:3;
y1 in dom F2 & y2 in dom F2 by A10,A11,A12,A26,A23,A24,FUNCT_2:def 1;
hence thesis by A7,A32;
end;
set G2 = L (#) F2;
A33: dom G2 = Seg(len G2) by FINSEQ_1:def 3;
reconsider f as Permutation of dom F1 by A16,A22,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;
A34: len G2 = len F2 by Def5;
A35: dom(G1) = Seg(len G1) by FINSEQ_1:def 3;
now
let i be Nat;
assume
A36: i in dom G2;
then
A37: G2.i = L.(F2/.i) * F2/.i & F2.i = F2/.i by A34,A12,A33,Def5,
PARTFUN1:def 6;
i in dom F2 by A34,A36,FINSEQ_3:29;
then reconsider u = F2.i as Element of V by FINSEQ_2:11;
i in dom f by A10,A21,A34,A35,A33,A36,FUNCT_2:def 1;
then
A38: f.i in dom F1 by A16,FUNCT_1:def 3;
then reconsider m = f.i as Element of NAT by A11;
reconsider v = F1.m as Element of V by A38,FINSEQ_2:11;
{F1.(f.i)} = Im(F1,f.i) by A38,FUNCT_1:59
.= F1 .: (F1 " {F2.i}) by A10,A34,A11,A33,A15,A36;
then
A39: u = v by FUNCT_1:75,ZFMISC_1:18;
F1.m = F1/.m by A38,PARTFUN1:def 6;
hence G2.i = G1.(f.i) by A21,A11,A35,A38,A39,A37,Def5;
end;
hence thesis by A1,A4,A5,A6,A7,A8,A9,A21,A34,FINSEQ_1:48,RLVECT_2:6;
end;
end;
Lm1: 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 Def6;
Carrier(ZeroLC(V)) = {} by Def3;
then F = {} by A1,RELAT_1:41;
then len F = 0;
then len(ZeroLC(V) (#) F) = 0 by Def5;
hence thesis by A2,RLVECT_1:75;
end;
theorem
0.GF <> 1.GF implies (A <> {} & A is linearly-closed iff for l holds
Sum(l) in A)
proof
assume
A1: 0.GF <> 1.GF;
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
A2: A <> {} and
A3: A is linearly-closed;
A4: P[0]
proof
let l;
assume card(Carrier(l)) = 0;
then Carrier(l) = {};
then l = ZeroLC(V) by Def3;
then Sum(l) = 0.V by Lm1;
hence thesis by A2,A3,VECTSP_4:1;
end;
A5: for k being Nat st P[k] holds P[k+1]
proof let k be Nat;
assume
A6: P[k];
let l;
deffunc F(Element of V) = l.$1;
consider F such that
A7: F is one-to-one and
A8: rng F = Carrier(l) and
A9: Sum(l) = Sum(l (#) F) by Def6;
reconsider G = F | Seg k as FinSequence of the carrier of V by
FINSEQ_1:18;
assume
A10: card(Carrier(l)) = k + 1;
then
A11: len F = k + 1 by A7,A8,FINSEQ_4:62;
then
A12: len(l (#) F) = k + 1 by Def5;
A13: k + 1 in Seg(k + 1) by FINSEQ_1:4;
then
A14: k + 1 in dom F by A11,FINSEQ_1:def 3;
k + 1 in dom F by A11,A13,FINSEQ_1:def 3;
then reconsider v = F.(k + 1) as Element of V by FINSEQ_2:11;
consider f being Function of the carrier of V, the carrier of GF such
that
A15: f.v = 0.GF and
A16: 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, the carrier of GF) by
FUNCT_2:8;
A17: v in Carrier(l) by A8,A14,FUNCT_1:def 3;
now
let u;
assume
A18: not u in Carrier(l);
hence f.u = l.u by A17,A16
.= 0.GF by A18;
end;
then reconsider f as Linear_Combination of V by Def1;
A19: A \ {v} c= A by XBOOLE_1:36;
A20: Carrier(l) c= A by Def4;
then
A21: l.v * v in A by A3,A17;
A22: 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
A23: u = x and
A24: f.u <> 0.GF;
f.u = l.u by A15,A16,A24;
then
A25: x in Carrier(l) by A23,A24;
not x in {v} by A15,A23,A24,TARSKI:def 1;
hence thesis by A25,XBOOLE_0:def 5;
end;
let x be object;
assume
A26: x in Carrier(l) \ {v};
then x in Carrier(l) by XBOOLE_0:def 5;
then consider u such that
A27: x = u and
A28: l.u <> 0.GF;
not x in {v} by A26,XBOOLE_0:def 5;
then x <> v by TARSKI:def 1;
then l.u = f.u by A16,A27;
hence thesis by A27,A28;
end;
then Carrier(f) c= A \ {v} by A20,XBOOLE_1:33;
then Carrier(f) c= A by A19;
then reconsider f as Linear_Combination of A by Def4;
A29: len G = k by A11,FINSEQ_3:53;
then
A30: len (f (#) G) = k by Def5;
A31: 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
A32: y in dom G and
A33: G.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A32,FINSEQ_3:23;
A34: dom G c= dom F & G.y = F.y by A32,FUNCT_1:47,RELAT_1:60;
now
assume x = v;
then
A35: k + 1 = y by A7,A14,A32,A33,A34;
A36: k in NAT by ORDINAL1:def 12;
y <= k by A29,A32,FINSEQ_3:25;
hence contradiction by A35,XREAL_1:29,A36;
end;
then
A37: not x in {v} by TARSKI:def 1;
x in rng F by A32,A33,A34,FUNCT_1:def 3;
hence thesis by A8,A22,A37,XBOOLE_0:def 5;
end;
let x be object;
assume
A38: x in Carrier(f);
then x in rng F by A8,A22,XBOOLE_0:def 5;
then consider y being object such that
A39: y in dom F and
A40: F.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A39,FINSEQ_3:23;
now
assume not y in Seg k;
then y in dom F \ Seg k by A39,XBOOLE_0:def 5;
then y in Seg(k + 1) \ Seg k by A11,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 A22,A38,A40,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
then y in dom F /\ Seg k by A39,XBOOLE_0:def 4;
then
A41: y in dom G by RELAT_1:61;
then G.y = F.y by FUNCT_1:47;
hence thesis by A40,A41,FUNCT_1:def 3;
end;
Seg(k + 1) /\ Seg k = Seg k by FINSEQ_1:7,NAT_1:12
.= dom(f (#) G) by A30,FINSEQ_1:def 3;
then
A42: dom(f (#) G) = dom(l (#) F) /\ Seg k by A12,FINSEQ_1:def 3;
now
let x be object;
A43: rng F c= the carrier of V by FINSEQ_1:def 4;
assume
A44: x in dom(f (#) G);
then reconsider n = x as Element of NAT by FINSEQ_3:23;
n in dom(l (#) F) by A42,A44,XBOOLE_0:def 4;
then
A45: n in dom F by A11,A12,FINSEQ_3:29;
then F.n in rng F by FUNCT_1:def 3;
then reconsider w = F.n as Element of V by A43;
A46: n in dom G by A29,A30,A44,FINSEQ_3:29;
then
A47: G.n in rng G by FUNCT_1:def 3;
rng G c= the carrier of V by FINSEQ_1:def 4;
then reconsider u = G.n as Element of V by A47;
not u in {v} by A22,A31,A47,XBOOLE_0:def 5;
then
A48: u <> v by TARSKI:def 1;
A49: (f (#) G).n = f.u * u by A46,Th8
.= l.u * u by A16,A48;
w = u by A46,FUNCT_1:47;
hence (f (#) G).x = (l (#) F).x by A49,A45,Th8;
end;
then f (#) G = (l (#) F) | Seg k by A42,FUNCT_1:46;
then
A50: f (#) G = (l (#) F) | dom (f (#) G) by A30,FINSEQ_1:def 3;
v in rng F by A14,FUNCT_1:def 3;
then {v} c= Carrier(l) by A8,ZFMISC_1:31;
then card(Carrier(f)) = k + 1 - card{v} by A10,A22,CARD_2:44
.= k + 1 - 1 by CARD_1:30
.= k by XCMPLX_1:26;
then
A51: Sum(f) in A by A6;
G is one-to-one by A7,FUNCT_1:52;
then
A52: Sum(f (#) G) = Sum(f) by A31,Def6;
(l (#) F).(len F) = l.v * v by A11,A14,Th8;
then Sum(l (#) F) = Sum (f (#) G) + l.v * v by A11,A12,A30,A50,
RLVECT_1:38;
hence thesis by A3,A9,A21,A52,A51;
end;
let l;
A53: card(Carrier(l)) = card(Carrier(l));
for k being Nat holds P[k] from NAT_1:sch 2(A4,A5);
hence thesis by A53;
end;
assume
A54: for l holds Sum(l) in A;
hence A <> {};
ZeroLC(V) is Linear_Combination of A & Sum(ZeroLC(V)) = 0.V by Lm1,Th5;
then
A55: 0.V in A by A54;
A56: for a,v st v in A holds a * v in A
proof
let a,v;
assume
A57: v in A;
now
per cases;
suppose
a = 0.GF;
hence thesis by A55,VECTSP_1:14;
end;
suppose
A58: a <> 0.GF;
deffunc F(set) = 0.GF;
consider f such that
A59: f.v = a and
A60: 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, the carrier of GF)
by FUNCT_2:8;
now
let u;
assume not u in {v};
then u <> v by TARSKI:def 1;
hence f.u = 0.GF by A60;
end;
then reconsider f as Linear_Combination of V by Def1;
A61: Carrier(f) = {v}
proof
thus Carrier(f) c= {v}
proof
let x be object;
assume x in Carrier(f);
then consider u such that
A62: x = u and
A63: f.u <> 0.GF;
u = v by A60,A63;
hence thesis by A62,TARSKI:def 1;
end;
let x be object;
assume x in {v};
then x = v by TARSKI:def 1;
hence thesis by A58,A59;
end;
{v} c= A by A57,ZFMISC_1:31;
then reconsider f as Linear_Combination of A by A61,Def4;
consider F such that
A64: F is one-to-one & rng F = Carrier(f) and
A65: Sum(f (#) F) = Sum(f) by Def6;
F = <* v *> by A61,A64,FINSEQ_3:97;
then f (#) F = <* f.v * v *> by Th10;
then Sum(f) = a * v by A59,A65,RLVECT_1:44;
hence thesis by A54;
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
A66: v in A and
A67: u in A;
now
per cases;
suppose
u = v;
then v + u = 1.GF * v + v
.= 1.GF * v + 1.GF * v
.= (1.GF + 1.GF) * v by VECTSP_1:def 15;
hence thesis by A56,A66;
end;
suppose
A68: v <> u;
deffunc F(set) = 0.GF;
consider f such that
A69: f.v = 1.GF & f.u = 1.GF and
A70: for w being Element of V st w <> v & w <> u holds f.w = F(w)
from FUNCT_2:sch 7(A68);
reconsider f as Element of Funcs(the carrier of V, the carrier of GF)
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.GF by A70;
end;
then reconsider f as Linear_Combination of V by Def1;
A71: 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.GF;
then x = v or x = u by A70;
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 A1,A69;
end;
then
A72: Carrier(f) c= A by A66,A67,ZFMISC_1:32;
reconsider f as Linear_Combination of A by A72,Def4;
consider F such that
A74: F is one-to-one & rng F = Carrier(f) and
A75: Sum(f (#) F) = Sum(f) by Def6;
F = <* v,u *> or F = <* u,v *> by A68,A71,A74,FINSEQ_3:99;
then f (#) F = <* 1.GF * v, 1.GF * u *> or f (#) F = <* 1.GF * u, 1.
GF * v *> by A69,Th11;
then Sum(f) = v + u by A75,RLVECT_1:45;
hence thesis by A54;
end;
end;
hence thesis;
end;
thus thesis by A56;
end;
theorem
Sum(ZeroLC(V)) = 0.V by Lm1;
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 Th6;
hence thesis by Lm1;
end;
theorem Th17:
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 Def4;
now
per cases by A1,ZFMISC_1:33;
suppose
Carrier(l) = {};
then
A2: l = ZeroLC(V) by Def3;
hence Sum(l) = 0.V by Lm1
.= 0.GF * v by VECTSP_1:14
.= l.v * v by A2,Th3;
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 Def6;
F = <* v *> by A3,FINSEQ_3:97;
then l (#) F = <* l.v * v *> by Th10;
hence thesis by A4,RLVECT_1:44;
end;
end;
hence thesis;
end;
theorem Th18:
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 Def4;
now
per cases by A2,ZFMISC_1:36;
suppose
Carrier(l) = {};
then
A3: l = ZeroLC(V) by Def3;
hence Sum(l) = 0.V by Lm1
.= 0.V + 0.V by RLVECT_1:4
.= 0.GF * v1 + 0.V by VECTSP_1:14
.= 0.GF * v1 + 0.GF * v2 by VECTSP_1:14
.= l.v1 * v1 + 0.GF * v2 by A3,Th3
.= l.v1 * v1 + l.v2 * v2 by A3,Th3;
end;
suppose
A4: Carrier(l) = {v1};
then reconsider L = l as Linear_Combination of {v1} by Def4;
A5: not v2 in Carrier(l) by A1,A4,TARSKI:def 1;
thus Sum(l) = Sum(L) .= l.v1 * v1 by Th17
.= l.v1 * v1 + 0.V by RLVECT_1:4
.= l.v1 * v1 + 0.GF * v2 by VECTSP_1:14
.= l.v1 * v1 + l.v2 * v2 by A5;
end;
suppose
A6: Carrier(l) = {v2};
then reconsider L = l as Linear_Combination of {v2} by Def4;
A7: not v1 in Carrier(l) by A1,A6,TARSKI:def 1;
thus Sum(l) = Sum(L) .= l.v2 * v2 by Th17
.= 0.V + l.v2 * v2 by RLVECT_1:4
.= 0.GF * v1 + l.v2 * v2 by VECTSP_1:14
.= 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 Def6;
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 Th11;
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 Def3;
hence thesis by Lm1;
end;
theorem
Carrier(L) = {v} implies Sum(L) = L.v * v
proof
assume Carrier(L) = {v};
then L is Linear_Combination of {v} by Def4;
hence thesis by Th17;
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,Def4;
hence thesis by A2,Th18;
end;
definition
let GF be non empty ZeroStr;
let V be non empty ModuleStr over GF;
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 by FUNCT_2:63;
end;
definition
let GF,V,L1,L2;
func L1 + L2 -> Linear_Combination of V equals
L1 + L2;
coherence
proof
set f = L1+L2;
A1: dom L1 = the carrier of V & dom L2 = the carrier of V by FUNCT_2:def 1;
A2: dom f = dom L1 /\ dom L2 by VFUNCT_1:def 1;
then f is Function of V,GF by A1,FUNCT_2:67;
then
A3: f is Element of Funcs(the carrier of V,the carrier of GF) by FUNCT_2:8;
now
let v;
assume
A4: not v in Carrier(L1) \/ Carrier(L2);
then not v in Carrier(L2) by XBOOLE_0:def 3;
then
A5: L2.v = 0.GF;
A6: L1/.v = L1.v & L2/.v = L2.v by A1,PARTFUN1:def 6;
not v in Carrier(L1) by A4,XBOOLE_0:def 3;
then
A7: L1.v = 0.GF;
thus f.v = f/.v by A1,A2,PARTFUN1:def 6
.= 0.GF + 0.GF by A1,A2,A5,A6,A7,VFUNCT_1:def 1
.= 0.GF by RLVECT_1:4;
end;
hence thesis by A3,Def1;
end;
end;
theorem Th22:
(L1+L2).v = L1.v + L2.v
proof
dom L1 = the carrier of V & dom L2 = the carrier of V by FUNCT_2:def 1;
then
A1: L1/.v = L1.v & L2/.v = L2.v by PARTFUN1:def 6;
A2: dom (L1+L2) = the carrier of V by FUNCT_2:def 1;
hence (L1+L2).v = (L1+L2)/.v by PARTFUN1:def 6
.= L1.v + L2.v by A1,A2,VFUNCT_1:def 1;
end;
theorem Th23:
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.GF;
(L1 + L2).u = L1.u + L2.u by Th22;
then L1.u <> 0.GF or L2.u <> 0.GF by A2,RLVECT_1:4;
then x in {v1 : L1.v1 <> 0.GF} or x in {v2 : L2.v2 <> 0.GF} by A1;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th24:
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 Def4;
then
A1: Carrier(L1) \/ Carrier(L2) c= A by XBOOLE_1:8;
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2) by Th23;
hence Carrier(L1 + L2) c= A by A1;
end;
theorem
L1 + L2 = L2 + L1;
theorem
L1 + (L2 + L3) = L1 + L2 + L3
proof
let v;
thus (L1 + (L2 + L3)).v = L1.v + (L2 + L3).v by Th22
.= L1.v + (L2.v + L3.v) by Th22
.= L1.v + L2.v + L3.v by RLVECT_1:def 3
.= (L1 + L2).v + L3.v by Th22
.= (L1 + L2 + L3).v by Th22;
end;
theorem
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 Th22
.= L.v + 0.GF by Th3
.= L.v by RLVECT_1:4;
end;
hence thesis;
end;
definition
let GF,V,a,L;
func a * L -> Linear_Combination of V means
:Def9:
for v holds it.v = a * L .v;
existence
proof
deffunc F(Element of V) = a*L.$1;
consider f being Function of the carrier of V, the carrier of GF 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,the carrier of GF) by
FUNCT_2:8;
now
let v;
assume not v in Carrier(L);
then L.v = 0.GF;
hence f.v = a * 0.GF by A1
.= 0.GF;
end;
then reconsider f as Linear_Combination of V by Def1;
take f;
let v;
thus thesis by A1;
end;
uniqueness
proof
let L1,L2;
assume
A2: for v holds L1.v = a * L.v;
assume
A3: for v holds L2.v = a * L.v;
let v;
thus L1.v = a * L.v by A2
.= L2.v by A3;
end;
end;
theorem Th28:
Carrier(a * L) c= Carrier(L)
proof
set T = {u : (a * L).u <> 0.GF};
set S = {v : L.v <> 0.GF};
T c= S
proof
let x be object;
assume x in T;
then consider u such that
A1: x = u and
A2: (a * L).u <> 0.GF;
(a * L).u = a * L.u by Def9;
then L.u <> 0.GF by A2;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th29:
for GF being Field, V being VectSp of GF, a being Element of GF,
L being Linear_Combination of V st a <> 0.GF holds Carrier(a * L) = Carrier(L)
proof
let GF be Field, V be VectSp of GF, a be Element of GF, L be
Linear_Combination of V;
set T = {u where u is Vector of V : (a * L).u <> 0.GF};
set S = {v where v is Vector of V : L.v <> 0.GF};
assume
A1: a <> 0.GF;
T = S
proof
thus T c= S
proof
let x be object;
assume x in T;
then consider u being Vector of V such that
A2: x = u and
A3: (a * L).u <> 0.GF;
(a * L).u = a * L.u by Def9;
then L.u <> 0.GF by A3;
hence thesis by A2;
end;
let x be object;
assume x in S;
then consider v being Vector of V such that
A4: x = v and
A5: L.v <> 0.GF;
(a * L).v = a * L.v by Def9;
then (a * L).v <> 0.GF by A1,A5,VECTSP_1:12;
hence thesis by A4;
end;
hence thesis;
end;
theorem Th30:
0.GF * L = ZeroLC(V)
proof
let v;
thus (0.GF * L).v = 0.GF * L.v by Def9
.= 0.GF
.= ZeroLC(V).v by Th3;
end;
theorem Th31:
L is Linear_Combination of A implies a * L is Linear_Combination of A
proof
assume L is Linear_Combination of A;
then
A1: Carrier(L) c= A by Def4;
Carrier(a * L) c= Carrier(L) by Th28;
then Carrier(a * L) c= A by A1;
hence thesis by Def4;
end;
theorem
(a + b) * L = a * L + b * L
proof
let v;
thus ((a + b) * L).v = (a + b) * L.v by Def9
.= a * L.v + b * L.v by VECTSP_1:def 7
.= (a * L).v + b * L.v by Def9
.= (a * L).v + (b * L). v by Def9
.= ((a * L) + (b * L)).v by Th22;
end;
theorem
a * (L1 + L2) = a * L1 + a * L2
proof
let v;
thus (a * (L1 + L2)).v = a * (L1 + L2).v by Def9
.= a * (L1.v + L2.v) by Th22
.= a * L1.v + a * L2.v by VECTSP_1:def 7
.= (a * L1).v + a * L2.v by Def9
.= (a * L1).v + (a * L2). v by Def9
.= ((a * L1) + (a * L2)).v by Th22;
end;
theorem Th34:
a * (b * L) = (a * b) * L
proof
let v;
thus (a * (b * L)).v = a * (b * L).v by Def9
.= a * (b * L.v) by Def9
.= a * b * L.v by GROUP_1:def 3
.= ((a * b) * L).v by Def9;
end;
theorem
1.GF * L = L
proof
let v;
thus (1.GF * L).v = 1.GF * L.v by Def9
.= L.v;
end;
definition
let GF,V,L;
func - L -> Linear_Combination of V equals
(- 1.GF) * L;
correctness;
involutiveness
proof
let L, L9 be Linear_Combination of V;
assume
A1: L = (- 1.GF) * L9;
let v;
thus L9.v = (1.GF) * L9.v
.= ((1.GF) * (1.GF)) * L9.v
.= ((- 1.GF) * (- 1.GF)) * L9.v by VECTSP_1:10
.= (((- 1.GF) * (- 1.GF)) * L9).v by Def9
.= ((- 1.GF) * L).v by A1,Th34;
end;
end;
Lm2: (- 1.GF) * a = - a
proof
thus (- 1.GF) * a = (0.GF - 1.GF) * a by RLVECT_1:14
.= 0.GF * a - 1.GF * a by VECTSP_1:13
.= 0.GF - 1.GF * a
.= - 1.GF * a by RLVECT_1:14
.= - a;
end;
theorem Th36:
(- L).v = - L.v
proof
thus (- L).v = (- 1.GF) * L.v by Def9
.= - L.v by Lm2;
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,Th22
.= 0.GF by Th3;
hence L2.v = - L1.v by RLVECT_1:6
.= (- L1).v by Th36;
end;
Lm3: for GF being Field holds - 1.GF <> 0.GF
proof
let GF be Field;
assume not thesis;
then 1.GF = - 0.GF by RLVECT_1:17;
hence thesis by RLVECT_1:12;
end;
theorem Th38:
Carrier(- L) = Carrier(L)
proof
Carrier(- L) c= Carrier(L) & Carrier(-- L) c= Carrier(-L) by Th28;
hence thesis;
end;
theorem
L is Linear_Combination of A implies - L is Linear_Combination of A by Th31;
definition
let GF,V,L1,L2;
func L1 - L2 -> Linear_Combination of V equals
L1 + (- L2);
coherence;
end;
theorem Th40:
(L1 - L2).v = L1.v - L2.v
proof
thus (L1 - L2).v = L1.v + (- L2).v by Th22
.= L1.v + (- L2.v) by Th36
.= L1.v - L2.v by RLVECT_1:def 11;
end;
theorem
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2)
proof
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(- L2) by Th23;
hence thesis by Th38;
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,Th31;
hence thesis by A1,Th24;
end;
theorem Th43:
L - L = ZeroLC(V)
proof
let v;
thus (L - L).v = L.v - L.v by Th40
.= 0.GF by RLVECT_1:15
.= ZeroLC(V).v by Th3;
end;
theorem Th44:
Sum(L1 + L2) = Sum(L1) + Sum(L2)
proof
set A = Carrier(L1 + L2) \/ Carrier(L1) \/ Carrier(L2);
set C1 = A \ Carrier(L1);
consider p such that
A1: rng p = C1 and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of the carrier of V by A1,FINSEQ_1:def 4;
A3: A = Carrier(L1) \/ (Carrier(L1 + L2) \/ Carrier(L2)) by XBOOLE_1:4;
set C3 = A \ Carrier(L1 + L2);
consider r such that
A4: rng r = C3 and
A5: r is one-to-one by FINSEQ_4:58;
reconsider r as FinSequence of the carrier of V by A4,FINSEQ_1:def 4;
A6: A = Carrier(L1 + L2) \/ (Carrier(L1) \/ Carrier(L2)) by XBOOLE_1:4;
set C2 = A \ Carrier(L2);
consider q such that
A7: rng q = C2 and
A8: q is one-to-one by FINSEQ_4:58;
reconsider q as FinSequence of the carrier of V by A7,FINSEQ_1:def 4;
consider F such that
A9: F is one-to-one and
A10: rng F = Carrier(L1 + L2) and
A11: Sum((L1 + L2) (#) F) = Sum(L1 + L2) by Def6;
set FF = F ^ r;
consider G such that
A12: G is one-to-one and
A13: rng G = Carrier(L1) and
A14: Sum(L1 (#) G) = Sum(L1) by Def6;
rng FF = rng F \/ rng r by FINSEQ_1:31;
then rng FF = Carrier(L1 + L2) \/ A by A10,A4,XBOOLE_1:39;
then
A15: rng FF = A by A6,XBOOLE_1:7,12;
set GG = G ^ p;
rng GG = rng G \/ rng p by FINSEQ_1:31;
then rng GG = Carrier(L1) \/ A by A13,A1,XBOOLE_1:39;
then
A16: rng GG = A by A3,XBOOLE_1:7,12;
rng F misses rng r
proof
set x = the Element of rng F /\ rng r;
assume not thesis;
then rng F /\ rng r <> {};
then x in Carrier(L1 + L2) & x in C3 by A10,A4,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A17: FF is one-to-one by A9,A5,FINSEQ_3:91;
rng G misses rng p
proof
set x = the Element of rng G /\ rng p;
assume not thesis;
then rng G /\ rng p <> {};
then x in Carrier(L1) & x in C1 by A13,A1,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A18: GG is one-to-one by A12,A2,FINSEQ_3:91;
then
A19: len GG = len FF by A17,A16,A15,FINSEQ_1:48;
deffunc F(Nat) = FF <- (GG.$1);
consider P being FinSequence such that
A20: len P = len FF and
A21: for k be Nat st k in dom P holds P.k = F(k) from FINSEQ_1:sch 2;
A22: dom P = Seg len FF by A20,FINSEQ_1:def 3;
A23: now
let x be object;
assume
A24: x in dom GG;
then reconsider n = x as Element of NAT by FINSEQ_3:23;
GG.n in rng FF by A16,A15,A24,FUNCT_1:def 3;
then
A25: FF just_once_values GG.n by A17,FINSEQ_4:8;
n in Seg(len FF) by A19,A24,FINSEQ_1:def 3;
then FF.(P.n) = FF.(FF <- (GG.n)) by A21,A22
.= GG.n by A25,FINSEQ_4:def 3;
hence GG.x = FF.(P.x);
end;
A26: rng P c= dom FF
proof
let x be object;
assume x in rng P;
then consider y being object such that
A27: y in dom P and
A28: P.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A27,FINSEQ_3:23;
y in dom GG by A19,A20,A27,FINSEQ_3:29;
then GG.y in rng FF by A16,A15,FUNCT_1:def 3;
then
A29: FF just_once_values GG.y by A17,FINSEQ_4:8;
P.y = FF <- (GG.y) by A21,A27;
hence thesis by A28,A29,FINSEQ_4:def 3;
end;
now
let x be object;
thus x in dom GG implies x in dom P & P.x in dom FF
proof
assume x in dom GG;
then x in Seg(len P) by A19,A20,FINSEQ_1:def 3;
hence x in dom P by FINSEQ_1:def 3;
then P.x in rng P by FUNCT_1:def 3;
hence thesis by A26;
end;
assume that
A30: x in dom P and
P.x in dom FF;
x in Seg(len P) by A30,FINSEQ_1:def 3;
hence x in dom GG by A19,A20,FINSEQ_1:def 3;
end;
then
A31: GG = FF * P by A23,FUNCT_1:10;
dom FF c= rng P
proof
set f = FF" * GG;
let x be object;
assume
A32: x in dom FF;
dom(FF") = rng GG by A17,A16,A15,FUNCT_1:33;
then
A33: rng f = rng(FF") by RELAT_1:28
.= dom FF by A17,FUNCT_1:33;
f = FF " * FF * P by A31,RELAT_1:36
.= id(dom FF) * P by A17,FUNCT_1:39
.= P by A26,RELAT_1:53;
hence thesis by A32,A33;
end;
then
A34: dom FF = rng P by A26;
A35: len r = len((L1 + L2) (#) r) by Def5;
now
let k be Nat;
assume
A36: k in dom r;
then r/.k = r.k by PARTFUN1:def 6;
then r/.k in C3 by A4,A36,FUNCT_1:def 3;
then
A37: not r/.k in Carrier((L1 + L2)) by XBOOLE_0:def 5;
k in dom((L1 + L2) (#) r) by A35,A36,FINSEQ_3:29;
then ((L1 + L2) (#) r).k = (L1 + L2).(r/.k) * r/.k by Def5;
hence ((L1 + L2) (#) r).k = 0.GF * r/.k by A37;
end;
then
A38: Sum((L1 + L2) (#) r) = 0.GF * Sum(r) by A35,RLVECT_2:67
.= 0.V by VECTSP_1:14;
A39: len p = len(L1 (#) p) by Def5;
now
let k be Nat;
assume
A40: k in dom p;
then p/.k = p.k by PARTFUN1:def 6;
then p/.k in C1 by A1,A40,FUNCT_1:def 3;
then
A41: not p/.k in Carrier(L1) by XBOOLE_0:def 5;
k in dom(L1 (#) p) by A39,A40,FINSEQ_3:29;
then (L1 (#) p).k = L1.(p/.k) * p/.k by Def5;
hence (L1 (#) p).k = 0.GF * p/.k by A41;
end;
then
A42: Sum(L1 (#) p) = 0.GF * Sum(p) by A39,RLVECT_2:67
.= 0.V by VECTSP_1:14;
A43: len q = len(L2 (#) q) by Def5;
now
let k be Nat;
assume
A44: k in dom q;
then q/.k = q.k by PARTFUN1:def 6;
then q/.k in C2 by A7,A44,FUNCT_1:def 3;
then
A45: not q/.k in Carrier(L2) by XBOOLE_0:def 5;
k in dom(L2 (#) q) by A43,A44,FINSEQ_3:29;
then (L2 (#) q).k = L2.(q/.k) * q/.k by Def5;
hence (L2 (#) q).k = 0.GF * q/.k by A45;
end;
then
A46: Sum(L2 (#) q) = 0.GF * Sum(q) by A43,RLVECT_2:67
.= 0.V by VECTSP_1:14;
set g = L1 (#) GG;
A47: len g = len GG by Def5;
then
A48: Seg len GG = dom g by FINSEQ_1:def 3;
set f = (L1 + L2) (#) FF;
consider H such that
A49: H is one-to-one and
A50: rng H = Carrier(L2) and
A51: Sum(L2 (#) H) = Sum(L2) by Def6;
set HH = H ^ q;
rng H misses rng q
proof
set x = the Element of rng H /\ rng q;
assume not thesis;
then rng H /\ rng q <> {};
then x in Carrier(L2) & x in C2 by A50,A7,XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 5;
end;
then
A52: HH is one-to-one by A49,A8,FINSEQ_3:91;
rng HH = rng H \/ rng q by FINSEQ_1:31;
then rng HH = Carrier(L2) \/ A by A50,A7,XBOOLE_1:39;
then
A53: rng HH = A by XBOOLE_1:7,12;
then
A54: len GG = len HH by A52,A18,A16,FINSEQ_1:48;
deffunc F(Nat) = HH <- (GG.$1);
consider R being FinSequence such that
A55: len R = len HH and
A56: for k be Nat st k in dom R holds R.k = F(k) from FINSEQ_1:sch 2;
A57: dom R = Seg len HH by A55,FINSEQ_1:def 3;
A58: now
let x be object;
assume
A59: x in dom GG;
then reconsider n = x as Element of NAT by FINSEQ_3:23;
GG.n in rng HH by A16,A53,A59,FUNCT_1:def 3;
then
A60: HH just_once_values GG.n by A52,FINSEQ_4:8;
n in Seg(len HH) by A54,A59,FINSEQ_1:def 3;
then HH.(R.n) = HH.(HH <- (GG.n)) by A56,A57
.= GG.n by A60,FINSEQ_4:def 3;
hence GG.x = HH.(R.x);
end;
A61: rng R c= dom HH
proof
let x be object;
assume x in rng R;
then consider y being object such that
A62: y in dom R and
A63: R.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A62,FINSEQ_3:23;
y in dom GG by A54,A55,A62,FINSEQ_3:29;
then GG.y in rng HH by A16,A53,FUNCT_1:def 3;
then
A64: HH just_once_values GG.y by A52,FINSEQ_4:8;
R.y = HH <- (GG.y) by A56,A62;
hence thesis by A63,A64,FINSEQ_4:def 3;
end;
now
let x be object;
thus x in dom GG implies x in dom R & R.x in dom HH
proof
assume x in dom GG;
then x in Seg(len R) by A54,A55,FINSEQ_1:def 3;
hence x in dom R by FINSEQ_1:def 3;
then R.x in rng R by FUNCT_1:def 3;
hence thesis by A61;
end;
assume that
A65: x in dom R and
R.x in dom HH;
x in Seg(len R) by A65,FINSEQ_1:def 3;
hence x in dom GG by A54,A55,FINSEQ_1:def 3;
end;
then
A66: GG = HH * R by A58,FUNCT_1:10;
dom HH c= rng R
proof
set f = HH" * GG;
let x be object;
assume
A67: x in dom HH;
dom(HH") = rng GG by A52,A16,A53,FUNCT_1:33;
then
A68: rng f = rng(HH") by RELAT_1:28
.= dom HH by A52,FUNCT_1:33;
f = HH " * HH * R by A66,RELAT_1:36
.= id(dom HH) * R by A52,FUNCT_1:39
.= R by A61,RELAT_1:53;
hence thesis by A67,A68;
end;
then
A69: dom HH = rng R by A61;
set h = L2 (#) HH;
A70: Sum(h) = Sum((L2 (#) H) ^ (L2 (#) q)) by Th13
.= Sum(L2 (#) H) + 0.V by A46,RLVECT_1:41
.= Sum(L2 (#) H) by RLVECT_1:4;
A71: Sum(g) = Sum((L1 (#) G) ^ (L1 (#) p)) by Th13
.= Sum(L1 (#) G) + 0.V by A42,RLVECT_1:41
.= Sum(L1 (#) G) by RLVECT_1:4;
A72: dom P = dom FF by A20,FINSEQ_3:29;
then
A73: P is one-to-one by A34,FINSEQ_4:60;
A74: dom R = dom HH by A55,FINSEQ_3:29;
then
A75: R is one-to-one by A69,FINSEQ_4:60;
reconsider R as Function of dom HH, dom HH by A61,A74,FUNCT_2:2;
reconsider R as Permutation of dom HH by A69,A75,FUNCT_2:57;
A76: len h = len HH by Def5;
then dom h = dom HH by FINSEQ_3:29;
then reconsider R as Permutation of dom h;
reconsider Hp = h * R as FinSequence of the carrier of V by FINSEQ_2:47;
A77: len Hp = len GG by A54,A76,FINSEQ_2:44;
reconsider P as Function of dom FF, dom FF by A26,A72,FUNCT_2:2;
reconsider P as Permutation of dom FF by A34,A73,FUNCT_2:57;
A78: len f = len FF by Def5;
then dom f = dom FF by FINSEQ_3:29;
then reconsider P as Permutation of dom f;
reconsider Fp = f * P as FinSequence of the carrier of V by FINSEQ_2:47;
A79: Sum(f) = Sum(((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Th13
.= Sum((L1 + L2) (#) F) + 0.V by A38,RLVECT_1:41
.= Sum((L1 + L2) (#) F) by RLVECT_1:4;
deffunc F(Nat) = g/.$1 + Hp/.$1;
consider I being FinSequence such that
A80: len I = len GG and
A81: for k be Nat st k in dom I holds I.k = F(k) from FINSEQ_1:sch 2;
A82: dom I = Seg len GG by A80,FINSEQ_1:def 3;
then
A83: for k be Nat st k in Seg(len GG) holds I.k = F(k) by A81;
rng I c= the carrier of V
proof
let x be object;
assume x in rng I;
then consider y being object such that
A84: y in dom I and
A85: I.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A84,FINSEQ_3:23;
I.y = g/.y + Hp/.y by A81,A84;
hence thesis by A85;
end;
then reconsider I as FinSequence of the carrier of V by FINSEQ_1:def 4;
A86: len Fp = len I by A19,A78,A80,FINSEQ_2:44;
A87: now
let x be object;
assume
A88: x in Seg(len I);
then reconsider k = x as Element of NAT;
A89: x in dom Hp by A80,A77,A88,FINSEQ_1:def 3;
then
A90: Hp/.k = (h * R).k by PARTFUN1:def 6
.= h.(R.k) by A89,FUNCT_1:12;
set v = GG/.k;
x in dom Fp by A86,A88,FINSEQ_1:def 3;
then
A91: Fp.k = f.(P.k) by FUNCT_1:12;
A92: x in dom HH by A54,A80,A88,FINSEQ_1:def 3;
then R.k in dom R by A69,A74,FUNCT_1:def 3;
then reconsider j = R.k as Element of NAT by FINSEQ_3:23;
A93: x in dom GG by A80,A88,FINSEQ_1:def 3;
then
A94: HH.j = GG.k by A58
.= GG/.k by A93,PARTFUN1:def 6;
A95: dom FF = dom GG by A19,FINSEQ_3:29;
then P.k in dom P by A34,A72,A93,FUNCT_1:def 3;
then reconsider l = P.k as Element of NAT by FINSEQ_3:23;
A96: FF.l = GG.k by A23,A93
.= GG/.k by A93,PARTFUN1:def 6;
R.k in dom HH by A69,A74,A92,FUNCT_1:def 3;
then
A97: h.j = L2.v * v by A94,Th8;
P.k in dom FF by A34,A72,A93,A95,FUNCT_1:def 3;
then
A98: f.l = (L1 + L2).v * v by A96,Th8
.= (L1.v + L2.v) * v by Th22
.= L1.v * v + L2.v * v by VECTSP_1:def 15;
A99: x in dom g by A80,A47,A88,FINSEQ_1:def 3;
then g/.k = g.k by PARTFUN1:def 6
.= L1.v * v by A99,Def5;
hence I.x = Fp.x by A80,A81,A82,A88,A90,A97,A91,A98;
end;
dom I = Seg(len I) & dom Fp = Seg(len I) by A86,FINSEQ_1:def 3;
then
A100: I = Fp by A87;
Sum(Fp) = Sum(f) & Sum(Hp) = Sum(h) by RLVECT_2:7;
hence thesis by A11,A14,A51,A71,A70,A79,A80,A83,A77,A47,A100,A48,RLVECT_2:2;
end;
theorem
for GF being Field, V being VectSp of GF, L being Linear_Combination
of V, a being Element of GF holds Sum(a * L) = a * Sum(L)
proof
let GF be Field, V be VectSp of GF, L be Linear_Combination of V, a be
Element of GF;
per cases;
suppose
A1: a <> 0.GF;
set l = a * L;
consider F being FinSequence of the carrier of V such that
A2: F is one-to-one and
A3: rng F = Carrier(a * L) and
A4: Sum(a * L) = Sum((a * L) (#) F) by Def6;
consider G being FinSequence of the carrier of V such that
A5: G is one-to-one and
A6: rng G = Carrier(L) and
A7: Sum(L) = Sum(L (#) G) by Def6;
A8: len G = len F by A1,A2,A3,A5,A6,Th29,FINSEQ_1:48;
set f = (a * L) (#) F;
set g = L (#) G;
deffunc F(Nat) = F <- (G.$1);
consider P being FinSequence such that
A9: len P = len F and
A10: for k be Nat st k in dom P holds P.k = F(k) from FINSEQ_1:sch 2;
A11: Carrier(l) = Carrier(L) by A1,Th29;
A12: rng P c= Seg(len F)
proof
let x be object;
assume x in rng P;
then consider y being object such that
A13: y in dom P and
A14: P.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A13,FINSEQ_3:23;
y in Seg(len F) by A9,A13,FINSEQ_1:def 3;
then y in dom G by A8,FINSEQ_1:def 3;
then G.y in rng F by A3,A6,A11,FUNCT_1:def 3;
then
A15: F just_once_values G.y by A2,FINSEQ_4:8;
P.y = F <- (G.y) by A10,A13;
then P.y in dom F by A15,FINSEQ_4:def 3;
hence thesis by A14,FINSEQ_1:def 3;
end;
A16: now
let x be object;
thus x in dom G implies x in dom P & P.x in dom F
proof
assume x in dom G;
then x in Seg(len P) by A9,A8,FINSEQ_1:def 3;
hence x in dom P by FINSEQ_1:def 3;
then P.x in rng P by FUNCT_1:def 3;
then P.x in Seg(len F) by A12;
hence thesis by FINSEQ_1:def 3;
end;
assume that
A17: x in dom P and
P.x in dom F;
x in Seg(len P) by A17,FINSEQ_1:def 3;
hence x in dom G by A9,A8,FINSEQ_1:def 3;
end;
A18: dom P = Seg len F by A9,FINSEQ_1:def 3;
now
let x be object;
assume
A19: x in dom G;
then reconsider n = x as Element of NAT by FINSEQ_3:23;
G.n in rng F by A3,A6,A11,A19,FUNCT_1:def 3;
then
A20: F just_once_values G.n by A2,FINSEQ_4:8;
n in Seg(len F) by A8,A19,FINSEQ_1:def 3;
then F.(P.n) = F.(F <- (G.n)) by A10,A18
.= G.n by A20,FINSEQ_4:def 3;
hence G.x = F.(P.x);
end;
then
A21: G = F * P by A16,FUNCT_1:10;
Seg(len F) c= rng P
proof
set f = F" * G;
let x be object;
assume
A22: x in Seg(len F);
dom(F") = rng G by A2,A3,A6,A11,FUNCT_1:33;
then
A23: rng f = rng(F") by RELAT_1:28
.= dom F by A2,FUNCT_1:33;
A24: rng P c= dom F by A12,FINSEQ_1:def 3;
f = F " * F * P by A21,RELAT_1:36
.= id(dom F) * P by A2,FUNCT_1:39
.= P by A24,RELAT_1:53;
hence thesis by A22,A23,FINSEQ_1:def 3;
end;
then
A25: Seg(len F) = rng P by A12;
A26: dom P = Seg(len F) by A9,FINSEQ_1:def 3;
then
A27: P is one-to-one by A25,FINSEQ_4:60;
reconsider P as Function of Seg(len F), Seg(len F) by A12,A26,FUNCT_2:2;
reconsider P as Permutation of Seg(len F) by A25,A27,FUNCT_2:57;
A28: len f = len F by Def5;
then dom f = Seg len F by FINSEQ_1:def 3;
then reconsider P as Permutation of dom f;
reconsider Fp = f * P as FinSequence of the carrier of V by FINSEQ_2:47;
A29: len Fp = len f by FINSEQ_2:44;
then
A30: len Fp = len g by A8,A28,Def5;
A31: now
let k be Nat;
let v be Vector of V;
assume that
A32: k in dom g and
A33: v = g.k;
A34: k in Seg len g by A32,FINSEQ_1:def 3;
then
A35: k in dom P by A9,A28,A29,A30,FINSEQ_1:def 3;
A36: k in dom G by A8,A28,A29,A30,A34,FINSEQ_1:def 3;
then G.k in rng G by FUNCT_1:def 3;
then F just_once_values G.k by A2,A3,A6,A11,FINSEQ_4:8;
then
A37: F <- (G.k) in dom F by FINSEQ_4:def 3;
then reconsider i = F <- (G.k) as Element of NAT by FINSEQ_3:23;
A38: G/.k = G.k by A36,PARTFUN1:def 6
.= F.(P.k) by A21,A35,FUNCT_1:13
.= F.i by A10,A18,A28,A29,A30,A34
.= F/.i by A37,PARTFUN1:def 6;
i in Seg(len f) by A28,A37,FINSEQ_1:def 3;
then
A39: i in dom f by FINSEQ_1:def 3;
thus Fp.k = f.(P.k) by A35,FUNCT_1:13
.= f.(F <- (G.k)) by A10,A18,A28,A29,A30,A34
.= l.(F/.i) * F/.i by A39,Def5
.= a * L.(F/.i) * F/.i by Def9
.= a * (L.(F/.i) * F/.i) by VECTSP_1:def 16
.= a * v by A32,A33,A38,Def5;
end;
Sum(Fp) = Sum(f) & dom Fp = dom g by A30,FINSEQ_3:29,RLVECT_2:7;
hence thesis by A4,A7,A30,A31,RLVECT_2:66;
end;
suppose
A40: a = 0.GF;
hence Sum(a * L) = Sum(ZeroLC(V)) by Th30
.= 0.V by Lm1
.= a * Sum(L) by A40,VECTSP_1:14;
end;
end;
theorem Th46:
Sum(- L) = - Sum(L)
proof
Sum(L) + Sum(- L) = Sum(L - L) by Th44
.= Sum ZeroLC V by Th43
.= 0.V by Lm1;
hence thesis by VECTSP_1:16;
end;
theorem
Sum(L1 - L2) = Sum(L1) - Sum(L2)
proof
thus Sum(L1 - L2) = Sum(L1) + Sum(- L2) by Th44
.= Sum(L1) + (- Sum(L2)) by Th46
.= Sum(L1) - Sum(L2) by RLVECT_1:def 11;
end;
::
:: Auxiliary theorems.
::
theorem
(- 1.GF) * a = - a by Lm2;
theorem
for GF being Field holds - 1.GF <> 0.GF by Lm3;