let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for p being Polynomial of F holds Ext_eval (p,a) in Lin (Base a)
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for p being Polynomial of F holds Ext_eval (p,a) in Lin (Base a)
let a be F -algebraic Element of E; :: thesis: for p being Polynomial of F holds Ext_eval (p,a) in Lin (Base a)
let p be Polynomial of F; :: thesis: Ext_eval (p,a) in Lin (Base a)
set ma = MinPoly (a,F);
set r = p mod (MinPoly (a,F));
B: F is Subring of E by FIELD_4:def 1;
C: p = ((p div (MinPoly (a,F))) *' (MinPoly (a,F))) + (p mod (MinPoly (a,F))) by RING_4:4;
D: deg (p mod (MinPoly (a,F))) < deg (MinPoly (a,F)) by FIELD_5:16;
Ext_eval (p,a) = (Ext_eval (((p div (MinPoly (a,F))) *' (MinPoly (a,F))),a)) + (Ext_eval ((p mod (MinPoly (a,F))),a)) by C, B, ALGNUM_1:15
.= ((Ext_eval ((p div (MinPoly (a,F))),a)) * (Ext_eval ((MinPoly (a,F)),a))) + (Ext_eval ((p mod (MinPoly (a,F))),a)) by B, ALGNUM_1:20
.= ((Ext_eval ((p div (MinPoly (a,F))),a)) * (0. E)) + (Ext_eval ((p mod (MinPoly (a,F))),a)) by mpol2
.= Ext_eval ((p mod (MinPoly (a,F))),a) ;
hence Ext_eval (p,a) in Lin (Base a) by D, lembas1a; :: thesis: verum