let R be Ring; for n being Nat
for S being Subring of R holds the multF of (GL (n,S)) = the multF of (GL (n,R)) || the carrier of (GL (n,S))
let n be Nat; for S being Subring of R holds the multF of (GL (n,S)) = the multF of (GL (n,R)) || the carrier of (GL (n,S))
let S be Subring of R; the multF of (GL (n,S)) = the multF of (GL (n,R)) || the carrier of (GL (n,S))
set US = the carrier of (GL (n,S));
set UR = the carrier of (GL (n,R));
set fS = the multF of (GL (n,S));
set fR = the multF of (GL (n,R));
A1:
the carrier of (GL (n,S)) c= the carrier of (GL (n,R))
by Th140;
then A2:
[: the carrier of (GL (n,S)), the carrier of (GL (n,S)):] c= [: the carrier of (GL (n,R)), the carrier of (GL (n,R)):]
by ZFMISC_1:96;
A3:
the multF of (GL (n,R)) || the carrier of (GL (n,S)) is Function of [: the carrier of (GL (n,S)), the carrier of (GL (n,S)):], the carrier of (GL (n,R))
by A2, FUNCT_2:32;
A4:
the multF of (GL (n,S)) is Function of [: the carrier of (GL (n,S)), the carrier of (GL (n,S)):], the carrier of (GL (n,R))
by A1, FUNCT_2:7;
for x, y being Element of the carrier of (GL (n,S)) holds the multF of (GL (n,S)) . (x,y) = ( the multF of (GL (n,R)) || the carrier of (GL (n,S))) . (x,y)
proof
let x,
y be
Element of the
carrier of
(GL (n,S));
the multF of (GL (n,S)) . (x,y) = ( the multF of (GL (n,R)) || the carrier of (GL (n,S))) . (x,y)
reconsider x9 =
x,
y9 =
y as
Element of
(GL (n,S)) ;
A5:
[x,y] in [: the carrier of (GL (n,S)), the carrier of (GL (n,S)):]
;
then
the
multF of
(GL (n,S)) . (
x,
y) is
Element of
(GL (n,R))
by A4, FUNCT_2:5;
then reconsider LHS = the
multF of
(GL (n,S)) . (
x,
y) as
Matrix of
n,
R by Th126;
( the multF of (GL (n,R)) || the carrier of (GL (n,S))) . (
x,
y)
in the
carrier of
(GL (n,R))
by A3, A5, FUNCT_2:5;
then reconsider RHS =
( the multF of (GL (n,R)) || the carrier of (GL (n,S))) . (
x,
y) as
Matrix of
n,
R by Th126;
reconsider a =
x9,
b =
y9 as
invertible Matrix of
n,
S by Th126;
reconsider X =
x9,
Y =
y9 as
Element of
(GL (n,R)) by A1, TARSKI:def 3;
reconsider A =
X,
B =
Y as
invertible Matrix of
n,
R by Th126;
thus the
multF of
(GL (n,S)) . (
x,
y) =
x9 * y9
.=
a * b
by Th127
.=
A * B
by Th92
.=
X * Y
by Th127
.=
( the multF of (GL (n,R)) || the carrier of (GL (n,S))) . (
x,
y)
by FUNCT_1:49, ZFMISC_1:87
;
verum
end;
hence
the multF of (GL (n,S)) = the multF of (GL (n,R)) || the carrier of (GL (n,S))
by A3, A4, BINOP_1:2; verum