let R be Ring; :: thesis: for n being Nat
for x being object holds
( x is Element of (GL (n,R)) iff x is invertible Matrix of n,R )
let n be Nat; :: thesis: for x being object holds
( x is Element of (GL (n,R)) iff x is invertible Matrix of n,R )
let x be object ; :: thesis: ( x is Element of (GL (n,R)) iff x is invertible Matrix of n,R )
set M = Matrix_ring (n,R);

hereby :: thesis: ( x is invertible Matrix of n,R implies x is Element of (GL (n,R)) )

assume x is Element of (GL (n,R)) ; :: thesis: x is invertible Matrix of n,R
then x in units (Matrix_ring (n,R)) ;
then reconsider x2 = x as unital Element of (Matrix_ring (n,R)) by Th107;
consider y being Element of (Matrix_ring (n,R)) such that
A1: ( x2 * y = 1. (Matrix_ring (n,R)) & y * x2 = 1. (Matrix_ring (n,R)) ) by GCD_1:def 2;
reconsider X = x2, Y = y as Matrix of n,R by Th72;
Y is_reverse_of X

proof

X * Y = 1. (R,n) by A1, Th75
.= Y * X by A1, Th75 ;
hence Y is_reverse_of X by A1, Th75, MATRIX_6:def 2; :: thesis: verum

end;

hence x is invertible Matrix of n,R by MATRIX_6:def 3; :: thesis: verum

end;

assume A2: x is invertible Matrix of n,R ; :: thesis: x is Element of (GL (n,R))
x is unital Element of (Matrix_ring (n,R))

proof

reconsider x2 = x as invertible Matrix of n,R by A2;
consider y being Matrix of n,R such that
A3: y is_reverse_of x2 by MATRIX_6:def 3;
A4: ( y * x2 = One (R,n) & x2 * y = One (R,n) ) by A3, MATRIX_6:def 2;
reconsider x3 = x2, y3 = y as Element of (Matrix_ring (n,R)) by Th72;
( y3 * x3 = 1. (Matrix_ring (n,R)) & x3 * y3 = 1. (Matrix_ring (n,R)) ) by A4, Th75;
hence x is unital Element of (Matrix_ring (n,R)) by GCD_1:def 2; :: thesis: verum

end;

hence x is Element of (GL (n,R)) by Th107; :: thesis: verum