let F be Field; :: thesis: for E being FieldExtension of F
for T being non empty finite Subset of E
for x being b₂ -evaluating Function of (card T),E holds Image_hom_Ext_eval (x,F) is Subring of RAdj (F,T)
let E be FieldExtension of F; :: thesis: for T being non empty finite Subset of E
for x being b₁ -evaluating Function of (card T),E holds Image_hom_Ext_eval (x,F) is Subring of RAdj (F,T)
let T be non empty finite Subset of E; :: thesis: for x being T -evaluating Function of (card T),E holds Image_hom_Ext_eval (x,F) is Subring of RAdj (F,T)
let x be T -evaluating Function of (card T),E; :: thesis: Image_hom_Ext_eval (x,F) is Subring of RAdj (F,T)
set S = Image_hom_Ext_eval (x,F);
set R = RAdj (F,T);
A: the carrier of (Image_hom_Ext_eval (x,F)) = rng (hom_Ext_eval (x,F)) by defIm;
then the carrier of (Image_hom_Ext_eval (x,F)) c= the carrier of (RAdj (F,T)) by lemphi2;
then J: [: the carrier of (Image_hom_Ext_eval (x,F)), the carrier of (Image_hom_Ext_eval (x,F)):] c= [: the carrier of (RAdj (F,T)), the carrier of (RAdj (F,T)):] by ZFMISC_1:96;
B: the addF of (Image_hom_Ext_eval (x,F)) = the addF of E || (rng (hom_Ext_eval (x,F))) by defIm
.= the addF of E || the carrier of (Image_hom_Ext_eval (x,F)) by defIm
.= ( the addF of E || the carrier of (RAdj (F,T))) || the carrier of (Image_hom_Ext_eval (x,F)) by J, FUNCT_1:51
.= ( the addF of E || (carrierRA T)) || the carrier of (Image_hom_Ext_eval (x,F)) by FIELD_6:def 4
.= the addF of (RAdj (F,T)) || the carrier of (Image_hom_Ext_eval (x,F)) by FIELD_6:def 4 ;
C: the multF of (Image_hom_Ext_eval (x,F)) = the multF of E || (rng (hom_Ext_eval (x,F))) by defIm
.= the multF of E || the carrier of (Image_hom_Ext_eval (x,F)) by defIm
.= ( the multF of E || the carrier of (RAdj (F,T))) || the carrier of (Image_hom_Ext_eval (x,F)) by J, FUNCT_1:51
.= ( the multF of E || (carrierRA T)) || the carrier of (Image_hom_Ext_eval (x,F)) by FIELD_6:def 4
.= the multF of (RAdj (F,T)) || the carrier of (Image_hom_Ext_eval (x,F)) by FIELD_6:def 4 ;
D: 1. (Image_hom_Ext_eval (x,F)) = 1. E by defIm
.= 1. (RAdj (F,T)) by FIELD_6:def 4 ;
0. (Image_hom_Ext_eval (x,F)) = 0. E by defIm
.= 0. (RAdj (F,T)) by FIELD_6:def 4 ;
hence Image_hom_Ext_eval (x,F) is Subring of RAdj (F,T) by A, B, C, D, C0SP1:def 3, lemphi2; :: thesis: verum