let R be Ring; :: thesis: for n being Nat
for x being Element of (Matrix_ring (n,R)) holds
( x is invertible iff ex X being invertible Matrix of n,R st X = x )
let n be Nat; :: thesis: for x being Element of (Matrix_ring (n,R)) holds
( x is invertible iff ex X being invertible Matrix of n,R st X = x )
let x be Element of (Matrix_ring (n,R)); :: thesis: ( x is invertible iff ex X being invertible Matrix of n,R st X = x )

hereby :: thesis: ( ex X being invertible Matrix of n,R st X = x implies x is invertible )

assume A1: x is invertible ; :: thesis: ex X being invertible Matrix of n,R st X = x
then consider a being Element of (Matrix_ring (n,R)) such that
A2: a * x = 1. (Matrix_ring (n,R)) by ALGSTR_0:def 27;
consider b being Element of (Matrix_ring (n,R)) such that
A3: x * b = 1. (Matrix_ring (n,R)) by A1, ALGSTR_0:def 28;
A4: a = a * (1. (Matrix_ring (n,R)))
.= (a * x) * b by A3, GROUP_1:def 3
.= b by A2 ;
reconsider X = x, A = a as Matrix of n,R by Th72;
A is_reverse_of X

proof

A * X = 1. (R,n) by A2, Th75
.= X * A by A3, A4, Th75 ;
hence A is_reverse_of X by A2, Th75, MATRIX_6:def 2; :: thesis: verum

end;

then reconsider X = X as invertible Matrix of n,R by MATRIX_6:def 3;
take X = X; :: thesis: X = x
thus X = x ; :: thesis: verum

end;

given X being invertible Matrix of n,R such that A5: X = x ; :: thesis: x is invertible
consider A being Matrix of n,R such that
A6: X is_reverse_of A by MATRIX_6:def 3;
reconsider a = A as Element of (Matrix_ring (n,R)) by Th72;
A7: ( X * A = A * X & X * A = 1. (R,n) ) by A6, MATRIX_6:def 2;
A8: x * a = 1. (Matrix_ring (n,R)) by A5, A7, Th75;
a * x = 1. (Matrix_ring (n,R)) by A5, A7, Th75;
then ( x is left_invertible & x is right_invertible ) by A8, ALGSTR_0:def 27, ALGSTR_0:def 28;
hence x is invertible ; :: thesis: verum