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