let K be Fanoian Field; 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; 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; ( M1 is symmetric & M1 is antisymmetric implies M1 = 0. (K,n,n) )
assume
( M1 is symmetric & M1 is antisymmetric )
; 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
let i,
j be
Nat;
( [i,j] in Indices M1 implies M1 * (i,j) = (0. (K,n,n)) * (i,j) )
assume A2:
[i,j] in Indices M1
;
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;
verum
end;
hence
M1 = 0. (K,n,n)
by MATRIX_0:27; verum