let K be Ring; for V, W being LeftMod of K
for T being linear-transformation of V,W
for s being Vector of W
for A being Subset of V
for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds
T . v = s ) holds
T . (Sum l) = (Sum (lCFST (l,T,s))) * s
let V, W be LeftMod of K; for T being linear-transformation of V,W
for s being Vector of W
for A being Subset of V
for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds
T . v = s ) holds
T . (Sum l) = (Sum (lCFST (l,T,s))) * s
let T be linear-transformation of V,W; for s being Vector of W
for A being Subset of V
for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds
T . v = s ) holds
T . (Sum l) = (Sum (lCFST (l,T,s))) * s
let s be Vector of W; for A being Subset of V
for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds
T . v = s ) holds
T . (Sum l) = (Sum (lCFST (l,T,s))) * s
A1:
T is additive
;
defpred S1[ Nat] means for A being Subset of V
for l being Linear_Combination of A st card (Carrier l) = $1 & ( for v being Vector of V st v in Carrier l holds
T . v = s ) holds
T . (Sum l) = (Sum (lCFST (l,T,s))) * s;
reconsider SZ0 = {(0. K)} as finite Subset of K ;
A2:
S1[ 0 ]
proof
let A be
Subset of
V;
for l being Linear_Combination of A st card (Carrier l) = 0 & ( for v being Vector of V st v in Carrier l holds
T . v = s ) holds
T . (Sum l) = (Sum (lCFST (l,T,s))) * slet l be
Linear_Combination of
A;
( card (Carrier l) = 0 & ( for v being Vector of V st v in Carrier l holds
T . v = s ) implies T . (Sum l) = (Sum (lCFST (l,T,s))) * s )
assume
(
card (Carrier l) = 0 & ( for
v being
Vector of
V st
v in Carrier l holds
T . v = s ) )
;
T . (Sum l) = (Sum (lCFST (l,T,s))) * s
then A3:
Carrier l = {}
;
then A4:
T . (Sum l) =
T . (0. V)
by VECTSP_6:19
.=
T . ((0. K) * (0. V))
by VECTSP_1:14
.=
(0. K) * (T . (0. V))
by MOD_2:def 2
.=
0. W
by VECTSP_1:14
;
set g =
canFS ((T " {s}) /\ (Carrier l));
lCFST (
l,
T,
s)
= <*> the
carrier of
K
by A3;
then
Sum (lCFST (l,T,s)) = 0. K
by RLVECT_1:43;
hence
T . (Sum l) = (Sum (lCFST (l,T,s))) * s
by A4, VECTSP_1:14;
verum
end;
A5:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A6:
S1[
n]
;
S1[n + 1]
let A be
Subset of
V;
for l being Linear_Combination of A st card (Carrier l) = n + 1 & ( for v being Vector of V st v in Carrier l holds
T . v = s ) holds
T . (Sum l) = (Sum (lCFST (l,T,s))) * slet l be
Linear_Combination of
A;
( card (Carrier l) = n + 1 & ( for v being Vector of V st v in Carrier l holds
T . v = s ) implies T . (Sum l) = (Sum (lCFST (l,T,s))) * s )
assume A7:
(
card (Carrier l) = n + 1 & ( for
v being
Vector of
V st
v in Carrier l holds
T . v = s ) )
;
T . (Sum l) = (Sum (lCFST (l,T,s))) * s
then
Carrier l <> {}
;
then consider w being
object such that A8:
w in Carrier l
by XBOOLE_0:def 1;
reconsider w =
w as
Element of the
carrier of
V by A8;
A9:
card ((Carrier l) \ {w}) =
(card (Carrier l)) - (card {w})
by A8, CARD_2:44, ZFMISC_1:31
.=
(n + 1) - 1
by A7, CARD_2:42
.=
n
;
reconsider A0 =
(Carrier l) \ {w} as
finite Subset of
V ;
reconsider B0 =
{w} as
finite Subset of
V ;
defpred S2[
object ,
object ]
means ( not $1 is
Vector of
V or ( $1
in A0 & $2
= l . $1 ) or ( not $1
in A0 & $2
= 0. K ) );
A10:
for
x being
object st
x in the
carrier of
V holds
ex
y being
object st
(
y in the
carrier of
K &
S2[
x,
y] )
consider l0 being
Function of the
carrier of
V, the
carrier of
K such that A13:
for
x being
object st
x in the
carrier of
V holds
S2[
x,
l0 . x]
from FUNCT_2:sch 1(A10);
A14:
for
v being
Vector of
V st not
v in A0 holds
l0 . v = 0. K
by A13;
reconsider l0 =
l0 as
Element of
Funcs ( the
carrier of
V, the
carrier of
K)
by FUNCT_2:8;
reconsider l0 =
l0 as
Linear_Combination of
V by A14, VECTSP_6:def 1;
A15:
for
x being
object holds
(
x in A0 iff
x in Carrier l0 )
then A19:
Carrier l0 = A0
by TARSKI:2;
then reconsider l0 =
l0 as
Linear_Combination of
A0 by VECTSP_6:def 4;
A20:
l0 | (Carrier l0) = l | (Carrier l0)
defpred S3[
object ,
object ]
means ( not $1 is
Vector of
V or ( $1
in B0 & $2
= l . $1 ) or ( not $1
in B0 & $2
= 0. K ) );
A22:
for
x being
object st
x in the
carrier of
V holds
ex
y being
object st
(
y in the
carrier of
K &
S3[
x,
y] )
consider l1 being
Function of
V,
K such that A25:
for
x being
object st
x in the
carrier of
V holds
S3[
x,
l1 . x]
from FUNCT_2:sch 1(A22);
A26:
for
v being
Vector of
V st not
v in B0 holds
l1 . v = 0. K
by A25;
reconsider l1 =
l1 as
Element of
Funcs ( the
carrier of
V, the
carrier of
K)
by FUNCT_2:8;
reconsider l1 =
l1 as
Linear_Combination of
V by A26, VECTSP_6:def 1;
for
x being
object holds
(
x in B0 iff
x in Carrier l1 )
then
Carrier l1 = B0
by TARSKI:2;
then reconsider l1 =
l1 as
Linear_Combination of
B0 by VECTSP_6:def 4;
for
v being
Element of
V holds
l . v = (l0 + l1) . v
then
l = l0 + l1
;
then A39:
Sum l = (Sum l0) + (Sum l1)
by VECTSP_6:44;
for
v being
Vector of
V st
v in Carrier l0 holds
T . v = s
then A40:
T . (Sum l0) = (Sum (lCFST (l0,T,s))) * s
by A6, A9, A19;
A41:
A0 \/ B0 =
(Carrier l) \/ B0
by XBOOLE_1:39
.=
Carrier l
by A8, XBOOLE_1:12, ZFMISC_1:31
;
A42:
w in B0
by TARSKI:def 1;
A43:
T . (Sum l1) =
T . ((l1 . w) * w)
by VECTSP_6:17
.=
(l1 . w) * (T . w)
by MOD_2:def 2
.=
(l1 . w) * s
by A7, A8
.=
(l . w) * s
by A25, A42
.=
(Sum <*(l . w)*>) * s
by RLVECT_1:44
;
set WW =
(lCFST (l0,T,s)) ^ <*(l /. w)*>;
rng ((lCFST (l0,T,s)) ^ <*(l /. w)*>) = (rng (lCFST (l0,T,s))) \/ (rng <*(l /. w)*>)
by FINSEQ_1:31;
then reconsider WW =
(lCFST (l0,T,s)) ^ <*(l /. w)*> as
FinSequence of
K by FINSEQ_1:def 4;
reconsider L =
Sum WW as
Element of
K ;
A44:
(T " {s}) /\ (Carrier l) =
((T " {s}) /\ A0) \/ ((T " {s}) /\ B0)
by A41, XBOOLE_1:23
.=
((T " {s}) /\ (Carrier l0)) \/ ((T " {s}) /\ B0)
by A15, TARSKI:2
;
reconsider S1 =
(T " {s}) /\ (Carrier l0) as
finite Subset of
V ;
then
B0 c= T " {s}
;
then A47:
(T " {s}) /\ B0 = {w}
by XBOOLE_1:28;
reconsider S2 =
(T " {s}) /\ B0 as
finite Subset of the
carrier of
V ;
A48:
((Carrier l) \ {w}) /\ B0 =
(B0 /\ (Carrier l)) \ B0
by XBOOLE_1:49
.=
{}
by XBOOLE_1:17, XBOOLE_1:37
;
A49:
S1 /\ S2 =
(((T " {s}) /\ (Carrier l0)) /\ B0) /\ (T " {s})
by XBOOLE_1:16
.=
(((T " {s}) /\ ((Carrier l) \ {w})) /\ B0) /\ (T " {s})
by A15, TARSKI:2
.=
((T " {s}) /\ {}) /\ (T " {s})
by A48, XBOOLE_1:16
.=
{}
;
A50:
Carrier l0 c= Carrier l
by A19, XBOOLE_1:36;
reconsider ll =
l as
Function of the
carrier of
V, the
carrier of
K ;
A51:
l * (canFS S2) =
ll * <*w*>
by A47, FINSEQ_1:94
.=
<*(ll . w)*>
by FINSEQ_2:35
;
rng (l * (canFS S1)) c= the
carrier of
K
;
then reconsider l1 =
l * (canFS S1) as
FinSequence of
K by FINSEQ_1:def 4;
reconsider l2 =
l * (canFS S2) as
FinSequence of
K by A51;
rng (lCFST (l,T,s)) c= the
carrier of
K
;
then reconsider ll0 =
lCFST (
l,
T,
s) as
FinSequence of
K by FINSEQ_1:def 4;
A52:
Sum ll0 =
(Sum l1) + (Sum l2)
by A44, A49, ThTF3C2
.=
(Sum (lCFST (l0,T,s))) + (Sum <*(l . w)*>)
by A20, A50, A51, ThTF3C3, XBOOLE_1:17
;
thus T . (Sum l) =
((Sum (lCFST (l0,T,s))) * s) + ((Sum <*(l . w)*>) * s)
by A1, A39, A40, A43
.=
(Sum (lCFST (l,T,s))) * s
by A52, VECTSP_1:def 15
;
verum
end;
A53:
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A5);
let A be Subset of V; for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds
T . v = s ) holds
T . (Sum l) = (Sum (lCFST (l,T,s))) * s
let l be Linear_Combination of A; ( ( for v being Vector of V st v in Carrier l holds
T . v = s ) implies T . (Sum l) = (Sum (lCFST (l,T,s))) * s )
assume A54:
for v being Vector of V st v in Carrier l holds
T . v = s
; T . (Sum l) = (Sum (lCFST (l,T,s))) * s
card (Carrier l) is Nat
;
hence
T . (Sum l) = (Sum (lCFST (l,T,s))) * s
by A53, A54; verum