let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for p being Element of the carrier of (Polynom-Ring F) holds
( Ext_eval (p,a) = 0. E iff MinPoly (a,F) divides p )
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for p being Element of the carrier of (Polynom-Ring F) holds
( Ext_eval (p,a) = 0. E iff MinPoly (a,F) divides p )
let a be F -algebraic Element of E; :: thesis: for p being Element of the carrier of (Polynom-Ring F) holds
( Ext_eval (p,a) = 0. E iff MinPoly (a,F) divides p )
let p be Element of the carrier of (Polynom-Ring F); :: thesis: ( Ext_eval (p,a) = 0. E iff MinPoly (a,F) divides p )
set ma = MinPoly (a,F);
set g = hom_Ext_eval (a,F);
X: F is Subring of E by FIELD_4:def 1;
reconsider p1 = p, ma1 = MinPoly (a,F) as Element of (Polynom-Ring F) ;

A: now :: thesis: ( Ext_eval (p,a) = 0. E implies MinPoly (a,F) divides p )

assume Ext_eval (p,a) = 0. E ; :: thesis: MinPoly (a,F) divides p
then (hom_Ext_eval (a,F)) . p = 0. E by ALGNUM_1:def 11;
then p in { v where v is Element of (Polynom-Ring F) : (hom_Ext_eval (a,F)) . v = 0. E } ;
then p in ker (hom_Ext_eval (a,F)) by VECTSP10:def 9;
then p in {(MinPoly (a,F))} -Ideal by mpol1;
hence MinPoly (a,F) divides p by RING_4:def 3, RING_2:18; :: thesis: verum

end;

now :: thesis: ( MinPoly (a,F) divides p implies 0. E = Ext_eval (p,a) )

assume MinPoly (a,F) divides p ; :: thesis: 0. E = Ext_eval (p,a)
then consider u being Polynomial of F such that
H: (MinPoly (a,F)) *' u = p by RING_4:1;
0. E = Ext_eval ((MinPoly (a,F)),a) by mpol2;
hence 0. E = (Ext_eval ((MinPoly (a,F)),a)) * (Ext_eval (u,a))
.= Ext_eval (p,a) by X, H, ALGNUM_1:20 ;
:: thesis: verum

end;

hence ( Ext_eval (p,a) = 0. E iff MinPoly (a,F) divides p ) by A; :: thesis: verum