let K be Field; :: thesis: for n being Nat

for M1 being Matrix of n,K holds (- M1) @ = - (M1 @)

let n be Nat; :: thesis: for M1 being Matrix of n,K holds (- M1) @ = - (M1 @)

let M1 be Matrix of n,K; :: thesis: (- M1) @ = - (M1 @)

for i, j being Nat st [i,j] in Indices ((- M1) @) holds

((- M1) @) * (i,j) = (- (M1 @)) * (i,j)

for M1 being Matrix of n,K holds (- M1) @ = - (M1 @)

let n be Nat; :: thesis: for M1 being Matrix of n,K holds (- M1) @ = - (M1 @)

let M1 be Matrix of n,K; :: thesis: (- M1) @ = - (M1 @)

for i, j being Nat st [i,j] in Indices ((- M1) @) holds

((- M1) @) * (i,j) = (- (M1 @)) * (i,j)

proof

hence
(- M1) @ = - (M1 @)
by MATRIX_0:27; :: thesis: verum
let i, j be Nat; :: thesis: ( [i,j] in Indices ((- M1) @) implies ((- M1) @) * (i,j) = (- (M1 @)) * (i,j) )

assume A1: [i,j] in Indices ((- M1) @) ; :: thesis: ((- M1) @) * (i,j) = (- (M1 @)) * (i,j)

then A2: [i,j] in Indices (M1 @) by MATRIX_0:26;

[i,j] in [:(Seg n),(Seg n):] by A1, MATRIX_0:24;

then ( i in Seg n & j in Seg n ) by ZFMISC_1:87;

then A3: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;

then A4: [j,i] in Indices M1 by MATRIX_0:24;

[j,i] in Indices (- M1) by A3, MATRIX_0:24;

then ((- M1) @) * (i,j) = (- M1) * (j,i) by MATRIX_0:def 6

.= - (M1 * (j,i)) by A4, MATRIX_3:def 2

.= - ((M1 @) * (i,j)) by A4, MATRIX_0:def 6

.= (- (M1 @)) * (i,j) by A2, MATRIX_3:def 2 ;

hence ((- M1) @) * (i,j) = (- (M1 @)) * (i,j) ; :: thesis: verum

end;assume A1: [i,j] in Indices ((- M1) @) ; :: thesis: ((- M1) @) * (i,j) = (- (M1 @)) * (i,j)

then A2: [i,j] in Indices (M1 @) by MATRIX_0:26;

[i,j] in [:(Seg n),(Seg n):] by A1, MATRIX_0:24;

then ( i in Seg n & j in Seg n ) by ZFMISC_1:87;

then A3: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;

then A4: [j,i] in Indices M1 by MATRIX_0:24;

[j,i] in Indices (- M1) by A3, MATRIX_0:24;

then ((- M1) @) * (i,j) = (- M1) * (j,i) by MATRIX_0:def 6

.= - (M1 * (j,i)) by A4, MATRIX_3:def 2

.= - ((M1 @) * (i,j)) by A4, MATRIX_0:def 6

.= (- (M1 @)) * (i,j) by A2, MATRIX_3:def 2 ;

hence ((- M1) @) * (i,j) = (- (M1 @)) * (i,j) ; :: thesis: verum