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