let R be Ring; for n being Nat
for S being Subring of R holds the carrier of (GL (n,S)) c= the carrier of (GL (n,R))
let n be Nat; for S being Subring of R holds the carrier of (GL (n,S)) c= the carrier of (GL (n,R))
let S be Subring of R; the carrier of (GL (n,S)) c= the carrier of (GL (n,R))
for x being object st x in the carrier of (GL (n,S)) holds
x in the carrier of (GL (n,R))
proof
let x be
object ;
( x in the carrier of (GL (n,S)) implies x in the carrier of (GL (n,R)) )
assume
x in the
carrier of
(GL (n,S))
;
x in the carrier of (GL (n,R))
then reconsider g =
x as
Element of
(GL (n,S)) ;
reconsider M1 =
g as
invertible Matrix of
n,
S by Th126;
reconsider M2 =
M1 as
Matrix of
n,
R by Th82;
M2 is
Element of
(GL (n,R))
by Th128, Th139;
hence
x in the
carrier of
(GL (n,R))
;
verum
end;
hence
the carrier of (GL (n,S)) c= the carrier of (GL (n,R))
by TARSKI:def 3; verum