let V be RealLinearSpace; for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
let L1, L2 be Linear_Combination of V; Sum (L1 + L2) = (Sum L1) + (Sum L2)
consider F being FinSequence of the carrier of V such that
A1:
F is one-to-one
and
A2:
rng F = Carrier (L1 + L2)
and
A3:
Sum ((L1 + L2) (#) F) = Sum (L1 + L2)
by RLVECT_2:def 10;
set A = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2);
set C3 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2));
consider r being FinSequence such that
A4:
rng r = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2))
and
A5:
r is one-to-one
by FINSEQ_4:73;
reconsider r = r as FinSequence of the carrier of V by A4, FINSEQ_1:def 4;
set FF = F ^ r;
A6:
((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier (L1 + L2)) \/ ((Carrier L1) \/ (Carrier L2))
by XBOOLE_1:4;
rng F misses rng r
then A7:
F ^ r is one-to-one
by A1, A5, FINSEQ_3:98;
A8:
len r = len ((L1 + L2) (#) r)
by RLVECT_2:def 9;
then A11: Sum ((L1 + L2) (#) r) =
0 * (Sum r)
by A8, RLVECT_2:5
.=
0. V
by RLVECT_1:23
;
set f = (L1 + L2) (#) (F ^ r);
set C1 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1);
consider G being FinSequence of the carrier of V such that
A12:
G is one-to-one
and
A13:
rng G = Carrier L1
and
A14:
Sum (L1 (#) G) = Sum L1
by RLVECT_2:def 10;
consider p being FinSequence such that
A15:
rng p = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1)
and
A16:
p is one-to-one
by FINSEQ_4:73;
reconsider p = p as FinSequence of the carrier of V by A15, FINSEQ_1:def 4;
set GG = G ^ p;
A17: Sum ((L1 + L2) (#) (F ^ r)) =
Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r))
by Lm1
.=
(Sum ((L1 + L2) (#) F)) + (0. V)
by A11, RLVECT_1:58
.=
Sum ((L1 + L2) (#) F)
by RLVECT_1:10
;
set C2 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2);
consider H being FinSequence of the carrier of V such that
A18:
H is one-to-one
and
A19:
rng H = Carrier L2
and
A20:
Sum (L2 (#) H) = Sum L2
by RLVECT_2:def 10;
consider q being FinSequence such that
A21:
rng q = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2)
and
A22:
q is one-to-one
by FINSEQ_4:73;
reconsider q = q as FinSequence of the carrier of V by A21, FINSEQ_1:def 4;
set HH = H ^ q;
rng H misses rng q
then A23:
H ^ q is one-to-one
by A18, A22, FINSEQ_3:98;
set h = L2 (#) (H ^ q);
A24:
((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier L1) \/ ((Carrier (L1 + L2)) \/ (Carrier L2))
by XBOOLE_1:4;
rng (G ^ p) = (rng G) \/ (rng p)
by FINSEQ_1:44;
then
rng (G ^ p) = (Carrier L1) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2))
by A13, A15, XBOOLE_1:39;
then A25:
rng (G ^ p) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)
by A24, XBOOLE_1:7, XBOOLE_1:12;
A26:
len q = len (L2 (#) q)
by RLVECT_2:def 9;
then A29: Sum (L2 (#) q) =
0 * (Sum q)
by A26, RLVECT_2:5
.=
0. V
by RLVECT_1:23
;
A30: Sum (L2 (#) (H ^ q)) =
Sum ((L2 (#) H) ^ (L2 (#) q))
by Lm1
.=
(Sum (L2 (#) H)) + (0. V)
by A29, RLVECT_1:58
.=
Sum (L2 (#) H)
by RLVECT_1:10
;
deffunc H1( Nat) -> set = (F ^ r) <- ((G ^ p) . $1);
set g = L1 (#) (G ^ p);
consider P being FinSequence such that
A31:
len P = len (F ^ r)
and
A32:
for k being Nat st k in dom P holds
P . k = H1(k)
from FINSEQ_1:sch 2();
A33:
dom P = Seg (len (F ^ r))
by A31, FINSEQ_1:def 3;
A34:
len p = len (L1 (#) p)
by RLVECT_2:def 9;
then A37: Sum (L1 (#) p) =
0 * (Sum p)
by A34, RLVECT_2:5
.=
0. V
by RLVECT_1:23
;
A38: Sum (L1 (#) (G ^ p)) =
Sum ((L1 (#) G) ^ (L1 (#) p))
by Lm1
.=
(Sum (L1 (#) G)) + (0. V)
by A37, RLVECT_1:58
.=
Sum (L1 (#) G)
by RLVECT_1:10
;
rng (F ^ r) = (rng F) \/ (rng r)
by FINSEQ_1:44;
then
rng (F ^ r) = (Carrier (L1 + L2)) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2))
by A2, A4, XBOOLE_1:39;
then A39:
rng (F ^ r) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)
by A6, XBOOLE_1:7, XBOOLE_1:12;
rng G misses rng p
then A40:
G ^ p is one-to-one
by A12, A16, FINSEQ_3:98;
then A41:
len (G ^ p) = len (F ^ r)
by A7, A25, A39, FINSEQ_1:65;
A42:
dom P = Seg (len (F ^ r))
by A31, FINSEQ_1:def 3;
A46:
rng P c= Seg (len (F ^ r))
proof
let x be
set ;
TARSKI:def 3 ( not x in rng P or x in Seg (len (F ^ r)) )
assume
x in rng P
;
x in Seg (len (F ^ r))
then consider y being
set such that A47:
y in dom P
and A48:
P . y = x
by FUNCT_1:def 5;
reconsider y =
y as
Element of
NAT by A47, FINSEQ_3:25;
y in Seg (len (F ^ r))
by A31, A47, FINSEQ_1:def 3;
then
y in dom (G ^ p)
by A41, FINSEQ_1:def 3;
then
(G ^ p) . y in rng (F ^ r)
by A25, A39, FUNCT_1:def 5;
then A49:
F ^ r just_once_values (G ^ p) . y
by A7, FINSEQ_4:10;
P . y = (F ^ r) <- ((G ^ p) . y)
by A32, A47;
then
P . y in dom (F ^ r)
by A49, FINSEQ_4:def 3;
hence
x in Seg (len (F ^ r))
by A48, FINSEQ_1:def 3;
verum
end;
then A51:
G ^ p = (F ^ r) * P
by A43, FUNCT_1:20;
Seg (len (F ^ r)) c= rng P
proof
set f =
((F ^ r) " ) * (G ^ p);
let x be
set ;
TARSKI:def 3 ( not x in Seg (len (F ^ r)) or x in rng P )
assume A52:
x in Seg (len (F ^ r))
;
x in rng P
dom ((F ^ r) " ) = rng (G ^ p)
by A7, A25, A39, FUNCT_1:55;
then A53:
rng (((F ^ r) " ) * (G ^ p)) =
rng ((F ^ r) " )
by RELAT_1:47
.=
dom (F ^ r)
by A7, FUNCT_1:55
;
A54:
rng P c= dom (F ^ r)
by A46, FINSEQ_1:def 3;
((F ^ r) " ) * (G ^ p) =
(((F ^ r) " ) * (F ^ r)) * P
by A51, RELAT_1:55
.=
(id (dom (F ^ r))) * P
by A7, FUNCT_1:61
.=
P
by A54, RELAT_1:79
;
hence
x in rng P
by A52, A53, FINSEQ_1:def 3;
verum
end;
then A55:
Seg (len (F ^ r)) = rng P
by A46, XBOOLE_0:def 10;
then A56:
P is one-to-one
by A33, FINSEQ_4:75;
( Seg (len (F ^ r)) = {} implies Seg (len (F ^ r)) = {} )
;
then reconsider P = P as Function of (Seg (len (F ^ r))),(Seg (len (F ^ r))) by A46, A33, FUNCT_2:def 1, RELSET_1:11;
reconsider P = P as Permutation of (Seg (len (F ^ r))) by A55, A56, FUNCT_2:83;
A57:
len ((L1 + L2) (#) (F ^ r)) = len (F ^ r)
by RLVECT_2:def 9;
then A58:
Seg (len (F ^ r)) = dom ((L1 + L2) (#) (F ^ r))
by FINSEQ_1:def 3;
then reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of the carrier of V by FINSEQ_2:51;
A59:
len (L1 (#) (G ^ p)) = len (G ^ p)
by RLVECT_2:def 9;
deffunc H2( Nat) -> set = (H ^ q) <- ((G ^ p) . $1);
consider R being FinSequence such that
A60:
len R = len (H ^ q)
and
A61:
for k being Nat st k in dom R holds
R . k = H2(k)
from FINSEQ_1:sch 2();
A62:
dom R = Seg (len (H ^ q))
by A60, FINSEQ_1:def 3;
rng (H ^ q) = (rng H) \/ (rng q)
by FINSEQ_1:44;
then
rng (H ^ q) = (Carrier L2) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2))
by A19, A21, XBOOLE_1:39;
then A63:
rng (H ^ q) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)
by XBOOLE_1:7, XBOOLE_1:12;
then A64:
len (G ^ p) = len (H ^ q)
by A23, A40, A25, FINSEQ_1:65;
A65:
dom R = Seg (len (H ^ q))
by A60, FINSEQ_1:def 3;
A69:
rng R c= Seg (len (H ^ q))
proof
let x be
set ;
TARSKI:def 3 ( not x in rng R or x in Seg (len (H ^ q)) )
assume
x in rng R
;
x in Seg (len (H ^ q))
then consider y being
set such that A70:
y in dom R
and A71:
R . y = x
by FUNCT_1:def 5;
reconsider y =
y as
Element of
NAT by A70, FINSEQ_3:25;
y in Seg (len (H ^ q))
by A60, A70, FINSEQ_1:def 3;
then
y in dom (G ^ p)
by A64, FINSEQ_1:def 3;
then
(G ^ p) . y in rng (H ^ q)
by A25, A63, FUNCT_1:def 5;
then A72:
H ^ q just_once_values (G ^ p) . y
by A23, FINSEQ_4:10;
R . y = (H ^ q) <- ((G ^ p) . y)
by A61, A70;
then
R . y in dom (H ^ q)
by A72, FINSEQ_4:def 3;
hence
x in Seg (len (H ^ q))
by A71, FINSEQ_1:def 3;
verum
end;
then A74:
G ^ p = (H ^ q) * R
by A66, FUNCT_1:20;
Seg (len (H ^ q)) c= rng R
proof
set f =
((H ^ q) " ) * (G ^ p);
let x be
set ;
TARSKI:def 3 ( not x in Seg (len (H ^ q)) or x in rng R )
assume A75:
x in Seg (len (H ^ q))
;
x in rng R
dom ((H ^ q) " ) = rng (G ^ p)
by A23, A25, A63, FUNCT_1:55;
then A76:
rng (((H ^ q) " ) * (G ^ p)) =
rng ((H ^ q) " )
by RELAT_1:47
.=
dom (H ^ q)
by A23, FUNCT_1:55
;
A77:
rng R c= dom (H ^ q)
by A69, FINSEQ_1:def 3;
((H ^ q) " ) * (G ^ p) =
(((H ^ q) " ) * (H ^ q)) * R
by A74, RELAT_1:55
.=
(id (dom (H ^ q))) * R
by A23, FUNCT_1:61
.=
R
by A77, RELAT_1:79
;
hence
x in rng R
by A75, A76, FINSEQ_1:def 3;
verum
end;
then A78:
Seg (len (H ^ q)) = rng R
by A69, XBOOLE_0:def 10;
then A79:
R is one-to-one
by A62, FINSEQ_4:75;
( Seg (len (H ^ q)) = {} implies Seg (len (H ^ q)) = {} )
;
then reconsider R = R as Function of (Seg (len (H ^ q))),(Seg (len (H ^ q))) by A69, A62, FUNCT_2:def 1, RELSET_1:11;
reconsider R = R as Permutation of (Seg (len (H ^ q))) by A78, A79, FUNCT_2:83;
A80:
len (L2 (#) (H ^ q)) = len (H ^ q)
by RLVECT_2:def 9;
then A81:
Seg (len (H ^ q)) = dom (L2 (#) (H ^ q))
by FINSEQ_1:def 3;
then reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of the carrier of V by FINSEQ_2:51;
A82:
len Hp = len (G ^ p)
by A64, A80, A81, FINSEQ_2:48;
deffunc H3( Nat) -> Element of the carrier of V = ((L1 (#) (G ^ p)) /. $1) + (Hp /. $1);
consider I being FinSequence such that
A83:
len I = len (G ^ p)
and
A84:
for k being Nat st k in dom I holds
I . k = H3(k)
from FINSEQ_1:sch 2();
dom I = Seg (len (G ^ p))
by A83, FINSEQ_1:def 3;
then A85:
for k being Element of NAT st k in Seg (len (G ^ p)) holds
I . k = H3(k)
by A84;
rng I c= the carrier of V
then reconsider I = I as FinSequence of the carrier of V by FINSEQ_1:def 4;
A88:
len Fp = len I
by A41, A57, A58, A83, FINSEQ_2:48;
A89:
now let x be
set ;
( x in dom I implies I . x = Fp . x )assume A90:
x in dom I
;
I . x = Fp . xthen reconsider k =
x as
Element of
NAT by FINSEQ_3:25;
A91:
x in dom Hp
by A83, A82, A90, FINSEQ_3:31;
k in dom R
by A64, A62, A83, A90, FINSEQ_1:def 3;
then A92:
R . k in dom R
by A78, A62, FUNCT_1:def 5;
then reconsider j =
R . k as
Element of
NAT by FINSEQ_3:25;
set v =
(G ^ p) /. k;
A93:
R . k in dom (H ^ q)
by A60, A92, FINSEQ_3:31;
A94:
x in dom (G ^ p)
by A83, A90, FINSEQ_3:31;
then (H ^ q) . j =
(G ^ p) . k
by A66
.=
(G ^ p) /. k
by A94, PARTFUN1:def 8
;
then A95:
(L2 (#) (H ^ q)) . j = (L2 . ((G ^ p) /. k)) * ((G ^ p) /. k)
by A93, RLVECT_2:40;
k in dom P
by A41, A33, A83, A90, FINSEQ_1:def 3;
then A96:
P . k in dom P
by A55, A33, FUNCT_1:def 5;
then reconsider l =
P . k as
Element of
NAT by FINSEQ_3:25;
A97:
P . k in dom (F ^ r)
by A31, A96, FINSEQ_3:31;
x in dom Fp
by A88, A90, FINSEQ_3:31;
then A98:
Fp . k = ((L1 + L2) (#) (F ^ r)) . (P . k)
by FUNCT_1:22;
k in dom Hp
by A83, A82, A90, FINSEQ_3:31;
then A99:
Hp /. k =
((L2 (#) (H ^ q)) * R) . k
by PARTFUN1:def 8
.=
(L2 (#) (H ^ q)) . (R . k)
by A91, FUNCT_1:22
;
A100:
x in dom (L1 (#) (G ^ p))
by A83, A59, A90, FINSEQ_3:31;
(F ^ r) . l =
(G ^ p) . k
by A43, A94
.=
(G ^ p) /. k
by A94, PARTFUN1:def 8
;
then A101:
((L1 + L2) (#) (F ^ r)) . l =
((L1 + L2) . ((G ^ p) /. k)) * ((G ^ p) /. k)
by A97, RLVECT_2:40
.=
((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) * ((G ^ p) /. k)
by RLVECT_2:def 12
.=
((L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)) + ((L2 . ((G ^ p) /. k)) * ((G ^ p) /. k))
by RLVECT_1:def 9
;
k in dom (L1 (#) (G ^ p))
by A83, A59, A90, FINSEQ_3:31;
then (L1 (#) (G ^ p)) /. k =
(L1 (#) (G ^ p)) . k
by PARTFUN1:def 8
.=
(L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)
by A100, RLVECT_2:def 9
;
hence
I . x = Fp . x
by A84, A90, A99, A95, A98, A101;
verum end;
dom (L2 (#) (H ^ q)) = Seg (len (L2 (#) (H ^ q)))
by FINSEQ_1:def 3;
then A102:
Sum Hp = Sum (L2 (#) (H ^ q))
by A80, RLVECT_2:9;
dom ((L1 + L2) (#) (F ^ r)) = Seg (len ((L1 + L2) (#) (F ^ r)))
by FINSEQ_1:def 3;
then A103:
Sum Fp = Sum ((L1 + L2) (#) (F ^ r))
by A57, RLVECT_2:9;
( dom I = Seg (len I) & dom Fp = Seg (len I) )
by A88, FINSEQ_1:def 3;
then A104:
I = Fp
by A89, FUNCT_1:9;
Seg (len (G ^ p)) = dom (L1 (#) (G ^ p))
by A59, FINSEQ_1:def 3;
hence
Sum (L1 + L2) = (Sum L1) + (Sum L2)
by A3, A14, A20, A38, A30, A17, A103, A102, A83, A85, A82, A59, A104, RLVECT_2:4; verum