let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for V being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
let V be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: 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 Def9;
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 Def9;
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 Def9;
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 Def8;
then A15: Sum (L1 (#) p) =
(0. GF) * (Sum p)
by A12, VECTSP_3:10
.=
0. V
by VECTSP_1:59
;
set GG = G ^ p;
set g = L1 (#) (G ^ p);
A16: Sum (L1 (#) (G ^ p)) =
Sum ((L1 (#) G) ^ (L1 (#) p))
by Th37
.=
(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 Def8;
then A22: Sum (L2 (#) q) =
(0. GF) * (Sum q)
by A19, VECTSP_3:10
.=
0. V
by VECTSP_1:59
;
set HH = H ^ q;
set h = L2 (#) (H ^ q);
A23: Sum (L2 (#) (H ^ q)) =
Sum ((L2 (#) H) ^ (L2 (#) q))
by Th37
.=
(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 Def8;
then A29: Sum ((L1 + L2) (#) r) =
(0. GF) * (Sum r)
by A26, VECTSP_3:10
.=
0. V
by VECTSP_1:59
;
set FF = F ^ r;
set f = (L1 + L2) (#) (F ^ r);
A30: Sum ((L1 + L2) (#) (F ^ r)) =
Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r))
by Th37
.=
(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= dom (F ^ r)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng P or x in dom (F ^ r) )
assume
x in rng P
;
:: thesis: x in dom (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:
dom (F ^ r) = Seg (len (F ^ r))
by FINSEQ_1:def 3;
A47:
y in dom (F ^ r)
by A40, A44, FINSEQ_3:31;
y in dom (G ^ p)
by A39, A40, A44, FINSEQ_3:31;
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, A47, A42, FINSEQ_4:10;
hence
x in dom (F ^ r)
by A45, FINSEQ_4:def 3;
:: thesis: verum
end;
then A52:
G ^ p = (F ^ r) * P
by A48, FUNCT_1:20;
dom (F ^ r) c= rng P
then A55:
dom (F ^ r) = rng P
by A43, XBOOLE_0:def 10;
A56:
dom P = dom (F ^ r)
by A40, FINSEQ_3:31;
then A57:
P is one-to-one
by A55, FINSEQ_4:75;
( dom (F ^ r) = {} implies dom (F ^ r) = {} )
;
then reconsider P = P as Function of (dom (F ^ r)),(dom (F ^ r)) by A43, A56, FUNCT_2:def 1, RELSET_1:11;
reconsider P = P as Permutation of (dom (F ^ r)) by A55, A57, FUNCT_2:83;
A58:
len ((L1 + L2) (#) (F ^ r)) = len (F ^ r)
by Def8;
then
dom ((L1 + L2) (#) (F ^ r)) = dom (F ^ r)
by FINSEQ_3:31;
then reconsider P = P as Permutation of (dom ((L1 + L2) (#) (F ^ r))) ;
reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of the carrier of V by FINSEQ_2:51;
A59:
Sum Fp = Sum ((L1 + L2) (#) (F ^ r))
by RLVECT_2: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;
A63:
rng R c= dom (H ^ q)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng R or x in dom (H ^ q) )
assume
x in rng R
;
:: thesis: x in dom (H ^ q)
then consider y being
set such that A64:
y in dom R
and A65:
R . y = x
by FUNCT_1:def 5;
reconsider y =
y as
Element of
NAT by A64, FINSEQ_3:25;
A66:
dom (H ^ q) = Seg (len (H ^ q))
by FINSEQ_1:def 3;
A67:
y in dom (H ^ q)
by A60, A64, FINSEQ_3:31;
y in dom (G ^ p)
by A39, A60, A64, FINSEQ_3:31;
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, A61, A66, A67, A62, FINSEQ_4:10;
hence
x in dom (H ^ q)
by A65, FINSEQ_4:def 3;
:: thesis: verum
end;
then A72:
G ^ p = (H ^ q) * R
by A68, FUNCT_1:20;
dom (H ^ q) c= rng R
then A75:
dom (H ^ q) = rng R
by A63, XBOOLE_0:def 10;
A76:
dom R = dom (H ^ q)
by A60, FINSEQ_3:31;
then A77:
R is one-to-one
by A75, FINSEQ_4:75;
( dom (H ^ q) = {} implies dom (H ^ q) = {} )
;
then reconsider R = R as Function of (dom (H ^ q)),(dom (H ^ q)) by A63, A76, FUNCT_2:def 1, RELSET_1:11;
reconsider R = R as Permutation of (dom (H ^ q)) by A75, A77, FUNCT_2:83;
A78:
len (L2 (#) (H ^ q)) = len (H ^ q)
by Def8;
then
dom (L2 (#) (H ^ q)) = dom (H ^ q)
by FINSEQ_3:31;
then reconsider R = R as Permutation of (dom (L2 (#) (H ^ q))) ;
reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of the carrier of V by FINSEQ_2:51;
A79:
Sum Hp = Sum (L2 (#) (H ^ q))
by RLVECT_2:9;
deffunc H3( Nat) -> Element of the carrier of V = ((L1 (#) (G ^ p)) /. $1) + (Hp /. $1);
consider I being FinSequence such that
A80:
len I = len (G ^ p)
and
A81:
for k being Nat st k in dom I holds
I . k = H3(k)
from FINSEQ_1:sch 2();
A82:
dom I = Seg (len (G ^ p))
by A80, FINSEQ_1:def 3;
A83:
for k being Element of NAT st k in Seg (len (G ^ p)) holds
I . k = H3(k)
by A81, A82;
rng I c= the carrier of V
then reconsider I = I as FinSequence of the carrier of V by FINSEQ_1:def 4;
A86:
len Fp = len I
by A39, A58, A80, FINSEQ_2:48;
then A87:
( dom I = Seg (len I) & dom Fp = Seg (len I) )
by FINSEQ_1:def 3;
A88:
( len Hp = len (G ^ p) & len (L1 (#) (G ^ p)) = len (G ^ p) )
by A39, A78, Def8, FINSEQ_2:48;
now let x be
set ;
:: thesis: ( x in Seg (len I) implies I . x = Fp . x )assume A89:
x in Seg (len I)
;
:: thesis: I . x = Fp . xthen A90:
(
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, A80, A86, A88, FINSEQ_1:def 3;
reconsider k =
x as
Element of
NAT by A89;
set v =
(G ^ p) /. k;
A91:
(L1 (#) (G ^ p)) /. k =
(L1 (#) (G ^ p)) . k
by A90, PARTFUN1:def 8
.=
(L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)
by A90, Def8
;
A92:
Hp /. k =
((L2 (#) (H ^ q)) * R) . k
by A90, PARTFUN1:def 8
.=
(L2 (#) (H ^ q)) . (R . k)
by A90, FUNCT_1:22
;
A93:
R . k in dom R
by A75, A76, A90, FUNCT_1:def 5;
A94:
R . k in dom (H ^ q)
by A75, A76, A90, FUNCT_1:def 5;
reconsider j =
R . k as
Element of
NAT by A93, FINSEQ_3:25;
(H ^ q) . j =
(G ^ p) . k
by A69, A90
.=
(G ^ p) /. k
by A90, PARTFUN1:def 8
;
then A95:
(L2 (#) (H ^ q)) . j = (L2 . ((G ^ p) /. k)) * ((G ^ p) /. k)
by A94, Th32;
A96:
Fp . k = ((L1 + L2) (#) (F ^ r)) . (P . k)
by A90, FUNCT_1:22;
A97:
dom (F ^ r) = dom (G ^ p)
by A39, FINSEQ_3:31;
then A98:
P . k in dom P
by A55, A56, A90, FUNCT_1:def 5;
A99:
P . k in dom (F ^ r)
by A55, A56, A90, A97, FUNCT_1:def 5;
reconsider l =
P . k as
Element of
NAT by A98, FINSEQ_3:25;
(F ^ r) . l =
(G ^ p) . k
by A49, A90
.=
(G ^ p) /. k
by A90, PARTFUN1:def 8
;
then ((L1 + L2) (#) (F ^ r)) . l =
((L1 + L2) . ((G ^ p) /. k)) * ((G ^ p) /. k)
by A99, Th32
.=
((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) * ((G ^ p) /. k)
by Def11
.=
((L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)) + ((L2 . ((G ^ p) /. k)) * ((G ^ p) /. k))
by VECTSP_1:def 26
;
hence
I . x = Fp . x
by A80, A81, A89, A91, A92, A95, A96, A82;
:: thesis: verum end;
then A100:
I = Fp
by A87, FUNCT_1:9;
Seg (len (G ^ p)) = dom (L1 (#) (G ^ p))
by A88, FINSEQ_1:def 3;
hence
Sum (L1 + L2) = (Sum L1) + (Sum L2)
by A3, A6, A9, A16, A23, A30, A59, A79, A80, A83, A88, A100, RLVECT_2:4; :: thesis: verum