let n, m, i be Nat; for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds
((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
let f be n -element real-valued FinSequence; for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds
((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
let M be Matrix of n,m,F_Real; ( 1 <= i & i <= m & n <> 0 implies ((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i)) )
assume that
A1:
( 1 <= i & i <= m )
and
A2:
n <> 0
; ((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
A3:
len M = n
by A2, MATRIX13:1;
set Lf = LineVec2Mx (@ f);
set LfM = (LineVec2Mx (@ f)) * M;
len f = n
by CARD_1:def 7;
then A4:
width (LineVec2Mx (@ f)) = n
by MATRIX13:1;
width M = m
by A2, MATRIX13:1;
then A5:
width ((LineVec2Mx (@ f)) * M) = m
by A4, A3, MATRIX_3:def 4;
len (LineVec2Mx (@ f)) = 1
by MATRIX13:1;
then
len ((LineVec2Mx (@ f)) * M) = 1
by A4, A3, MATRIX_3:def 4;
then A6:
[1,i] in Indices ((LineVec2Mx (@ f)) * M)
by A1, A5, MATRIX_0:30;
set LM = Line (((LineVec2Mx (@ f)) * M),1);
( i in Seg m & (Mx2Tran M) . f = Line (((LineVec2Mx (@ f)) * M),1) )
by A1, A2, Def3;
hence ((Mx2Tran M) . f) . i =
((LineVec2Mx (@ f)) * M) * (1,i)
by A5, MATRIX_0:def 7
.=
(Line ((LineVec2Mx (@ f)),1)) "*" (Col (M,i))
by A4, A3, A6, MATRIX_3:def 4
.=
(@ f) "*" (Col (M,i))
by MATRIX15:25
;
verum