let F be Field; :: thesis: for E being FieldExtension of F
for T being Subset of E holds RAdj (F,T) is Subring of FAdj (F,T)
let E be FieldExtension of F; :: thesis: for T being Subset of E holds RAdj (F,T) is Subring of FAdj (F,T)
let T be Subset of E; :: thesis: RAdj (F,T) is Subring of FAdj (F,T)
set Pf = FAdj (F,T);
set Pr = RAdj (F,T);
A: 1. (RAdj (F,T)) = 1. E by dRA
.= 1. (FAdj (F,T)) by dFA ;
B: 0. (RAdj (F,T)) = 0. E by dRA
.= 0. (FAdj (F,T)) by dFA ;
now :: thesis: for o being object st o in the carrier of (RAdj (F,T)) holds
o in the carrier of (FAdj (F,T))
let o be object ; :: thesis: ( o in the carrier of (RAdj (F,T)) implies o in the carrier of (FAdj (F,T)) )
assume o in the carrier of (RAdj (F,T)) ; :: thesis: o in the carrier of (FAdj (F,T))
then o in carrierRA T by dRA;
then consider x being Element of E such that
B1: ( x = o & ( for U being Subring of E st F is Subring of U & T is Subset of U holds
x in U ) ) ;
now :: thesis: for U being Subfield of E st F is Subfield of U & T is Subset of U holds
x in U
let U be Subfield of E; :: thesis: ( F is Subfield of U & T is Subset of U implies x in U )
assume ( F is Subfield of U & T is Subset of U ) ; :: thesis: x in U
then ( F is Subring of U & U is Subring of E & T is Subset of U ) by RING_3:43;
hence x in U by B1; :: thesis: verum
end;
then x in carrierFA T ;
hence o in the carrier of (FAdj (F,T)) by B1, dFA; :: thesis: verum
end;
then C: the carrier of (RAdj (F,T)) c= the carrier of (FAdj (F,T)) ;
then Y: [: the carrier of (RAdj (F,T)), the carrier of (RAdj (F,T)):] c= [: the carrier of (FAdj (F,T)), the carrier of (FAdj (F,T)):] by ZFMISC_1:96;
D: the addF of (FAdj (F,T)) || the carrier of (RAdj (F,T)) = ( the addF of E || (carrierFA T)) || the carrier of (RAdj (F,T)) by dFA
.= ( the addF of E || the carrier of (FAdj (F,T))) || the carrier of (RAdj (F,T)) by dFA
.= the addF of E || the carrier of (RAdj (F,T)) by Y, FUNCT_1:51
.= the addF of E || (carrierRA T) by dRA
.= the addF of (RAdj (F,T)) by dRA ;
the multF of (FAdj (F,T)) || the carrier of (RAdj (F,T)) = ( the multF of E || (carrierFA T)) || the carrier of (RAdj (F,T)) by dFA
.= ( the multF of E || the carrier of (FAdj (F,T))) || the carrier of (RAdj (F,T)) by dFA
.= the multF of E || the carrier of (RAdj (F,T)) by Y, FUNCT_1:51
.= the multF of E || (carrierRA T) by dRA
.= the multF of (RAdj (F,T)) by dRA ;
hence RAdj (F,T) is Subring of FAdj (F,T) by A, B, C, D, C0SP1:def 3; :: thesis: verum