take M = (n,n) --> (0. K); :: thesis: M is Anti-subsymmetric

let i, j, k, l be Nat; :: according to MATRIX17:def 2 :: thesis: ( [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i implies M * (i,j) = - (M * (k,l)) )

assume that

A1: [i,j] in Indices M and

A2: ( k = (n + 1) - j & l = (n + 1) - i ) ; :: thesis: M * (i,j) = - (M * (k,l))

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

( k in Seg n & l in Seg n ) by A2, A1, A3, Lm2;

then [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;

then A4: M * (k,l) = 0. K by A3, MATRIX_0:46;

0. K = - (0. K) by RLVECT_1:12;

hence M * (i,j) = - (M * (k,l)) by A4, A1, MATRIX_0:46; :: thesis: verum

let i, j, k, l be Nat; :: according to MATRIX17:def 2 :: thesis: ( [i,j] in Indices M & k = (n + 1) - j & l = (n + 1) - i implies M * (i,j) = - (M * (k,l)) )

assume that

A1: [i,j] in Indices M and

A2: ( k = (n + 1) - j & l = (n + 1) - i ) ; :: thesis: M * (i,j) = - (M * (k,l))

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

( k in Seg n & l in Seg n ) by A2, A1, A3, Lm2;

then [k,l] in [:(Seg n),(Seg n):] by ZFMISC_1:87;

then A4: M * (k,l) = 0. K by A3, MATRIX_0:46;

0. K = - (0. K) by RLVECT_1:12;

hence M * (i,j) = - (M * (k,l)) by A4, A1, MATRIX_0:46; :: thesis: verum