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