let N be Matrix of n,K; :: thesis: ( N = - M implies N is Anti-subsymmetric )

assume A1: N = - M ; :: thesis: N is Anti-subsymmetric

A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;

let i, j, k, l be Nat; :: according to MATRIX17:def 2 :: thesis: ( [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 ) ; :: thesis: 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; :: thesis: verum

assume A1: N = - M ; :: thesis: N is Anti-subsymmetric

A2: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;

let i, j, k, l be Nat; :: according to MATRIX17:def 2 :: thesis: ( [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 ) ; :: thesis: 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; :: thesis: verum