let n be Nat; for K being Field
for M1, M2 being Matrix of n,K st M2 is invertible & M2 * M1 = 1. (K,n) holds
M1 is_reverse_of M2
let K be Field; for M1, M2 being Matrix of n,K st M2 is invertible & M2 * M1 = 1. (K,n) holds
M1 is_reverse_of M2
let M1, M2 be Matrix of n,K; ( M2 is invertible & M2 * M1 = 1. (K,n) implies M1 is_reverse_of M2 )
A1:
( len M1 = n & width M2 = n )
by MATRIX_0:24;
A2:
( len M2 = n & width (M2 ~) = n )
by MATRIX_0:24;
assume that
A3:
M2 is invertible
and
A4:
M2 * M1 = 1. (K,n)
; M1 is_reverse_of M2
A5:
M2 ~ is_reverse_of M2
by A3, Def4;
(M2 ~) * (M2 * M1) = M2 ~
by A4, MATRIX_3:19;
then
((M2 ~) * M2) * M1 = M2 ~
by A1, A2, MATRIX_3:33;
then
(1. (K,n)) * M1 = M2 ~
by A5;
then
M1 = M2 ~
by MATRIX_3:18;
hence
M1 is_reverse_of M2
by A3, Def4; verum