let K be Field; :: thesis: for V, W being finite-dimensional VectSp of K
for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W
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 finite-dimensional VectSp of K; :: thesis: for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W
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; :: thesis: for B being Basis of V
for T being linear-transformation of V,W
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; :: thesis: for T being linear-transformation of V,W
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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: T . (Sum l) = Sum (T @* l)
then A1: T | (B \ A) is one-to-one by RANKNULL:22;
A2: (T | (B \ A)) | (Carrier l) = T | (Carrier l) by RELAT_1:74, VECTSP_6:def 4;
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;
A7: rng (T * G) = T .: (Carrier l) by A5, RELAT_1:127
.= Carrier (T @* l) by A3, ZMODUL05:56 ;
dom T = [#] V by RANKNULL:7;
then T * G is one-to-one by A1, A2, A4, A5, FUNCT_1:52, RANKNULL:1;
then A8: Sum (T @* l) = Sum ((T @* l) (#) (T * G)) by A7, VECTSP_6:def 6;
T * (l (#) G) = (T @* l) (#) (T * G) by A3, A5, ZMODUL05:55;
hence T . (Sum l) = Sum (T @* l) by A6, A8, MATRLIN:16; :: thesis: verum