let R be Ring; :: thesis: for V being RightMod of R
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
let V be RightMod of R; :: 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 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 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 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 V by A10, FINSEQ_1:def 4;
A12:
len p = len (L1 (#) p)
by Def8;
then A15: Sum (L1 (#) p) =
(Sum p) * (0. R)
by A12, Lm2
.=
0. V
by VECTSP_2:90
;
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:def 7
;
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 V by A17, FINSEQ_1:def 4;
A19:
len q = len (L2 (#) q)
by Def8;
then A22: Sum (L2 (#) q) =
(Sum q) * (0. R)
by A19, Lm2
.=
0. V
by VECTSP_2:90
;
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:def 7
;
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 V by A24, FINSEQ_1:def 4;
A26:
len r = len ((L1 + L2) (#) r)
by Def8;
then A29: Sum ((L1 + L2) (#) r) =
(Sum r) * (0. R)
by A26, Lm2
.=
0. V
by VECTSP_2:90
;
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:def 7
;
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;
then A40:
( dom (G ^ p) = dom (F ^ r) & dom (G ^ p) = dom (H ^ q) )
by FINSEQ_3:31;
deffunc H1( Nat) -> set = (F ^ r) <- ((G ^ p) . $1);
consider P being FinSequence such that
A41:
len P = len (F ^ r)
and
A42:
for k being Nat st k in dom P holds
P . k = H1(k)
from FINSEQ_1:sch 2();
A43:
dom P = Seg (len (F ^ r))
by A41, FINSEQ_1:def 3;
A44:
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 A45:
y in dom P
and A46:
P . y = x
by FUNCT_1:def 5;
reconsider y =
y as
Nat by A45, FINSEQ_3:25;
A47:
dom (F ^ r) = Seg (len (F ^ r))
by FINSEQ_1:def 3;
A48:
y in dom (F ^ r)
by A41, A45, FINSEQ_3:31;
then
(G ^ p) . y in rng (F ^ r)
by A38, A40, FUNCT_1:def 5;
then
(
P . y = (F ^ r) <- ((G ^ p) . y) &
F ^ r just_once_values (G ^ p) . y )
by A36, A42, A47, A48, A43, FINSEQ_4:10;
hence
x in dom (F ^ r)
by A46, FINSEQ_4:def 3;
:: thesis: verum
end;
then A53:
G ^ p = (F ^ r) * P
by A49, FUNCT_1:20;
dom (F ^ r) c= rng P
then A56:
dom (F ^ r) = rng P
by A44, XBOOLE_0:def 10;
A57:
dom P = dom (F ^ r)
by A41, FINSEQ_3:31;
then A58:
P is one-to-one
by A56, FINSEQ_4:75;
( dom (F ^ r) = {} implies dom (F ^ r) = {} )
;
then reconsider P = P as Function of (dom (F ^ r)),(dom (F ^ r)) by A44, A57, FUNCT_2:def 1, RELSET_1:11;
A59:
len ((L1 + L2) (#) (F ^ r)) = len (F ^ r)
by Def8;
then A60:
dom ((L1 + L2) (#) (F ^ r)) = dom (F ^ r)
by FINSEQ_3:31;
then reconsider P = P as Function of (dom ((L1 + L2) (#) (F ^ r))),(dom ((L1 + L2) (#) (F ^ r))) ;
reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of V by FINSEQ_2:51;
reconsider P = P as Permutation of (dom ((L1 + L2) (#) (F ^ r))) by A56, A58, A60, FUNCT_2:83;
A61:
Fp = ((L1 + L2) (#) (F ^ r)) * P
;
then A62:
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
A63:
len R = len (H ^ q)
and
A64:
for k being Nat st k in dom R holds
R . k = H2(k)
from FINSEQ_1:sch 2();
A65:
dom R = Seg (len (H ^ q))
by A63, FINSEQ_1:def 3;
A66:
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 A67:
y in dom R
and A68:
R . y = x
by FUNCT_1:def 5;
reconsider y =
y as
Nat by A67, FINSEQ_3:25;
A69:
dom (H ^ q) = Seg (len (H ^ q))
by FINSEQ_1:def 3;
A70:
y in dom (H ^ q)
by A63, A67, FINSEQ_3:31;
then
(G ^ p) . y in rng (H ^ q)
by A38, A40, FUNCT_1:def 5;
then
(
R . y = (H ^ q) <- ((G ^ p) . y) &
H ^ q just_once_values (G ^ p) . y )
by A36, A64, A69, A70, A65, FINSEQ_4:10;
hence
x in dom (H ^ q)
by A68, FINSEQ_4:def 3;
:: thesis: verum
end;
then A75:
G ^ p = (H ^ q) * R
by A71, FUNCT_1:20;
dom (H ^ q) c= rng R
then A78:
dom (H ^ q) = rng R
by A66, XBOOLE_0:def 10;
A79:
dom R = dom (H ^ q)
by A63, FINSEQ_3:31;
then A80:
R is one-to-one
by A78, FINSEQ_4:75;
( dom (H ^ q) = {} implies dom (H ^ q) = {} )
;
then reconsider R = R as Function of (dom (H ^ q)),(dom (H ^ q)) by A66, A79, FUNCT_2:def 1, RELSET_1:11;
A81:
len (L2 (#) (H ^ q)) = len (H ^ q)
by Def8;
then A82:
dom (L2 (#) (H ^ q)) = dom (H ^ q)
by FINSEQ_3:31;
then reconsider R = R as Function of (dom (L2 (#) (H ^ q))),(dom (L2 (#) (H ^ q))) ;
reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of V by FINSEQ_2:51;
reconsider R = R as Permutation of (dom (L2 (#) (H ^ q))) by A78, A80, A82, FUNCT_2:83;
A83:
Hp = (L2 (#) (H ^ q)) * R
;
then A84:
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
A85:
len I = len (G ^ p)
and
A86:
for k being Nat st k in dom I holds
I . k = H3(k)
from FINSEQ_1:sch 2();
A87:
dom I = Seg (len (G ^ p))
by A85, FINSEQ_1:def 3;
A88:
for k being Element of NAT st k in Seg (len (G ^ p)) holds
I . k = H3(k)
by A86, A87;
rng I c= the carrier of V
then reconsider I = I as FinSequence of V by FINSEQ_1:def 4;
A91:
len Fp = len I
by A39, A59, A61, A85, FINSEQ_2:48;
then A92:
( dom I = Seg (len I) & dom Fp = Seg (len I) )
by FINSEQ_1:def 3;
A93:
( len Hp = len (G ^ p) & len (L1 (#) (G ^ p)) = len (G ^ p) )
by A39, A81, A83, Def8, FINSEQ_2:48;
now let x be
set ;
:: thesis: ( x in Seg (len I) implies I . x = Fp . x )assume A94:
x in Seg (len I)
;
:: thesis: I . x = Fp . xthen A95:
(
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, A85, A91, A93, FINSEQ_1:def 3;
reconsider k =
x as
Element of
NAT by A94;
set v =
(G ^ p) /. k;
A96:
(L1 (#) (G ^ p)) /. k =
(L1 (#) (G ^ p)) . k
by A95, PARTFUN1:def 8
.=
((G ^ p) /. k) * (L1 . ((G ^ p) /. k))
by A95, Def8
;
A97:
Hp /. k =
((L2 (#) (H ^ q)) * R) . k
by A95, PARTFUN1:def 8
.=
(L2 (#) (H ^ q)) . (R . k)
by A95, FUNCT_1:22
;
A98:
R . k in dom R
by A78, A79, A95, FUNCT_1:def 5;
A99:
R . k in dom (H ^ q)
by A78, A79, A95, FUNCT_1:def 5;
reconsider j =
R . k as
Nat by A98, FINSEQ_3:25;
(H ^ q) . j =
(G ^ p) . k
by A72, A95
.=
(G ^ p) /. k
by A95, PARTFUN1:def 8
;
then A100:
(L2 (#) (H ^ q)) . j = ((G ^ p) /. k) * (L2 . ((G ^ p) /. k))
by A99, Th32;
A101:
P . k in dom P
by A40, A56, A57, A95, FUNCT_1:def 5;
A102:
P . k in dom (F ^ r)
by A40, A56, A57, A95, FUNCT_1:def 5;
reconsider l =
P . k as
Nat by A101, FINSEQ_3:25;
(F ^ r) . l =
(G ^ p) . k
by A50, A95
.=
(G ^ p) /. k
by A95, PARTFUN1:def 8
;
then A103:
((L1 + L2) (#) (F ^ r)) . l =
((G ^ p) /. k) * ((L1 + L2) . ((G ^ p) /. k))
by A102, Th32
.=
((G ^ p) /. k) * ((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k)))
by Def11
.=
(((G ^ p) /. k) * (L1 . ((G ^ p) /. k))) + (((G ^ p) /. k) * (L2 . ((G ^ p) /. k)))
by VECTSP_2:def 23
;
thus I . x =
(((G ^ p) /. k) * (L1 . ((G ^ p) /. k))) + (((G ^ p) /. k) * (L2 . ((G ^ p) /. k)))
by A85, A86, A94, A96, A97, A100, A87
.=
Fp . x
by A95, A103, FUNCT_1:22
;
:: thesis: verum end;
then A104:
I = Fp
by A92, FUNCT_1:9;
Seg (len (G ^ p)) = dom (L1 (#) (G ^ p))
by A93, FINSEQ_1:def 3;
hence
Sum (L1 + L2) = (Sum L1) + (Sum L2)
by A3, A6, A9, A16, A23, A30, A62, A84, A85, A88, A93, A104, RLVECT_2:4; :: thesis: verum