let K be Field; :: thesis: for n being Nat
for M1 being Matrix of n,K st M1 is antisymmetric holds
- M1 is antisymmetric
let n be Nat; :: thesis: for M1 being Matrix of n,K st M1 is antisymmetric holds
- M1 is antisymmetric
let M1 be Matrix of n,K; :: thesis: ( M1 is antisymmetric implies - M1 is antisymmetric )
assume A1: M1 is antisymmetric ; :: thesis: - M1 is antisymmetric
(- M1) @ = - (M1 @ ) by Th27
.= - (- M1) by A1, Def6 ;
hence - M1 is antisymmetric by Def6; :: thesis: verum