let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K st n > 0 & M1 is Nilpotent holds
not M1 is invertible
let K be Field; :: thesis: for M1 being Matrix of n,K st n > 0 & M1 is Nilpotent holds
not M1 is invertible
let M1 be Matrix of n,K; :: thesis: ( n > 0 & M1 is Nilpotent implies not M1 is invertible )
assume that
A1: n > 0 and
A2: M1 is Nilpotent ; :: thesis: not M1 is invertible
A3: ( len M1 = n & width M1 = n ) by MATRIX_0:24;
assume M1 is invertible ; :: thesis: contradiction
then consider M2 being Matrix of n,K such that
A4: M1 is_reverse_of M2 by MATRIX_6:def 3;
A5: width M2 = n by MATRIX_0:24;
A6: len M2 = n by MATRIX_0:24;
M1 = M1 * (1. (K,n)) by MATRIX_3:19
.= M1 * (M1 * M2) by A4, MATRIX_6:def 2
.= (M1 * M1) * M2 by A3, A6, MATRIX_3:33
.= (0. (K,n)) * M2 by A2
.= 0. (K,n,n) by A6, A5, MATRIX_6:1 ;
then A7: M1 * M2 = 0. (K,n) by A6, A5, MATRIX_6:1;
M1 * M2 = 1. (K,n) by A4, MATRIX_6:def 2;
hence contradiction by A1, A7, Th28; :: thesis: verum