let K be Fanoian Field; :: thesis: for n, i, j, k, l being Nat

for M1 being Matrix of n,K st [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric holds

M1 * (i,j) = 0. K

let n, i, j, k, l be Nat; :: thesis: for M1 being Matrix of n,K st [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric holds

M1 * (i,j) = 0. K

let M1 be Matrix of n,K; :: thesis: ( [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric implies M1 * (i,j) = 0. K )

assume that

A1: [i,j] in Indices M1 and

A2: ( i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i ) and

A3: M1 is Anti-subsymmetric ; :: thesis: M1 * (i,j) = 0. K

M1 * (i,j) = - (M1 * (i,j)) by A1, A3, A2;

then (M1 * (i,j)) + (M1 * (i,j)) = 0. K by RLVECT_1:5;

then ((1_ K) * (M1 * (i,j))) + (M1 * (i,j)) = 0. K ;

then ((1_ K) * (M1 * (i,j))) + ((1_ K) * (M1 * (i,j))) = 0. K ;

then ( (1_ K) + (1_ K) <> 0. K & ((1_ K) + (1_ K)) * (M1 * (i,j)) = 0. K ) by VECTSP_1:def 7, VECTSP_1:def 19;

hence M1 * (i,j) = 0. K by VECTSP_1:12; :: thesis: verum

for M1 being Matrix of n,K st [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric holds

M1 * (i,j) = 0. K

let n, i, j, k, l be Nat; :: thesis: for M1 being Matrix of n,K st [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric holds

M1 * (i,j) = 0. K

let M1 be Matrix of n,K; :: thesis: ( [i,j] in Indices M1 & i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i & M1 is Anti-subsymmetric implies M1 * (i,j) = 0. K )

assume that

A1: [i,j] in Indices M1 and

A2: ( i + j = n + 1 & k = (n + 1) - j & l = (n + 1) - i ) and

A3: M1 is Anti-subsymmetric ; :: thesis: M1 * (i,j) = 0. K

M1 * (i,j) = - (M1 * (i,j)) by A1, A3, A2;

then (M1 * (i,j)) + (M1 * (i,j)) = 0. K by RLVECT_1:5;

then ((1_ K) * (M1 * (i,j))) + (M1 * (i,j)) = 0. K ;

then ((1_ K) * (M1 * (i,j))) + ((1_ K) * (M1 * (i,j))) = 0. K ;

then ( (1_ K) + (1_ K) <> 0. K & ((1_ K) + (1_ K)) * (M1 * (i,j)) = 0. K ) by VECTSP_1:def 7, VECTSP_1:def 19;

hence M1 * (i,j) = 0. K by VECTSP_1:12; :: thesis: verum