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

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