let n be Element of NAT ; :: thesis: for K being Field
for A, B being Matrix of n,K st A * B = 1. K,n holds
( A is invertible & B is invertible )
let K be Field; :: thesis: for A, B being Matrix of n,K st A * B = 1. K,n holds
( A is invertible & B is invertible )
let A, B be Matrix of n,K; :: thesis: ( A * B = 1. K,n implies ( A is invertible & B is invertible ) )
assume A1: A * B = 1. K,n ; :: thesis: ( A is invertible & B is invertible )
consider B2 being Matrix of n,K such that
A5: B2 * A = 1. K,n by AA4600, A1;
B2 = B2 * (1. K,n) by MATRIX_3:21
.= (B2 * A) * B by AA41, A1
.= B by A5, MATRIX_3:20 ;
then A is_reverse_of B by A1, A5, MATRIX_6:def 2;
hence A is invertible by MATRIX_6:def 3; :: thesis: B is invertible
consider B3 being Matrix of n,K such that
A5: B * B3 = 1. K,n by AA4500, A1;
B3 = (1. K,n) * B3 by MATRIX_3:20
.= A * (B * B3) by AA41, A1
.= A by A5, MATRIX_3:21 ;
then B is_reverse_of A by A1, A5, MATRIX_6:def 2;
hence B is invertible by MATRIX_6:def 3; :: thesis: verum