let x, y be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len x = width A & len y = len x & len x > 0 & len A > 0 holds
A * (x - y) = (A * x) - (A * y)
let A be Matrix of REAL; :: thesis: ( len x = width A & len y = len x & len x > 0 & len A > 0 implies A * (x - y) = (A * x) - (A * y) )
assume that
A1: len x = width A and
A2: len y = len x and
A3: len x > 0 and
A4: len A > 0 ; :: thesis: A * (x - y) = (A * x) - (A * y)
A5: len (ColVec2Mx y) = len y by A2, A3, MATRIXR1:def 9;
A6: width (ColVec2Mx y) = 1 by A2, A3, MATRIXR1:def 9;
A7: len (ColVec2Mx x) = len x by A3, MATRIXR1:def 9;
then A8: len (A * (ColVec2Mx x)) = len A by A1, MATRIX_3:def 4
.= len (A * (ColVec2Mx y)) by A1, A2, A5, MATRIX_3:def 4 ;
A9: width (ColVec2Mx x) = 1 by A3, MATRIXR1:def 9;
then A10: 1 <= width (A * (ColVec2Mx x)) by A1, A7, MATRIX_3:def 4;
A11: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A7, MATRIX_3:def 4
.= width (ColVec2Mx y) by A3, A6, MATRIXR1:def 9
.= width (A * (ColVec2Mx y)) by A1, A2, A5, MATRIX_3:def 4 ;
thus A * (x - y) = Col ((A * ((ColVec2Mx x) - (ColVec2Mx y))),1) by A2, A3, Th24
.= Col (((A * (ColVec2Mx x)) - (A * (ColVec2Mx y))),1) by A1, A2, A3, A4, A7, A5, A9, A6, Th20
.= (A * x) - (A * y) by A8, A11, A10, Th26 ; :: thesis: verum