let n, m be Nat; for r being Real
for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
let r be Real; for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
let f be n -element real-valued FinSequence; for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
let M be Matrix of n,m,F_Real; (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
set rf = r * f;
set T = Mx2Tran M;
per cases
( n <> 0 or n = 0 )
;
suppose A1:
n <> 0
;
(Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)per cases
( m = 0 or m > 0 )
;
suppose
m > 0
;
(Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)reconsider R =
r as
Element of
F_Real by XREAL_0:def 1;
set Lr =
LineVec2Mx (@ (r * f));
set L =
LineVec2Mx (@ f);
A3:
R * (@ f) = @ (r * f)
by MATRIXR1:17;
len f = n
by CARD_1:def 7;
then A4:
width (LineVec2Mx (@ f)) = n
by MATRIX13:1;
A5:
len M = n
by A1, MATRIX13:1;
len (LineVec2Mx (@ f)) = 1
by MATRIX13:1;
then A6:
len ((LineVec2Mx (@ f)) * M) = 1
by A4, A5, MATRIX_3:def 4;
(Mx2Tran M) . (@ f) = Line (
((LineVec2Mx (@ f)) * M),1)
by A1, Def3;
hence r * ((Mx2Tran M) . f) =
R * (Line (((LineVec2Mx (@ f)) * M),1))
by MATRIXR1:17
.=
Line (
(R * ((LineVec2Mx (@ f)) * M)),1)
by A6, MATRIXR1:20
.=
Line (
((R * (LineVec2Mx (@ f))) * M),1)
by A4, A5, MATRIX15:1
.=
Line (
((LineVec2Mx (@ (r * f))) * M),1)
by A3, MATRIX15:29
.=
(Mx2Tran M) . (r * f)
by A1, Def3
;
verum end; end; end; end;