let n be Nat; for a being Real
for M being Matrix of n,REAL
for x being FinSequence of REAL st n > 0 & len x = n holds
M * (a * x) = (a * M) * x
let a be Real; for M being Matrix of n,REAL
for x being FinSequence of REAL st n > 0 & len x = n holds
M * (a * x) = (a * M) * x
let M be Matrix of n,REAL; for x being FinSequence of REAL st n > 0 & len x = n holds
M * (a * x) = (a * M) * x
let x be FinSequence of REAL ; ( n > 0 & len x = n implies M * (a * x) = (a * M) * x )
assume that
A1:
n > 0
and
A2:
len x = n
; M * (a * x) = (a * M) * x
( width M = n & len M = n )
by MATRIX_0:24;
then A3:
( width M = len (ColVec2Mx x) & len M > 0 & len (ColVec2Mx x) > 0 & width (ColVec2Mx x) > 0 )
by A1, A2, MATRIXR1:def 9;
(a * M) * x =
Col (((a * M) * (ColVec2Mx x)),1)
by MATRIXR1:def 11
.=
Col ((a * (M * (ColVec2Mx x))),1)
by A3, MATRIXR1:41
.=
Col ((M * (a * (ColVec2Mx x))),1)
by A3, MATRIXR1:40
.=
Col ((M * (ColVec2Mx (a * x))),1)
by A1, A2, MATRIXR1:47
.=
M * (a * x)
by MATRIXR1:def 11
;
hence
M * (a * x) = (a * M) * x
; verum