let x be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(- x) * A = - (x * A)
let A be Matrix of REAL; :: thesis: ( len A = len x & len x > 0 & width A > 0 implies (- x) * A = - (x * A) )
assume that
A1: len A = len x and
A2: len x > 0 and
A3: width A > 0 ; :: thesis: (- x) * A = - (x * A)
A4: (A @) * x = x * A by A1, A2, A3, MATRIXR1:52;
A5: width (A @) = len x by A1, A3, MATRIX_0:54;
then A6: (A @) * (- x) = (- 1) * ((A @) * x) by A2, MATRIXR1:59;
A7: len (- x) = len x by RVSUM_1:114;
len (A @) > 0 by A3, MATRIX_0:54;
then (- x) * ((A @) @) = (A @) * (- x) by A2, A5, A7, MATRIXR1:53;
hence (- x) * A = - (x * A) by A1, A2, A3, A6, A4, MATRIX_0:57; :: thesis: verum