let x be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len x = width A & len x > 0 holds
A * (- x) = - (A * x)
let A be Matrix of REAL; :: thesis: ( len x = width A & len x > 0 implies A * (- x) = - (A * x) )
assume that
A1: len x = width A and
A2: len x > 0 ; :: thesis: A * (- x) = - (A * x)
A3: len (ColVec2Mx x) = len x by A2, MATRIXR1:def 9;
width (ColVec2Mx x) = 1 by A2, MATRIXR1:def 9;
then A4: 1 <= width (A * (ColVec2Mx x)) by A1, A3, MATRIX_3:def 4;
thus A * (- x) = Col ((A * ((- 1) * (ColVec2Mx x))),1) by A2, MATRIXR1:47
.= Col (((- 1) * (A * (ColVec2Mx x))),1) by A1, A3, MATRIXR1:40
.= - (A * x) by A4, MATRIXR1:56 ; :: thesis: verum