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_1:25;
A3: ( len (M1 @ ) = n & width (M1 @ ) = n ) by MATRIX_1:25;
(M1 - (M1 @ )) @ = (M1 @ ) + ((- (M1 @ )) @ ) by Th24
.= (M1 @ ) + (- ((M1 @ ) @ )) by Th27
.= (M1 @ ) - M1 by A1, A2, MATRIX_2:15
.= - (M1 - (M1 @ )) by A2, A3, MATRIX_4:43 ;
hence M1 - (M1 @ ) is antisymmetric by Def6; :: thesis: verum