let R be Ring; for V being LeftMod of R
for A, B being finite Subset of V
for l being Linear_Combination of V
for l0, l1, l2 being FinSequence of R st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) holds
Sum l0 = (Sum l1) + (Sum l2)
let V be LeftMod of R; for A, B being finite Subset of V
for l being Linear_Combination of V
for l0, l1, l2 being FinSequence of R st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) holds
Sum l0 = (Sum l1) + (Sum l2)
let A, B be finite Subset of V; for l being Linear_Combination of V
for l0, l1, l2 being FinSequence of R st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) holds
Sum l0 = (Sum l1) + (Sum l2)
let l be Linear_Combination of V; for l0, l1, l2 being FinSequence of R st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) holds
Sum l0 = (Sum l1) + (Sum l2)
let l0, l1, l2 be FinSequence of R; ( A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) implies Sum l0 = (Sum l1) + (Sum l2) )
assume A1:
A /\ B = {}
; ( not l0 = l * (canFS (A \/ B)) or not l1 = l * (canFS A) or not l2 = l * (canFS B) or Sum l0 = (Sum l1) + (Sum l2) )
assume TT:
( l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) )
; Sum l0 = (Sum l1) + (Sum l2)
per cases
( A \/ B = {} or A \/ B <> {} )
;
suppose A5:
A \/ B <> {}
;
Sum l0 = (Sum l1) + (Sum l2)
rng (canFS A) = A
by FUNCT_2:def 3;
then reconsider ca =
canFS A as the
carrier of
V -valued FinSequence by RELAT_1:def 19;
rng (canFS B) = B
by FUNCT_2:def 3;
then reconsider cb =
canFS B as the
carrier of
V -valued FinSequence by RELAT_1:def 19;
set la =
len (canFS A);
set lb =
len (canFS B);
set lab =
len ((canFS A) ^ (canFS B));
set lavb =
len (canFS (A \/ B));
set F =
l * (canFS (A \/ B));
set G =
l1 ^ l2;
set H =
((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B));
A6:
len (canFS A) = card A
by FINSEQ_1:93;
A7:
len (canFS (A \/ B)) =
card (A \/ B)
by FINSEQ_1:93
.=
(card A) + (card B)
by A1, CARD_2:40, XBOOLE_0:def 7
.=
(len (canFS A)) + (len (canFS B))
by A6, FINSEQ_1:93
;
A8:
len ((canFS A) ^ (canFS B)) = (len (canFS A)) + (len (canFS B))
by FINSEQ_1:22;
then A9:
dom ((canFS A) ^ (canFS B)) = Seg ((len (canFS A)) + (len (canFS B)))
by FINSEQ_1:def 3;
A10:
rng ((canFS A) ^ (canFS B)) =
(rng (canFS A)) \/ (rng (canFS B))
by FINSEQ_1:31
.=
A \/ (rng (canFS B))
by FUNCT_2:def 3
.=
A \/ B
by FUNCT_2:def 3
;
reconsider AB =
(canFS A) ^ (canFS B) as
Function of
(Seg ((len (canFS A)) + (len (canFS B)))),
(A \/ B) by A9, A10, FUNCT_2:1;
A11:
rng (canFS (A \/ B)) = A \/ B
by FUNCT_2:def 3;
reconsider INVAB =
(canFS (A \/ B)) " as
Function of
(A \/ B),
(Seg (card (A \/ B))) by FINSEQ_1:95;
A12:
(
INVAB * (canFS (A \/ B)) = id (dom (canFS (A \/ B))) &
(canFS (A \/ B)) * INVAB = id (rng (canFS (A \/ B))) )
by FUNCT_1:39;
A13:
dom (canFS (A \/ B)) =
Seg (len (canFS (A \/ B)))
by FINSEQ_1:def 3
.=
Seg (card (A \/ B))
by FINSEQ_1:93
;
then A14:
canFS (A \/ B) is
Function of
(Seg (card (A \/ B))),
(A \/ B)
by A11, FUNCT_2:1;
A15:
dom INVAB = A \/ B
by A5, FUNCT_2:def 1;
A16:
rng INVAB =
Seg (card (A \/ B))
by A12, A13, A14, FUNCT_2:18
.=
Seg ((card A) + (card B))
by A1, CARD_2:40, XBOOLE_0:def 7
.=
Seg ((len (canFS A)) + (len (canFS B)))
by A6, FINSEQ_1:93
;
A17:
dom (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) =
dom ((canFS A) ^ (canFS B))
by A10, A15, RELAT_1:27
.=
Seg ((len (canFS A)) + (len (canFS B)))
by A8, FINSEQ_1:def 3
;
A18:
rng (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) = Seg ((len (canFS A)) + (len (canFS B)))
by A10, A15, A16, RELAT_1:28;
A19:
the
carrier of
V = dom l
by FUNCT_2:def 1;
A20:
dom (l * (canFS (A \/ B))) =
dom (canFS (A \/ B))
by A11, A19, RELAT_1:27
.=
Seg ((len (canFS A)) + (len (canFS B)))
by A7, FINSEQ_1:def 3
;
rng (canFS A) = A
by FUNCT_2:def 3;
then dom (l * (canFS A)) =
dom (canFS A)
by A19, RELAT_1:27
.=
Seg (len (canFS A))
by FINSEQ_1:def 3
;
then A21:
len (l * (canFS A)) = len (canFS A)
by FINSEQ_1:def 3;
A22:
rng (canFS B) = B
by FUNCT_2:def 3;
then dom (l * (canFS B)) =
dom (canFS B)
by A19, RELAT_1:27
.=
Seg (len (canFS B))
by FINSEQ_1:def 3
;
then A23:
len (l * (canFS B)) = len (canFS B)
by FINSEQ_1:def 3;
set G =
(l * (canFS A)) ^ (l * (canFS B));
A24:
len ((l * (canFS A)) ^ (l * (canFS B))) = (len (canFS A)) + (len (canFS B))
by A21, A23, FINSEQ_1:22;
rng (canFS A) misses rng (canFS B)
by A1, A22, FUNCT_2:def 3;
then A25:
(canFS A) ^ (canFS B) is
one-to-one
by FINSEQ_3:91;
A26:
dom (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) = dom ((l * (canFS A)) ^ (l * (canFS B)))
by A17, A24, FINSEQ_1:def 3;
A27:
(l * (canFS (A \/ B))) * (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) =
((l * (canFS (A \/ B))) * ((canFS (A \/ B)) ")) * ((canFS A) ^ (canFS B))
by RELAT_1:36
.=
(l * ((canFS (A \/ B)) * ((canFS (A \/ B)) "))) * ((canFS A) ^ (canFS B))
by RELAT_1:36
.=
(l * (id (rng (canFS (A \/ B))))) * ((canFS A) ^ (canFS B))
by FUNCT_1:39
.=
(l * (id (A \/ B))) * ((canFS A) ^ (canFS B))
by FUNCT_2:def 3
.=
l * ((id (A \/ B)) * AB)
by RELAT_1:36
.=
l * ((canFS A) ^ (canFS B))
by FUNCT_2:17
.=
(l * ca) ^ (l * cb)
by ThTF3C3
.=
(l * (canFS A)) ^ (l * (canFS B))
;
Z2:
rng ((l * (canFS A)) ^ (l * (canFS B))) = (rng (l * (canFS A))) \/ (rng (l * (canFS B)))
by FINSEQ_1:31;
rng (l * (canFS (A \/ B))) c= the
carrier of
R
;
then reconsider FR =
l * (canFS (A \/ B)) as
FinSequence of
R by FINSEQ_1:def 4;
reconsider GR =
(l * (canFS A)) ^ (l * (canFS B)) as
FinSequence of
R by Z2, FINSEQ_1:def 4;
thus Sum l0 =
Sum FR
by TT
.=
Sum GR
by A18, A20, A25, A26, A27, CLASSES1:77, RF9
.=
Sum (l1 ^ l2)
by TT
.=
(Sum (l * (canFS A))) + (Sum (l * (canFS B)))
by TT, RLVECT_1:41
.=
(Sum l1) + (Sum l2)
by TT
;
verum end;