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:19
.= (B2 * A) * B by A1, Th17
.= B by A2, MATRIX_3:18 ;
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:18
.= A * (B * B3) by A1, Th17
.= A by A3, MATRIX_3:19 ;
then B is_reverse_of A by A1, A3, MATRIX_6:def 2;
hence B is invertible by MATRIX_6:def 3; :: thesis: verum