let K be Fanoian Field; :: thesis: for n being Nat

for M1 being Matrix of n,K st M1 is symmetric & M1 is antisymmetric holds

M1 = 0. (K,n,n)

let n be Nat; :: thesis: for M1 being Matrix of n,K st M1 is symmetric & M1 is antisymmetric holds

M1 = 0. (K,n,n)

let M1 be Matrix of n,K; :: thesis: ( M1 is symmetric & M1 is antisymmetric implies M1 = 0. (K,n,n) )

assume ( M1 is symmetric & M1 is antisymmetric ) ; :: thesis: M1 = 0. (K,n,n)

then A1: ( M1 @ = M1 & M1 @ = - M1 ) ;

for i, j being Nat st [i,j] in Indices M1 holds

M1 * (i,j) = (0. (K,n,n)) * (i,j)

for M1 being Matrix of n,K st M1 is symmetric & M1 is antisymmetric holds

M1 = 0. (K,n,n)

let n be Nat; :: thesis: for M1 being Matrix of n,K st M1 is symmetric & M1 is antisymmetric holds

M1 = 0. (K,n,n)

let M1 be Matrix of n,K; :: thesis: ( M1 is symmetric & M1 is antisymmetric implies M1 = 0. (K,n,n) )

assume ( M1 is symmetric & M1 is antisymmetric ) ; :: thesis: M1 = 0. (K,n,n)

then A1: ( M1 @ = M1 & M1 @ = - M1 ) ;

for i, j being Nat st [i,j] in Indices M1 holds

M1 * (i,j) = (0. (K,n,n)) * (i,j)

proof

hence
M1 = 0. (K,n,n)
by MATRIX_0:27; :: thesis: verum
let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = (0. (K,n,n)) * (i,j) )

assume A2: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = (0. (K,n,n)) * (i,j)

then M1 * (i,j) = - (M1 * (i,j)) by A1, MATRIX_3:def 2;

then (M1 * (i,j)) + (M1 * (i,j)) = 0. K by RLVECT_1:5;

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;

then A3: M1 * (i,j) = 0. K by VECTSP_1:12;

[i,j] in Indices (0. (K,n,n)) by A2, MATRIX_0:26;

hence M1 * (i,j) = (0. (K,n,n)) * (i,j) by A3, MATRIX_3:1; :: thesis: verum

end;assume A2: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = (0. (K,n,n)) * (i,j)

then M1 * (i,j) = - (M1 * (i,j)) by A1, MATRIX_3:def 2;

then (M1 * (i,j)) + (M1 * (i,j)) = 0. K by RLVECT_1:5;

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;

then A3: M1 * (i,j) = 0. K by VECTSP_1:12;

[i,j] in Indices (0. (K,n,n)) by A2, MATRIX_0:26;

hence M1 * (i,j) = (0. (K,n,n)) * (i,j) by A3, MATRIX_3:1; :: thesis: verum