let N be Matrix of n,K; ( N = - M implies N is Anti-subsymmetric )
assume A1:
N = - M
; N is Anti-subsymmetric
A2:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
let i, j, k, l be Nat; MATRIX17:def 2 ( [i,j] in Indices N & k = (n + 1) - j & l = (n + 1) - i implies N * (i,j) = - (N * (k,l)) )
assume that
A3:
[i,j] in Indices N
and
A4:
( k = (n + 1) - j & l = (n + 1) - i )
; N * (i,j) = - (N * (k,l))
A5:
Indices (- M) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then
( i in Seg n & j in Seg n )
by A1, A3, ZFMISC_1:87;
then
( k in Seg n & l in Seg n )
by A4, Lm1;
then A6:
[k,l] in [:(Seg n),(Seg n):]
by ZFMISC_1:87;
(- M) * (i,j) =
- (M * (i,j))
by A1, A2, A3, A5, MATRIX_3:def 2
.=
- (- (M * (k,l)))
by A1, A2, A3, A5, A4, Def2
.=
- ((- M) * (k,l))
by A2, A6, MATRIX_3:def 2
;
hence
N * (i,j) = - (N * (k,l))
by A1; verum