let R be Ring; :: thesis: for S being RingExtension of R
for T being Subset of S
for U being Subring of S st R is Subring of U & T is Subset of U holds
RAdj (R,T) is Subring of U
let S be RingExtension of R; :: thesis: for T being Subset of S
for U being Subring of S st R is Subring of U & T is Subset of U holds
RAdj (R,T) is Subring of U
let T be Subset of S; :: thesis: for U being Subring of S st R is Subring of U & T is Subset of U holds
RAdj (R,T) is Subring of U
let U be Subring of S; :: thesis: ( R is Subring of U & T is Subset of U implies RAdj (R,T) is Subring of U )
assume AS: ( R is Subring of U & T is Subset of U ) ; :: thesis: RAdj (R,T) is Subring of U
set P = RAdj (R,T);
A: 1. (RAdj (R,T)) = 1. S by dRA
.= 1. U by C0SP1:def 3 ;
B: 0. (RAdj (R,T)) = 0. S by dRA
.= 0. U by C0SP1:def 3 ;
C: the carrier of (RAdj (R,T)) c= the carrier of U
proof
now :: thesis: for o being object st o in the carrier of (RAdj (R,T)) holds
o in the carrier of U
let o be object ; :: thesis: ( o in the carrier of (RAdj (R,T)) implies o in the carrier of U )
assume o in the carrier of (RAdj (R,T)) ; :: thesis: o in the carrier of U
then o in carrierRA T by dRA;
then consider x being Element of S such that
C2: ( x = o & ( for U being Subring of S st R is Subring of U & T is Subset of U holds
x in U ) ) ;
x in U by C2, AS;
hence o in the carrier of U by C2; :: thesis: verum
end;
hence the carrier of (RAdj (R,T)) c= the carrier of U ; :: thesis: verum
end;
then Y: [: the carrier of (RAdj (R,T)), the carrier of (RAdj (R,T)):] c= [: the carrier of U, the carrier of U:] by ZFMISC_1:96;
D: the addF of U || the carrier of (RAdj (R,T)) = ( the addF of S || the carrier of U) || the carrier of (RAdj (R,T)) by C0SP1:def 3
.= the addF of S || the carrier of (RAdj (R,T)) by Y, FUNCT_1:51
.= the addF of S || (carrierRA T) by dRA
.= the addF of (RAdj (R,T)) by dRA ;
the multF of U || the carrier of (RAdj (R,T)) = ( the multF of S || the carrier of U) || the carrier of (RAdj (R,T)) by C0SP1:def 3
.= the multF of S || the carrier of (RAdj (R,T)) by Y, FUNCT_1:51
.= the multF of S || (carrierRA T) by dRA
.= the multF of (RAdj (R,T)) by dRA ;
hence RAdj (R,T) is Subring of U by A, B, C, D, C0SP1:def 3; :: thesis: verum