let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. K,n holds
M2 = 0. K,n
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st M1 is invertible & M2 * M1 = 0. K,n holds
M2 = 0. K,n
let M1, M2 be Matrix of n,K; :: thesis: ( M1 is invertible & M2 * M1 = 0. K,n implies M2 = 0. K,n )
assume A1: ( M1 is invertible & M2 * M1 = 0. K,n ) ; :: thesis: M2 = 0. K,n
then A2: M1 ~ is_reverse_of M1 by MATRIX_6:def 4;
A3: ( width M1 = n & len M1 = n ) by MATRIX_1:25;
A4: ( width M2 = n & len M2 = n ) by MATRIX_1:25;
A5: ( width (M1 ~ ) = n & len (M1 ~ ) = n ) by MATRIX_1:25;
M2 = M2 * (1. K,n) by MATRIX_3:21
.= M2 * (M1 * (M1 ~ )) by A2, MATRIX_6:def 2
.= (M2 * M1) * (M1 ~ ) by A3, A4, A5, MATRIX_3:35
.= 0. K,n,n by A1, A5, MATRIX_6:1
.= 0. K,n ;
hence M2 = 0. K,n ; :: thesis: verum