thus (hom_Ext_eval (x,F_Rat)) . (1_ (Polynom-Ring F_Rat)) =
(hom_Ext_eval (x,F_Rat)) . (1_. F_Rat)
by POLYNOM3:37
.=
Ext_eval ((1_. F_Rat),x)
by Def9
.=
1_ F_Complex
by Th3, Th18
; GROUP_1:def 13 ( hom_Ext_eval (x,F_Rat) is additive & hom_Ext_eval (x,F_Rat) is multiplicative )
hereby VECTSP_1:def 19 hom_Ext_eval (x,F_Rat) is multiplicative
let a,
b be
Element of
(Polynom-Ring F_Rat);
(hom_Ext_eval (x,F_Rat)) . (a + b) = ((hom_Ext_eval (x,F_Rat)) . a) + ((hom_Ext_eval (x,F_Rat)) . b)reconsider p =
a,
q =
b as
Polynomial of
F_Rat by POLYNOM3:def 10;
thus (hom_Ext_eval (x,F_Rat)) . (a + b) =
(hom_Ext_eval (x,F_Rat)) . (p + q)
by POLYNOM3:def 10
.=
Ext_eval (
(p + q),
x)
by Def9
.=
(Ext_eval (p,x)) + (Ext_eval (q,x))
by Th3, Th19
.=
((hom_Ext_eval (x,F_Rat)) . a) + (Ext_eval (q,x))
by Def9
.=
((hom_Ext_eval (x,F_Rat)) . a) + ((hom_Ext_eval (x,F_Rat)) . b)
by Def9
;
verum
end;
hereby GROUP_6:def 6 verum
let a,
b be
Element of
(Polynom-Ring F_Rat);
(hom_Ext_eval (x,F_Rat)) . (a * b) = ((hom_Ext_eval (x,F_Rat)) . a) * ((hom_Ext_eval (x,F_Rat)) . b)reconsider p =
a,
q =
b as
Polynomial of
F_Rat by POLYNOM3:def 10;
thus (hom_Ext_eval (x,F_Rat)) . (a * b) =
(hom_Ext_eval (x,F_Rat)) . (p *' q)
by POLYNOM3:def 10
.=
Ext_eval (
(p *' q),
x)
by Def9
.=
(Ext_eval (p,x)) * (Ext_eval (q,x))
by Th3, Th24
.=
((hom_Ext_eval (x,F_Rat)) . a) * (Ext_eval (q,x))
by Def9
.=
((hom_Ext_eval (x,F_Rat)) . a) * ((hom_Ext_eval (x,F_Rat)) . b)
by Def9
;
verum
end;