let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; 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)
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
A1:
rng p = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1)
and
A2:
p is one-to-one
by FINSEQ_4:58;
reconsider p = p as FinSequence of the carrier of V by A1, FINSEQ_1:def 4;
A3:
((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier L1) \/ ((Carrier (L1 + L2)) \/ (Carrier L2))
by XBOOLE_1:4;
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:58;
reconsider r = r as FinSequence of the carrier of V by A4, FINSEQ_1:def 4;
A6:
((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier (L1 + L2)) \/ ((Carrier L1) \/ (Carrier L2))
by XBOOLE_1:4;
set C2 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2);
consider q being FinSequence such that
A7:
rng q = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2)
and
A8:
q is one-to-one
by FINSEQ_4:58;
reconsider q = q as FinSequence of the carrier of V by A7, FINSEQ_1:def 4;
consider F being FinSequence of V 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 being FinSequence of V such that
A12:
G is one-to-one
and
A13:
rng G = Carrier L1
and
A14:
Sum (L1 (#) G) = Sum L1
by Def6;
rng (F ^ r) = (rng F) \/ (rng r)
by FINSEQ_1:31;
then
rng (F ^ r) = (Carrier (L1 + L2)) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2))
by A10, A4, XBOOLE_1:39;
then A15:
rng (F ^ r) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)
by A6, XBOOLE_1:7, XBOOLE_1:12;
set GG = G ^ p;
rng (G ^ p) = (rng G) \/ (rng p)
by FINSEQ_1:31;
then
rng (G ^ p) = (Carrier L1) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2))
by A13, A1, XBOOLE_1:39;
then A16:
rng (G ^ p) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)
by A3, XBOOLE_1:7, XBOOLE_1:12;
rng F misses rng r
then A17:
F ^ r is one-to-one
by A9, A5, FINSEQ_3:91;
rng G misses rng p
then A18:
G ^ p is one-to-one
by A12, A2, FINSEQ_3:91;
then A19:
len (G ^ p) = len (F ^ r)
by A17, A16, A15, FINSEQ_1:48;
deffunc H1( Nat) -> set = (F ^ r) <- ((G ^ p) . $1);
consider P being FinSequence such that
A20:
len P = len (F ^ r)
and
A21:
for k being Nat st k in dom P holds
P . k = H1(k)
from FINSEQ_1:sch 2();
A22:
dom P = Seg (len (F ^ r))
by A20, FINSEQ_1:def 3;
A26:
rng P c= dom (F ^ r)
proof
let x be
object ;
TARSKI:def 3 ( not x in rng P or x in dom (F ^ r) )
assume
x in rng P
;
x in dom (F ^ r)
then consider y being
object such that A27:
y in dom P
and A28:
P . y = x
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A27, FINSEQ_3:23;
y in dom (G ^ p)
by A19, A20, A27, FINSEQ_3:29;
then
(G ^ p) . y in rng (F ^ r)
by A16, A15, FUNCT_1:def 3;
then A29:
F ^ r just_once_values (G ^ p) . y
by A17, FINSEQ_4:8;
P . y = (F ^ r) <- ((G ^ p) . y)
by A21, A27;
hence
x in dom (F ^ r)
by A28, A29, FINSEQ_4:def 3;
verum
end;
then A31:
G ^ p = (F ^ r) * P
by A23, FUNCT_1:10;
dom (F ^ r) c= rng P
then A34:
dom (F ^ r) = rng P
by A26;
A35:
len r = len ((L1 + L2) (#) r)
by Def5;
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;
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;
then A46: Sum (L2 (#) q) =
(0. GF) * (Sum q)
by A43, RLVECT_2:67
.=
0. V
by VECTSP_1:14
;
set g = L1 (#) (G ^ p);
A47:
len (L1 (#) (G ^ p)) = len (G ^ p)
by Def5;
then A48:
Seg (len (G ^ p)) = dom (L1 (#) (G ^ p))
by FINSEQ_1:def 3;
set f = (L1 + L2) (#) (F ^ r);
consider H being FinSequence of V 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
then A52:
H ^ q is one-to-one
by A49, A8, FINSEQ_3:91;
rng (H ^ q) = (rng H) \/ (rng q)
by FINSEQ_1:31;
then
rng (H ^ q) = (Carrier L2) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2))
by A50, A7, XBOOLE_1:39;
then A53:
rng (H ^ q) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)
by XBOOLE_1:7, XBOOLE_1:12;
then A54:
len (G ^ p) = len (H ^ q)
by A52, A18, A16, FINSEQ_1:48;
deffunc H2( Nat) -> set = (H ^ q) <- ((G ^ p) . $1);
consider R being FinSequence such that
A55:
len R = len (H ^ q)
and
A56:
for k being Nat st k in dom R holds
R . k = H2(k)
from FINSEQ_1:sch 2();
A57:
dom R = Seg (len (H ^ q))
by A55, FINSEQ_1:def 3;
A61:
rng R c= dom (H ^ q)
proof
let x be
object ;
TARSKI:def 3 ( not x in rng R or x in dom (H ^ q) )
assume
x in rng R
;
x in dom (H ^ q)
then consider y being
object such that A62:
y in dom R
and A63:
R . y = x
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A62, FINSEQ_3:23;
y in dom (G ^ p)
by A54, A55, A62, FINSEQ_3:29;
then
(G ^ p) . y in rng (H ^ q)
by A16, A53, FUNCT_1:def 3;
then A64:
H ^ q just_once_values (G ^ p) . y
by A52, FINSEQ_4:8;
R . y = (H ^ q) <- ((G ^ p) . y)
by A56, A62;
hence
x in dom (H ^ q)
by A63, A64, FINSEQ_4:def 3;
verum
end;
then A66:
G ^ p = (H ^ q) * R
by A58, FUNCT_1:10;
dom (H ^ q) c= rng R
then A69:
dom (H ^ q) = rng R
by A61;
set h = L2 (#) (H ^ q);
A70: Sum (L2 (#) (H ^ q)) =
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 (L1 (#) (G ^ p)) =
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 (F ^ r)
by A20, FINSEQ_3:29;
then A73:
P is one-to-one
by A34, FINSEQ_4:60;
A74:
dom R = dom (H ^ q)
by A55, FINSEQ_3:29;
then A75:
R is one-to-one
by A69, FINSEQ_4:60;
reconsider R = R as Function of (dom (H ^ q)),(dom (H ^ q)) by A61, A74, FUNCT_2:2;
reconsider R = R as Permutation of (dom (H ^ q)) by A69, A75, FUNCT_2:57;
A76:
len (L2 (#) (H ^ q)) = len (H ^ q)
by Def5;
then
dom (L2 (#) (H ^ q)) = dom (H ^ q)
by FINSEQ_3:29;
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:47;
A77:
len Hp = len (G ^ p)
by A54, A76, FINSEQ_2:44;
reconsider P = P as Function of (dom (F ^ r)),(dom (F ^ r)) by A26, A72, FUNCT_2:2;
reconsider P = P as Permutation of (dom (F ^ r)) by A34, A73, FUNCT_2:57;
A78:
len ((L1 + L2) (#) (F ^ r)) = len (F ^ r)
by Def5;
then
dom ((L1 + L2) (#) (F ^ r)) = dom (F ^ r)
by FINSEQ_3:29;
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:47;
A79: Sum ((L1 + L2) (#) (F ^ r)) =
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 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;
then A83:
for k being Nat st k in Seg (len (G ^ p)) holds
I . k = H3(k)
by A81;
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 A19, A78, A80, FINSEQ_2:44;
A87:
now for x being object st x in Seg (len I) holds
I . x = Fp . xlet x be
object ;
( x in Seg (len I) implies I . x = Fp . x )assume A88:
x in Seg (len I)
;
I . x = Fp . xthen reconsider k =
x as
Element of
NAT ;
A89:
x in dom Hp
by A80, A77, A88, FINSEQ_1:def 3;
then A90:
Hp /. k =
((L2 (#) (H ^ q)) * R) . k
by PARTFUN1:def 6
.=
(L2 (#) (H ^ q)) . (R . k)
by A89, FUNCT_1:12
;
set v =
(G ^ p) /. k;
x in dom Fp
by A86, A88, FINSEQ_1:def 3;
then A91:
Fp . k = ((L1 + L2) (#) (F ^ r)) . (P . k)
by FUNCT_1:12;
A92:
x in dom (H ^ q)
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 (G ^ p)
by A80, A88, FINSEQ_1:def 3;
then A94:
(H ^ q) . j =
(G ^ p) . k
by A58
.=
(G ^ p) /. k
by A93, PARTFUN1:def 6
;
A95:
dom (F ^ r) = dom (G ^ p)
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:
(F ^ r) . l =
(G ^ p) . k
by A23, A93
.=
(G ^ p) /. k
by A93, PARTFUN1:def 6
;
R . k in dom (H ^ q)
by A69, A74, A92, FUNCT_1:def 3;
then A97:
(L2 (#) (H ^ q)) . j = (L2 . ((G ^ p) /. k)) * ((G ^ p) /. k)
by A94, Th8;
P . k in dom (F ^ r)
by A34, A72, A93, A95, FUNCT_1:def 3;
then A98:
((L1 + L2) (#) (F ^ r)) . l =
((L1 + L2) . ((G ^ p) /. k)) * ((G ^ p) /. k)
by A96, Th8
.=
((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) * ((G ^ p) /. k)
by Th22
.=
((L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)) + ((L2 . ((G ^ p) /. k)) * ((G ^ p) /. k))
by VECTSP_1:def 15
;
A99:
x in dom (L1 (#) (G ^ p))
by A80, A47, A88, FINSEQ_1:def 3;
then (L1 (#) (G ^ p)) /. k =
(L1 (#) (G ^ p)) . k
by PARTFUN1:def 6
.=
(L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)
by A99, Def5
;
hence
I . x = Fp . x
by A80, A81, A82, A88, A90, A97, A91, A98;
verum 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 ((L1 + L2) (#) (F ^ r)) & Sum Hp = Sum (L2 (#) (H ^ q)) )
by RLVECT_2:7;
hence
Sum (L1 + L2) = (Sum L1) + (Sum L2)
by A11, A14, A51, A71, A70, A79, A80, A83, A77, A47, A100, A48, RLVECT_2:2; verum