let F be Field; for V, W being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds
T . (Sum l) = Sum (T @ l)
let V, W be VectSp of F; for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds
T . (Sum l) = Sum (T @ l)
let T be linear-transformation of V,W; for A being Subset of V
for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds
T . (Sum l) = Sum (T @ l)
let A be Subset of V; for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds
T . (Sum l) = Sum (T @ l)
let B be Basis of V; for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds
T . (Sum l) = Sum (T @ l)
let l be Linear_Combination of B \ A; ( A is Basis of (ker T) & A c= B implies T . (Sum l) = Sum (T @ l) )
assume
( A is Basis of (ker T) & A c= B )
; T . (Sum l) = Sum (T @ l)
then A1:
T | (B \ A) is one-to-one
by Th22;
Carrier l c= B \ A
by VECTSP_6:def 4;
then A2:
(T | (B \ A)) | (Carrier l) = T | (Carrier l)
by RELAT_1:74;
then A3:
T | (Carrier l) is one-to-one
by A1, FUNCT_1:52;
consider G being FinSequence of V such that
A4:
G is one-to-one
and
A5:
rng G = Carrier l
and
A6:
Sum l = Sum (l (#) G)
by VECTSP_6:def 6;
set H = T * G;
reconsider H = T * G as FinSequence of W ;
A7: rng H =
T .: (Carrier l)
by A5, RELAT_1:127
.=
Carrier (T @ l)
by A3, Th39
;
dom T = [#] V
by Th7;
then
H is one-to-one
by A4, A5, A1, A2, Th1, FUNCT_1:52;
then A8:
Sum (T @ l) = Sum ((T @ l) (#) H)
by A7, VECTSP_6:def 6;
T * (l (#) G) = (T @ l) (#) H
by A5, A3, Th38;
hence
T . (Sum l) = Sum (T @ l)
by A6, A8, MATRLIN:16; verum