let i, j be Nat; for M being Matrix of COMPLEX st [i,j] in Indices M holds
(- M) * (i,j) = - (M * (i,j))
let M be Matrix of COMPLEX; ( [i,j] in Indices M implies (- M) * (i,j) = - (M * (i,j)) )
A1: COMPLEX2Field (- M) =
COMPLEX2Field (Field2COMPLEX (- (COMPLEX2Field M)))
by MATRIX_5:def 4
.=
- (COMPLEX2Field M)
by MATRIX_5:6
;
reconsider m = COMPLEX2Field (- M) as Matrix of COMPLEX by COMPLFLD:def 1;
reconsider m1 = COMPLEX2Field M as Matrix of COMPLEX by COMPLFLD:def 1;
A2: M * (i,j) =
m1 * (i,j)
by MATRIX_5:def 1
.=
(COMPLEX2Field M) * (i,j)
by COMPLFLD:def 1
;
assume
[i,j] in Indices M
; (- M) * (i,j) = - (M * (i,j))
then A3:
[i,j] in Indices (COMPLEX2Field M)
by MATRIX_5:def 1;
(- M) * (i,j) =
m * (i,j)
by MATRIX_5:def 1
.=
(- (COMPLEX2Field M)) * (i,j)
by A1, COMPLFLD:def 1
.=
- ((COMPLEX2Field M) * (i,j))
by A3, MATRIX_3:def 2
;
hence
(- M) * (i,j) = - (M * (i,j))
by A2, COMPLFLD:2; verum