let F be Field; :: thesis: for E being Polynom-Ring F -homomorphic FieldExtension of F
for a being Element of E holds F is Subring of Image (hom_Ext_eval (a,F))
let E be Polynom-Ring F -homomorphic FieldExtension of F; :: thesis: for a being Element of E holds F is Subring of Image (hom_Ext_eval (a,F))
let a be Element of E; :: thesis: F is Subring of Image (hom_Ext_eval (a,F))
set R = Image (hom_Ext_eval (a,F));
set f = hom_Ext_eval (a,F);
X: F is Subring of E by FIELD_4:def 1;
then Y: the carrier of F c= the carrier of E by C0SP1:def 3;

Z: now :: thesis: for x being object st x in the carrier of F holds
x in rng (hom_Ext_eval (a,F))

let x be object ; :: thesis: ( x in the carrier of F implies x in rng (hom_Ext_eval (a,F)) )
assume x in the carrier of F ; :: thesis: x in rng (hom_Ext_eval (a,F))
then reconsider b = x as Element of F ;
reconsider c = b as Element of E by Y;
reconsider p = b | F as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider q = c | E as Element of the carrier of (Polynom-Ring E) by POLYNOM3:def 10;
Ext_eval (p,a) = eval (q,a) by constpol, FIELD_4:26
.= b by RING_5:8 ;
then b in { (Ext_eval (p,a)) where p is Polynomial of F : verum } ;
hence x in rng (hom_Ext_eval (a,F)) by lemphi1; :: thesis: verum

end;

then ZZ: the carrier of F c= rng (hom_Ext_eval (a,F)) ;

now :: thesis: for x being object st x in the carrier of F holds
x in the carrier of (Image (hom_Ext_eval (a,F)))

let x be object ; :: thesis: ( x in the carrier of F implies x in the carrier of (Image (hom_Ext_eval (a,F))) )
assume x in the carrier of F ; :: thesis: x in the carrier of (Image (hom_Ext_eval (a,F)))
then x in rng (hom_Ext_eval (a,F)) by Z;
hence x in the carrier of (Image (hom_Ext_eval (a,F))) by RING_2:def 6; :: thesis: verum

end;

then A: the carrier of F c= the carrier of (Image (hom_Ext_eval (a,F))) ;
set adF = the addF of F;
set adR = the addF of (Image (hom_Ext_eval (a,F)));
H1c: dom the addF of E = [: the carrier of E, the carrier of E:] by FUNCT_2:def 1;
the addF of (Image (hom_Ext_eval (a,F))) = the addF of E || (rng (hom_Ext_eval (a,F))) by RING_2:def 6
.= the addF of E | [:(rng (hom_Ext_eval (a,F))),(rng (hom_Ext_eval (a,F))):] ;
then H1b: dom the addF of (Image (hom_Ext_eval (a,F))) = [: the carrier of E, the carrier of E:] /\ [:(rng (hom_Ext_eval (a,F))),(rng (hom_Ext_eval (a,F))):] by H1c, RELAT_1:61;
H1: dom ( the addF of (Image (hom_Ext_eval (a,F))) || the carrier of F) = (dom the addF of (Image (hom_Ext_eval (a,F)))) /\ [: the carrier of F, the carrier of F:] by RELAT_1:61
.= [: the carrier of E, the carrier of E:] /\ ([:(rng (hom_Ext_eval (a,F))),(rng (hom_Ext_eval (a,F))):] /\ [: the carrier of F, the carrier of F:]) by H1b, XBOOLE_1:16
.= [: the carrier of E, the carrier of E:] /\ [: the carrier of F, the carrier of F:] by ZZ, ZFMISC_1:96, XBOOLE_1:28
.= [: the carrier of F, the carrier of F:] by Y, ZFMISC_1:96, XBOOLE_1:28
.= dom the addF of F by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom the addF of F holds
the addF of F . o = ( the addF of (Image (hom_Ext_eval (a,F))) | [: the carrier of F, the carrier of F:]) . o

