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 )
assume that
A1: M1 is antisymmetric and
A2: i in Seg n ; :: thesis: M1 * (i,i) = 0. K
A3: M1 @ = - M1 by A1;
Indices M1 = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A4: [i,i] in Indices M1 by A2, ZFMISC_1:87;
then (M1 @) * (i,i) = M1 * (i,i) by MATRIX_0:def 6;
then M1 * (i,i) = - (M1 * (i,i)) by A4, A3, MATRIX_3:def 2;
then (M1 * (i,i)) + (M1 * (i,i)) = 0. K by RLVECT_1:5;
then ((1_ K) * (M1 * (i,i))) + ((1_ K) * (M1 * (i,i))) = 0. K ;
then ( (1_ K) + (1_ K) <> 0. K & ((1_ K) + (1_ K)) * (M1 * (i,i)) = 0. K ) by VECTSP_1:def 7, VECTSP_1:def 19;
hence M1 * (i,i) = 0. K by VECTSP_1:12; :: thesis: verum