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