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 Th23

.= (M1 @) + (- ((M1 @) @)) by Th26

.= (M1 @) - M1 by A1, A2, MATRIX_0:57

.= - (M1 - (M1 @)) by A2, A3, MATRIX_4:43 ;

hence M1 - (M1 @) is antisymmetric ; :: thesis: verum

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 Th23

.= (M1 @) + (- ((M1 @) @)) by Th26

.= (M1 @) - M1 by A1, A2, MATRIX_0:57

.= - (M1 - (M1 @)) by A2, A3, MATRIX_4:43 ;

hence M1 - (M1 @) is antisymmetric ; :: thesis: verum