let K be Ring; :: thesis: for A, C being Matrix of K st width A = len C & len C > 0 holds
A * (- C) = - (A * C)
let A, C be Matrix of K; :: thesis: ( width A = len C & len C > 0 implies A * (- C) = - (A * C) )
assume that
A1: width A = len C and
A3: len C > 0 ; :: thesis: A * (- C) = - (A * C)
A4: len C = len (- C) by MATRIX_3:def 2;
then A5: len A = len (A * (- C)) by A1, MATRIX_3:def 4;
width (- C) = width C by MATRIX_3:def 2;
then A6: width (A * (- C)) = width C by A1, A4, MATRIX_3:def 4;
reconsider D = C as Matrix of len C, width C,K by A3, MATRIX_0:20;
A7: ( len (A * C) = len A & width (A * C) = width C ) by A1, MATRIX_3:def 4;
( len C = len (- C) & width (- C) = width C ) by MATRIX_3:def 2;
then (A * C) + (A * (- C)) = A * (D + (- D)) by A1, MATRIX_4:62
.= A * (0. (K,(len C),(width C))) by MATRIX_3:5
.= 0. (K,(len A),(width C)) by A1, A3, Th18 ;
hence A * (- C) = - (A * C) by A7, A5, A6, MATRIX_4:8; :: thesis: verum