let F be Field; :: thesis:
let E be FieldExtension of F; :: thesis:
let a be F -algebraic Element of E; :: thesis:
let p be Element of the carrier of (Polynom-Ring F); :: thesis:
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 Z: ( 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 ) ;

A: now :: thesis:

assume A1: p = MinPoly (a,F) ; :: thesis:
hence p is monic ; :: thesis:
thus Ext_eval (p,a) = 0. E by Z1, A1; :: thesis:
thus for q being non zero Polynomial of F st Ext_eval (q,a) = 0. E holds
deg p <= deg q :: thesis:

proof

let q be non zero Polynomial of F; :: thesis:
assume Ext_eval (q,a) = 0. E ; :: thesis:
then q in {(MinPoly (a,F))} -Ideal by Z;
then q in { ((MinPoly (a,F)) * r) where r is Element of (Polynom-Ring F) : verum } by IDEAL_1:64;
then consider r being Element of the carrier of (Polynom-Ring F) such that
A2: q = (MinPoly (a,F)) * r ;
reconsider r1 = r as Polynomial of F ;
A3: m1 *' r1 = (MinPoly (a,F)) * r by Z1, POLYNOM3:def 10;
A5: r1 <> 0_. F by A2, A3;
then A6: deg q = (deg p) + (deg r1) by A1, A3, A2, Z1, HURWITZ:23;
deg r1 is Nat by A5, FIELD_1:1;
hence deg p <= deg q by A6, INT_1:6; :: thesis:

end;

now :: thesis:

assume A: ( p is monic & Ext_eval (p,a) = 0. E & ( for q being non zero Polynomial of F st Ext_eval (q,a) = 0. E holds
deg p <= deg q ) ) ; :: thesis:
then A1: p <> 0_. F ;
reconsider p1 = p as Element of (Polynom-Ring F) ;

A2: now :: thesis:

assume p1 is Unit of (Polynom-Ring F) ; :: thesis:
then p1 divides 1. (Polynom-Ring F) by GCD_1:def 20;
then consider u1 being Element of (Polynom-Ring F) such that
A3: p1 * u1 = 1. (Polynom-Ring F) ;
reconsider u = u1 as Element of the carrier of (Polynom-Ring F) ;
p *' u = 1. (Polynom-Ring F) by A3, POLYNOM3:def 10
.= 1_. F by POLYNOM3:def 10 ;
then Ext_eval ((1_. F),a) = (Ext_eval (p,a)) * (Ext_eval (u,a)) by X, ALGNUM_1:20
.= 0. E by A ;
then Ext_eval ((1_. F),a) <> 1. E ;
hence contradiction by X, ALGNUM_1:14; :: thesis:

end;

B: now :: thesis:

assume p is reducible ; :: thesis:
then consider q being Element of the carrier of (Polynom-Ring F) such that
A4: ( q divides p & 1 <= deg q & deg q < deg p ) by A1, A2, RING_4:41;
reconsider q1 = q as Polynomial of F ;
consider u1 being Polynomial of F such that
A3: q1 *' u1 = p1 by A4, RING_4:1;
A6: q1 <> 0_. F by A3, A;
A7: u1 <> 0_. F by A3, A;
then Y: ( deg q1 is Nat & deg u1 is Element of NAT ) by A6, FIELD_1:1;
A11: deg p = (deg q1) + (deg u1) by A3, A7, A6, HURWITZ:23;
then A10: deg u1 <= deg p by Y, INT_1:6;
A19: 0. E = (Ext_eval (q1,a)) * (Ext_eval (u1,a)) by X, A3, A, ALGNUM_1:20;

per cases by A19, VECTSP_2:def 1;

suppose A9: Ext_eval (q1,a) = 0. E ; :: thesis:

not q1 is zero by A3, A;
hence contradiction by A4, A9, A; :: thesis:

end;

suppose A9: Ext_eval (u1,a) = 0. E ; :: thesis:

not u1 is zero by A3, A;
then deg p <= deg u1 by A9, A;
then deg u1 = deg p by A10, XXREAL_0:1;
hence contradiction by A4, A11; :: thesis:

end;

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, v1 = v, p1 = p as Polynomial of F by POLYNOM3:def 10;
C3a: p = u1 *' v1 by C3, POLYNOM3:def 10;
then C3b: ( u1 <> 0_. F & v1 <> 0_. F ) by A;
C3c: not u1 is zero by C3a, A;
C4: deg p = (deg u1) + (deg v1) by C3a, C3b, HURWITZ:23;
u in ker (hom_Ext_eval (a,F)) by C1, IDEAL_1:66;
then u in { v where v is Element of (Polynom-Ring F) : (hom_Ext_eval (a,F)) . v = 0. E } by VECTSP10:def 9;
then consider w being Element of (Polynom-Ring F) such that
C5: ( u = w & (hom_Ext_eval (a,F)) . w = 0. E ) ;
Ext_eval (u1,a) = 0. E by C5, ALGNUM_1:def 11;
then C10: (deg p) + (deg v1) <= deg p by A, C3c, C4, XREAL_1:6;
reconsider degv = deg v1 as Element of NAT by C3b, FIELD_1:1;
((deg p) + (deg v1)) - (deg p) <= (deg p) - (deg p) by C10, XREAL_1:9;
then consider b being Element of F such that
C6: v1 = b | F by RING_4:20, RING_4:def 4;
reconsider v2 = (b ") | F as Element of (Polynom-Ring F) by POLYNOM3:def 10;
C7: b <> 0. F by A, C3a, C6;
(u1 *' v1) *' ((b ") | F) = u1 *' (v1 *' ((b ") | F)) by POLYNOM3:33
.= u1 *' (((b ") * b) | F) by C6, RING_4:18
.= u1 *' ((1. F) | F) by C7, VECTSP_1:def 10
.= u1 *' (1_. F) by RING_4:14 ;
then u1 = p1 *' ((b ") | F) by C3, POLYNOM3:def 10
.= p * v2 by POLYNOM3:def 10 ;
then u in { (p * r) where r is Element of (Polynom-Ring F) : verum } ;
then u in {p} -Ideal by IDEAL_1:64;
then C: ker (hom_Ext_eval (a,F)) c= {p} -Ideal by C1, IDEAL_1:67;
{p} -Ideal c= ker (hom_Ext_eval (a,F)) by C1, C2, IDEAL_1:67;
hence p = MinPoly (a,F) by A, B, mpol1, C, TARSKI:2; :: thesis:

end;

hence ( p = MinPoly (a,F) iff ( p is monic & Ext_eval (p,a) = 0. E & ( for q being non zero Polynomial of F st Ext_eval (q,a) = 0. E holds
deg p <= deg q ) ) ) by A; :: thesis: