let F be Field; for V, W being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @ l) (#) (T * G)
let V, W be VectSp of F; for T being linear-transformation of V,W
for l being Linear_Combination of V
for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @ l) (#) (T * G)
let T be linear-transformation of V,W; for l being Linear_Combination of V
for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @ l) (#) (T * G)
let l be Linear_Combination of V; for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @ l) (#) (T * G)
let G be FinSequence of V; ( rng G = Carrier l & T | (Carrier l) is one-to-one implies T * (l (#) G) = (T @ l) (#) (T * G) )
assume that
A1:
rng G = Carrier l
and
A2:
T | (Carrier l) is one-to-one
; T * (l (#) G) = (T @ l) (#) (T * G)
reconsider R = (T @ l) (#) (T * G) as FinSequence of W ;
reconsider L = T * (l (#) G) as FinSequence of W ;
A3: len R =
len (T * G)
by VECTSP_6:def 5
.=
len G
by FINSEQ_2:33
;
A4: len L =
len (l (#) G)
by FINSEQ_2:33
.=
len G
by VECTSP_6:def 5
;
for k being Nat st 1 <= k & k <= len L holds
L . k = R . k
proof
A5:
dom R = Seg (len G)
by A3, FINSEQ_1:def 3;
let k be
Nat;
( 1 <= k & k <= len L implies L . k = R . k )
assume A6:
( 1
<= k &
k <= len L )
;
L . k = R . k
reconsider gk =
G /. k as
Element of
V ;
len (l (#) G) = len G
by VECTSP_6:def 5;
then A7:
dom (l (#) G) = Seg (len G)
by FINSEQ_1:def 3;
A8:
k in dom (l (#) G)
by A4, A6, A7;
then A9:
k in dom G
by A7, FINSEQ_1:def 3;
then A10:
G . k = G /. k
by PARTFUN1:def 6;
then reconsider Gk =
G . k as
Element of
V ;
(T * G) . k = T . Gk
by A9, FUNCT_1:13;
then reconsider TGk =
(T * G) . k as
Element of
W ;
(l (#) G) . k = (l . gk) * gk
by A8, VECTSP_6:def 5;
then A11:
L . k =
T . ((l . gk) * gk)
by A8, FUNCT_1:13
.=
(l . gk) * (T . gk)
by MOD_2:def 2
.=
(l . Gk) * TGk
by A9, A10, FUNCT_1:13
;
(
G . k in rng G &
(T * G) . k = T . (G . k) )
by A9, FUNCT_1:3, FUNCT_1:13;
then A12:
(T @ l) . ((T * G) . k) = l . (G . k)
by A1, A2, Th37;
dom T = [#] V
by Th7;
then
dom (T * G) = dom G
by A1, RELAT_1:27;
then
(T * G) /. k = (T * G) . k
by A9, PARTFUN1:def 6;
hence
L . k = R . k
by A7, A8, A11, A5, A12, VECTSP_6:def 5;
verum
end;
hence
T * (l (#) G) = (T @ l) (#) (T * G)
by A4, A3; verum