let K be Fanoian Field; 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; 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; ( 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
; 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; verum