let n be Element of NAT ; 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; 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; ( A * B = 1. (K,n) implies ( A is invertible & B is invertible ) )
assume A1:
A * B = 1. (K,n)
; ( 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; 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; verum