let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K st n > 0 holds
M1 - (M1 @) is antisymmetric
let K be Field; :: thesis: for M1 being Matrix of n,K st n > 0 holds
M1 - (M1 @) is antisymmetric
let M1 be Matrix of n,K; :: thesis: ( n > 0 implies M1 - (M1 @) is antisymmetric )
assume A1: n > 0 ; :: thesis: M1 - (M1 @) is antisymmetric
set M2 = M1 - (M1 @);
A2: ( len M1 = n & width M1 = n ) by MATRIX_0:24;
A3: ( len (M1 @) = n & width (M1 @) = n ) by MATRIX_0:24;
(M1 - (M1 @)) @ = (M1 @) + ((- (M1 @)) @) by Th24
.= (M1 @) + (- ((M1 @) @)) by Th27
.= (M1 @) - M1 by A1, A2, MATRIX_0:57
.= - (M1 - (M1 @)) by A2, A3, MATRIX_4:43 ;
hence M1 - (M1 @) is antisymmetric ; :: thesis: verum