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

assume A1: M1 = a * M ; :: thesis: M1 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 M1 & k = (n + 1) - j & l = (n + 1) - i implies M1 * (i,j) = - (M1 * (k,l)) )

assume that

A3: [i,j] in Indices M1 and

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

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

then ( k in Seg n & l in Seg n ) by A3, A4, Lm2;

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

A6: [i,j] in Indices M by A2, A3, MATRIX_0:24;

then (a * M) * (i,j) = a * (M * (i,j)) by MATRIX_3:def 5

.= a * (- (M * (k,l))) by A4, A6, Def2

.= - (a * (M * (k,l))) by VECTSP_1:8

.= - ((a * M) * (k,l)) by A2, A5, MATRIX_3:def 5 ;

hence M1 * (i,j) = - (M1 * (k,l)) by A1; :: thesis: verum

assume A1: M1 = a * M ; :: thesis: M1 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 M1 & k = (n + 1) - j & l = (n + 1) - i implies M1 * (i,j) = - (M1 * (k,l)) )

assume that

A3: [i,j] in Indices M1 and

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

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

then ( k in Seg n & l in Seg n ) by A3, A4, Lm2;

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

A6: [i,j] in Indices M by A2, A3, MATRIX_0:24;

then (a * M) * (i,j) = a * (M * (i,j)) by MATRIX_3:def 5

.= a * (- (M * (k,l))) by A4, A6, Def2

.= - (a * (M * (k,l))) by VECTSP_1:8

.= - ((a * M) * (k,l)) by A2, A5, MATRIX_3:def 5 ;

hence M1 * (i,j) = - (M1 * (k,l)) by A1; :: thesis: verum