let o be object ; :: thesis: ( o in dom the addF of F implies the addF of F . o = ( the addF of (Image (hom_Ext_eval (a,F))) | [: the carrier of F, the carrier of F:]) . o )
assume AS: o in dom the addF of F ; :: thesis: the addF of F . o = ( the addF of (Image (hom_Ext_eval (a,F))) | [: the carrier of F, the carrier of F:]) . o
then consider a, b being object such that
B1: ( a in the carrier of F & b in the carrier of F & o = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of F by B1;
( a in rng (hom_Ext_eval (a,F)) & b in rng (hom_Ext_eval (a,F)) ) by Z;
then B3: o in [:(rng (hom_Ext_eval (a,F))),(rng (hom_Ext_eval (a,F))):] by B1, ZFMISC_1:def 2;
B5: the addF of F = the addF of E || the carrier of F by C0SP1:def 3, X;
thus the addF of F . o = the addF of E . o by AS, B5, FUNCT_1:49
.= ( the addF of E || (rng (hom_Ext_eval (a,F)))) . o by B3, FUNCT_1:49
.= the addF of (Image (hom_Ext_eval (a,F))) . o by RING_2:def 6
.= ( the addF of (Image (hom_Ext_eval (a,F))) | [: the carrier of F, the carrier of F:]) . o by AS, H1, FUNCT_1:47 ; :: thesis: verum

end;

then B: the addF of F = the addF of (Image (hom_Ext_eval (a,F))) || the carrier of F by H1;
set muF = the multF of F;
set muR = the multF of (Image (hom_Ext_eval (a,F)));
H1c: dom the multF of E = [: the carrier of E, the carrier of E:] by FUNCT_2:def 1;
the multF of (Image (hom_Ext_eval (a,F))) = the multF of E || (rng (hom_Ext_eval (a,F))) by RING_2:def 6
.= the multF of E | [:(rng (hom_Ext_eval (a,F))),(rng (hom_Ext_eval (a,F))):] ;
then H1b: dom the multF of (Image (hom_Ext_eval (a,F))) = [: the carrier of E, the carrier of E:] /\ [:(rng (hom_Ext_eval (a,F))),(rng (hom_Ext_eval (a,F))):] by H1c, RELAT_1:61;
H1: dom ( the multF of (Image (hom_Ext_eval (a,F))) || the carrier of F) = (dom the multF of (Image (hom_Ext_eval (a,F)))) /\ [: the carrier of F, the carrier of F:] by RELAT_1:61
.= [: the carrier of E, the carrier of E:] /\ ([:(rng (hom_Ext_eval (a,F))),(rng (hom_Ext_eval (a,F))):] /\ [: the carrier of F, the carrier of F:]) by H1b, XBOOLE_1:16
.= [: the carrier of E, the carrier of E:] /\ [: the carrier of F, the carrier of F:] by ZZ, ZFMISC_1:96, XBOOLE_1:28
.= [: the carrier of F, the carrier of F:] by Y, ZFMISC_1:96, XBOOLE_1:28
.= dom the multF of F by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom the multF of F holds
the multF of F . o = ( the multF of (Image (hom_Ext_eval (a,F))) | [: the carrier of F, the carrier of F:]) . o

let o be object ; :: thesis: ( o in dom the multF of F implies the multF of F . o = ( the multF of (Image (hom_Ext_eval (a,F))) | [: the carrier of F, the carrier of F:]) . o )
assume AS: o in dom the multF of F ; :: thesis: the multF of F . o = ( the multF of (Image (hom_Ext_eval (a,F))) | [: the carrier of F, the carrier of F:]) . o
then consider a, b being object such that
B1: ( a in the carrier of F & b in the carrier of F & o = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of F by B1;
( a in rng (hom_Ext_eval (a,F)) & b in rng (hom_Ext_eval (a,F)) ) by Z;
then B3: o in [:(rng (hom_Ext_eval (a,F))),(rng (hom_Ext_eval (a,F))):] by B1, ZFMISC_1:def 2;
B5: the multF of F = the multF of E || the carrier of F by C0SP1:def 3, X;
thus the multF of F . o = the multF of E . o by AS, B5, FUNCT_1:49
.= ( the multF of E || (rng (hom_Ext_eval (a,F)))) . o by B3, FUNCT_1:49
.= the multF of (Image (hom_Ext_eval (a,F))) . o by RING_2:def 6
.= ( the multF of (Image (hom_Ext_eval (a,F))) | [: the carrier of F, the carrier of F:]) . o by AS, H1, FUNCT_1:47 ; :: thesis: verum

end;

then C: the multF of F = the multF of (Image (hom_Ext_eval (a,F))) || the carrier of F by H1;
D: 0. F = 0. E by X, C0SP1:def 3
.= 0. (Image (hom_Ext_eval (a,F))) by RING_2:def 6 ;
1. F = 1. E by X, C0SP1:def 3
.= 1. (Image (hom_Ext_eval (a,F))) by RING_2:def 6 ;
hence F is Subring of Image (hom_Ext_eval (a,F)) by A, B, C, D, C0SP1:def 3; :: thesis: verum