let R be strict Ring; :: thesis: for S being RingExtension of R
for T being Subset of S holds
( RAdj (R,T) = R iff T is Subset of R )
let S be RingExtension of R; :: thesis: for T being Subset of S holds
( RAdj (R,T) = R iff T is Subset of R )
let T be Subset of S; :: thesis: ( RAdj (R,T) = R iff T is Subset of R )
set P = RAdj (R,T);
X: ( R is Subring of R & R is Subring of S ) by FIELD_4:def 1, LIOUVIL2:18;
Z: now :: thesis: for o being object st o in the carrier of R holds
o in the carrier of (RAdj (R,T))
let o be object ; :: thesis: ( o in the carrier of R implies o in the carrier of (RAdj (R,T)) )
assume C1: o in the carrier of R ; :: thesis: o in the carrier of (RAdj (R,T))
the carrier of R c= the carrier of S by X, C0SP1:def 3;
then reconsider a = o as Element of S by C1;
now :: thesis: for U being Subring of S st R is Subring of U & T is Subset of U holds
o in U
let U be Subring of S; :: thesis: ( R is Subring of U & T is Subset of U implies o in U )
assume ( R is Subring of U & T is Subset of U ) ; :: thesis: o in U
then the carrier of R c= the carrier of U by C0SP1:def 3;
hence o in U by C1; :: thesis: verum
end;
then a in carrierRA T ;
hence o in the carrier of (RAdj (R,T)) by dRA; :: thesis: verum
end;
now :: thesis: ( T is Subset of R implies RAdj (R,T) = R )
assume B0: T is Subset of R ; :: thesis: RAdj (R,T) = R
B5: now :: thesis: for o being object st o in the carrier of (RAdj (R,T)) holds
o in the carrier of R
let o be object ; :: thesis: ( o in the carrier of (RAdj (R,T)) implies o in the carrier of R )
assume o in the carrier of (RAdj (R,T)) ; :: thesis: o in the carrier of R
then o in carrierRA T by dRA;
then consider x being Element of S such that
B1: ( 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 R by X, B0, B1;
hence o in the carrier of R by B1; :: thesis: verum
end;
then B1: the carrier of R = the carrier of (RAdj (R,T)) by Z, TARSKI:2;
B2: 1. (RAdj (R,T)) = 1. S by dRA
.= 1. R by X, C0SP1:def 3 ;
B3: 0. (RAdj (R,T)) = 0. S by dRA
.= 0. R by X, C0SP1:def 3 ;
B4: the addF of (RAdj (R,T)) = the addF of S || (carrierRA T) by dRA
.= the addF of S || the carrier of R by B1, dRA
.= the addF of R by X, C0SP1:def 3 ;
the multF of (RAdj (R,T)) = the multF of S || (carrierRA T) by dRA
.= the multF of S || the carrier of R by B1, dRA
.= the multF of R by X, C0SP1:def 3 ;
hence RAdj (R,T) = R by Z, TARSKI:2, B5, B2, B3, B4; :: thesis: verum
end;
hence ( RAdj (R,T) = R iff T is Subset of R ) by RAt; :: thesis: verum