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 )
then consider B2 being Matrix of n,K such that
A2: B2 * A = 1. K,n by Th55;
B2 = B2 * (1. K,n) by MATRIX_3:21
.= (B2 * A) * B by A1, Th17
.= B by A2, MATRIX_3:20 ;
then A is_reverse_of B by A1, A2, 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
A3: B * B3 = 1. K,n by A1, Th54;
B3 = (1. K,n) * B3 by MATRIX_3:20
.= A * (B * B3) by A1, Th17
.= A by A3, MATRIX_3:21 ;
then B is_reverse_of A by A1, A3, MATRIX_6:def 2;
hence B is invertible by MATRIX_6:def 3; :: thesis: verum