let K be Ring; for V, W being LeftMod of K
for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds
T . (Sum l) = Sum Tl
let V, W be LeftMod of K; for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds
T . (Sum l) = Sum Tl
let T be linear-transformation of V,W; for A being Subset of V
for l being Linear_Combination of A
for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds
T . (Sum l) = Sum Tl
A1:
T is additive
;
A2:
dom T = the carrier of V
by FUNCT_2:def 1;
defpred S1[ Nat] means for A being Subset of V
for l being Linear_Combination of A
for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = $1 holds
T . (Sum l) = Sum Tl;
A3:
S1[ 0 ]
A6:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A21:
S1[
n]
;
S1[n + 1]
let A be
Subset of
V;
for l being Linear_Combination of A
for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = n + 1 holds
T . (Sum l) = Sum Tllet l be
Linear_Combination of
A;
for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l & card (T .: (Carrier l)) = n + 1 holds
T . (Sum l) = Sum Tllet Tl be
Linear_Combination of
T .: (Carrier l);
( Tl = T @* l & card (T .: (Carrier l)) = n + 1 implies T . (Sum l) = Sum Tl )
assume A7:
(
Tl = T @* l &
card (T .: (Carrier l)) = n + 1 )
;
T . (Sum l) = Sum Tl
then
T .: (Carrier l) <> {}
;
then consider w being
object such that A8:
w in T .: (Carrier l)
by XBOOLE_0:def 1;
reconsider w =
w as
Element of the
carrier of
W by A8;
A9:
card ((T .: (Carrier l)) \ {w}) =
(card (T .: (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) \ (T " {w}) as
finite Subset of
V ;
reconsider B0 =
(T " {w}) /\ (Carrier l) as
Subset of
V ;
reconsider B0 =
B0 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 the
carrier of
V, the
carrier of
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;
A27:
for
x being
object holds
(
x in B0 iff
x in Carrier l1 )
then A30:
Carrier l1 = B0
by TARSKI:2;
then reconsider l1 =
l1 as
Linear_Combination of
B0 by VECTSP_6:def 4;
A31:
l1 | (Carrier l1) = l | (Carrier l1)
A33:
for
v being
Element of
V holds
l . v = (l0 + l1) . v
then A42:
l = l0 + l1
;
reconsider Tl0 =
T @* l0 as
Linear_Combination of
T .: (Carrier l0) by LTh29;
reconsider Tl1 =
T @* l1 as
Linear_Combination of
T .: (Carrier l1) by LTh29;
A43:
(T .: (Carrier l0)) /\ (T .: (Carrier l1)) = {}
A49:
T .: (Carrier l) c= T .: ((Carrier l1) \/ (Carrier l0))
by A42, RELAT_1:123, VECTSP_6:23;
A50:
for
w being
Vector of
W st
w in T .: (Carrier l0) holds
Tl . w = Tl0 . w
proof
let v be
Vector of
W;
( v in T .: (Carrier l0) implies Tl . v = Tl0 . v )
assume
v in T .: (Carrier l0)
;
Tl . v = Tl0 . v
then consider x being
object such that A51:
(
x in the
carrier of
V &
x in Carrier l0 &
v = T . x )
by FUNCT_2:64;
reconsider x =
x as
Vector of
V by A51;
A52:
Tl0 . v = Sum (lCFST (l0,T,v))
by LDef5;
A53:
Tl . v = Sum (lCFST (l,T,v))
by A7, LDef5;
A54:
Carrier l0 c= Carrier l
by A19, XBOOLE_1:36;
then
(T " {v}) /\ (Carrier l) c= (T " {v}) /\ (Carrier l0)
;
then A57:
(T " {v}) /\ (Carrier l0) = (T " {v}) /\ (Carrier l)
by A19, XBOOLE_1:26, XBOOLE_1:36;
reconsider XX =
(T " {v}) /\ (Carrier l0) as
finite Subset of
V ;
thus
Tl . v = Tl0 . v
by A20, A52, A53, A54, A57, ThTF3C3, XBOOLE_1:17;
verum
end;
A58:
for
w being
Vector of
W st
w in T .: (Carrier l1) holds
Tl . w = Tl1 . w
proof
let v be
Vector of
W;
( v in T .: (Carrier l1) implies Tl . v = Tl1 . v )
assume
v in T .: (Carrier l1)
;
Tl . v = Tl1 . v
then consider x being
object such that A59:
(
x in the
carrier of
V &
x in Carrier l1 &
v = T . x )
by FUNCT_2:64;
reconsider x =
x as
Vector of
V by A59;
A60:
Tl1 . v = Sum (lCFST (l1,T,v))
by LDef5;
A61:
Tl . v = Sum (lCFST (l,T,v))
by A7, LDef5;
A62:
Carrier l1 c= Carrier l
by A30, XBOOLE_1:17;
then
(T " {v}) /\ (Carrier l) c= (T " {v}) /\ (Carrier l1)
;
then A66:
(T " {v}) /\ (Carrier l1) = (T " {v}) /\ (Carrier l)
by A30, XBOOLE_1:17, XBOOLE_1:26;
reconsider XX =
(T " {v}) /\ (Carrier l1) as
finite Subset of
V ;
thus
Tl . v = Tl1 . v
by A31, A60, A61, A62, A66, ThTF3C3, XBOOLE_1:17;
verum
end;
A67:
for
x being
object st
x in Carrier Tl0 holds
x in Carrier Tl
A70:
for
x being
object st
x in Carrier Tl1 holds
x in Carrier Tl
A73:
T .: (Carrier l0) = T .: ((Carrier l) \ (T " {w}))
by A15, TARSKI:2;
then A74:
(T .: (Carrier l)) \ (T .: (T " {w})) c= T .: (Carrier l0)
by RELAT_1:122;
A75:
T .: (Carrier l) c= T .: (dom T)
by RELAT_1:114;
A76:
T .: (Carrier l) c= rng T
by A75, RELAT_1:113;
for
x being
object st
x in T .: (Carrier l0) holds
x in (T .: (Carrier l)) \ {w}
then
T .: (Carrier l0) c= (T .: (Carrier l)) \ {w}
;
then A80:
T .: (Carrier l0) = (T .: (Carrier l)) \ {w}
by A8, A74, A76, FUNCT_1:77, ZFMISC_1:31;
for
y being
object st
y in Carrier Tl1 holds
y in {w}
then A87:
Carrier Tl1 c= {w}
;
A88:
T . (Sum l1) = Sum Tl1
for
w being
Element of
W holds
Tl . w = (Tl0 + Tl1) . w
then A102:
Tl = Tl0 + Tl1
;
l = l0 + l1
by A33;
hence T . (Sum l) =
T . ((Sum l0) + (Sum l1))
by VECTSP_6:44
.=
(T . (Sum l0)) + (T . (Sum l1))
by A1
.=
(Sum Tl0) + (Sum Tl1)
by A9, A21, A80, A88
.=
Sum Tl
by A102, VECTSP_6:44
;
verum
end;
A103:
for n being Nat holds S1[n]
from NAT_1:sch 2(A3, A6);
let A be Subset of V; for l being Linear_Combination of A
for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds
T . (Sum l) = Sum Tl
let l be Linear_Combination of A; for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds
T . (Sum l) = Sum Tl
let Tl be Linear_Combination of T .: (Carrier l); ( Tl = T @* l implies T . (Sum l) = Sum Tl )
assume A104:
Tl = T @* l
; T . (Sum l) = Sum Tl
card (T .: (Carrier l)) is Nat
;
hence
T . (Sum l) = Sum Tl
by A103, A104; verum