set F = R;
set E = S;
X:
R is Subring of S
by FIELD_4:def 1;
set g = hom_Ext_eval (a,R);
now for x, y being Element of (Polynom-Ring R) holds (hom_Ext_eval (a,R)) . (x + y) = ((hom_Ext_eval (a,R)) . x) + ((hom_Ext_eval (a,R)) . y)let x,
y be
Element of
(Polynom-Ring R);
(hom_Ext_eval (a,R)) . (x + y) = ((hom_Ext_eval (a,R)) . x) + ((hom_Ext_eval (a,R)) . y)reconsider p =
x,
q =
y as
Polynomial of
R by POLYNOM3:def 10;
thus (hom_Ext_eval (a,R)) . (x + y) =
(hom_Ext_eval (a,R)) . (p + q)
by POLYNOM3:def 10
.=
Ext_eval (
(p + q),
a)
by ALGNUM_1:def 11
.=
(Ext_eval (p,a)) + (Ext_eval (q,a))
by X, ALGNUM_1:15
.=
((hom_Ext_eval (a,R)) . x) + (Ext_eval (q,a))
by ALGNUM_1:def 11
.=
((hom_Ext_eval (a,R)) . x) + ((hom_Ext_eval (a,R)) . y)
by ALGNUM_1:def 11
;
verum end;
hence
hom_Ext_eval (a,R) is additive
; ( hom_Ext_eval (a,R) is multiplicative & hom_Ext_eval (a,R) is unity-preserving )
now for x, y being Element of (Polynom-Ring R) holds (hom_Ext_eval (a,R)) . (x * y) = ((hom_Ext_eval (a,R)) . x) * ((hom_Ext_eval (a,R)) . y)let x,
y be
Element of
(Polynom-Ring R);
(hom_Ext_eval (a,R)) . (x * y) = ((hom_Ext_eval (a,R)) . x) * ((hom_Ext_eval (a,R)) . y)reconsider p =
x,
q =
y as
Polynomial of
R by POLYNOM3:def 10;
thus (hom_Ext_eval (a,R)) . (x * y) =
(hom_Ext_eval (a,R)) . (p *' q)
by POLYNOM3:def 10
.=
Ext_eval (
(p *' q),
a)
by ALGNUM_1:def 11
.=
(Ext_eval (p,a)) * (Ext_eval (q,a))
by X, ALGNUM_1:20
.=
((hom_Ext_eval (a,R)) . x) * (Ext_eval (q,a))
by ALGNUM_1:def 11
.=
((hom_Ext_eval (a,R)) . x) * ((hom_Ext_eval (a,R)) . y)
by ALGNUM_1:def 11
;
verum end;
hence
hom_Ext_eval (a,R) is multiplicative
; hom_Ext_eval (a,R) is unity-preserving
(hom_Ext_eval (a,R)) . (1_ (Polynom-Ring R)) =
(hom_Ext_eval (a,R)) . (1_. R)
by POLYNOM3:37
.=
Ext_eval ((1_. R),a)
by ALGNUM_1:def 11
.=
1_ S
by X, ALGNUM_1:14
;
hence
hom_Ext_eval (a,R) is unity-preserving
; verum