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
( p = MinPoly (a,F) iff ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E ) )
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
( p = MinPoly (a,F) iff ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E ) )
let a be F -algebraic Element of E; :: thesis: for p being Element of the carrier of (Polynom-Ring F) holds
( p = MinPoly (a,F) iff ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E ) )
let p be Element of the carrier of (Polynom-Ring F); :: thesis: ( p = MinPoly (a,F) iff ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E ) )
set m = MinPoly (a,F);
set g = hom_Ext_eval (a,F);
X: F is Subring of E by FIELD_4:def 1;
a is_integral_over F by alg1;
then ( MinPoly (a,F) <> 0_. F & {(MinPoly (a,F))} -Ideal = Ann_Poly (a,F) & MinPoly (a,F) = NormPolynomial (MinPoly (a,F)) ) by X, ALGNUM_1:def 9;
then MinPoly (a,F) in { p where p is Polynomial of F : Ext_eval (p,a) = 0. E } by IDEAL_1:66;
then consider m1 being Polynomial of F such that
Z1: ( m1 = MinPoly (a,F) & Ext_eval (m1,a) = 0. E ) ;

now :: thesis: ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E implies p = MinPoly (a,F) )

assume A: ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E ) ; :: thesis: p = MinPoly (a,F)
reconsider p1 = p as Element of (Polynom-Ring F) ;
ker (hom_Ext_eval (a,F)) is principal by IDEAL_1:def 28;
then consider u being Element of (Polynom-Ring F) such that
C1: ker (hom_Ext_eval (a,F)) = {u} -Ideal ;
(hom_Ext_eval (a,F)) . p = 0. E by A, 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 C2: p in {u} -Ideal by C1, VECTSP10:def 9;
p in { (u * r) where r is Element of (Polynom-Ring F) : verum } by C2, IDEAL_1:64;
then consider v being Element of (Polynom-Ring F) such that
C3: p = u * v ;
reconsider u1 = u as Polynomial of F by POLYNOM3:def 10;

A2: now :: thesis: u is not Unit of (Polynom-Ring F)

assume u is Unit of (Polynom-Ring F) ; :: thesis: contradiction
then {u} -Ideal = [#] (Polynom-Ring F) by RING_2:20;
hence contradiction by C1; :: thesis: verum

end;

u divides p by C3;
then u is_associated_to p by A2, A, RING_2:def 9;
then {p} -Ideal = ker (hom_Ext_eval (a,F)) by C1, RING_2:21;
hence p = MinPoly (a,F) by A, mpol1; :: thesis: verum

end;

hence ( p = MinPoly (a,F) iff ( p is monic & p is irreducible & Ext_eval (p,a) = 0. E ) ) by Z1; :: thesis: verum