let K be Fanoian Field; :: thesis: for n, i being Nat
for M1 being Matrix of n,K st M1 is antisymmetric & i in Seg n holds
M1 * i,i = 0. K
let n, i be Nat; :: thesis: for M1 being Matrix of n,K st M1 is antisymmetric & i in Seg n holds
M1 * i,i = 0. K
let M1 be Matrix of n,K; :: thesis: ( M1 is antisymmetric & i in Seg n implies M1 * i,i = 0. K )
A1: (1_ K) + (1_ K) <> 0. K by VECTSP_1:def 29;
assume A2: ( M1 is antisymmetric & i in Seg n ) ; :: thesis: M1 * i,i = 0. K
Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A3: [i,i] in Indices M1 by A2, ZFMISC_1:106;
A4: M1 @ = - M1 by A2, Def6;
(M1 @ ) * i,i = M1 * i,i by A3, MATRIX_1:def 7;
then M1 * i,i = - (M1 * i,i) by A3, A4, MATRIX_3:def 2;
then (M1 * i,i) + (M1 * i,i) = 0. K by RLVECT_1:16;
then ((1_ K) * (M1 * i,i)) + (M1 * i,i) = 0. K by VECTSP_1:def 19;
then ((1_ K) * (M1 * i,i)) + ((1_ K) * (M1 * i,i)) = 0. K by VECTSP_1:def 19;
then ((1_ K) + (1_ K)) * (M1 * i,i) = 0. K by VECTSP_1:def 18;
hence M1 * i,i = 0. K by A1, VECTSP_1:44; :: thesis: verum