let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E holds MinPoly (a,F) is irreducible
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E holds MinPoly (a,F) is irreducible
let a be F -algebraic Element of E; :: thesis: MinPoly (a,F) is irreducible
set m = MinPoly (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 ) ;
reconsider m2 = MinPoly (a,F) as Element of (Polynom-Ring F) ;
reconsider m1 = m1 as non zero Element of the carrier of (Polynom-Ring F) by Z1, Z, UPROOTS:def 5;
A2: MinPoly (a,F) <> 0. (Polynom-Ring F) by Z, POLYNOM3:def 10;

A3: now :: thesis: m2 is not Unit of (Polynom-Ring F)

assume m2 is Unit of (Polynom-Ring F) ; :: thesis: contradiction
then A4: {(MinPoly (a,F))} -Ideal = [#] (Polynom-Ring F) by RING_2:20;
ker (hom_Ext_eval (a,F)) is proper ;
hence contradiction by A4, Z, alg0; :: thesis: verum

end;

now :: thesis: for x being Element of (Polynom-Ring F) holds
( not x divides MinPoly (a,F) or x is Unit of (Polynom-Ring F) or x is_associated_to MinPoly (a,F) )

let x be Element of (Polynom-Ring F); :: thesis: ( not x divides MinPoly (a,F) or b₁ is Unit of (Polynom-Ring F) or b₁ is_associated_to MinPoly (a,F) )
assume B: x divides MinPoly (a,F) ; :: thesis: ( b₁ is Unit of (Polynom-Ring F) or b₁ is_associated_to MinPoly (a,F) )
consider y being Element of (Polynom-Ring F) such that
A4: x * y = m2 by B;
reconsider x1 = x, y1 = y as Polynomial of F by POLYNOM3:def 10;
m1 = x1 *' y1 by Z1, A4, POLYNOM3:def 10;
then A5: Ext_eval (m1,a) = (Ext_eval (x1,a)) * (Ext_eval (y1,a)) by ALGNUM_1:20, X;

per cases ( Ext_eval (x1,a) = 0. E or Ext_eval (y1,a) = 0. E ) by A5, Z1, VECTSP_2:def 1;

suppose Ext_eval (x1,a) = 0. E ; :: thesis: ( b₁ is Unit of (Polynom-Ring F) or b₁ is_associated_to MinPoly (a,F) )

then x1 in {(MinPoly (a,F))} -Ideal by Z;
then x1 in { ((MinPoly (a,F)) * r) where r is Element of (Polynom-Ring F) : verum } by IDEAL_1:64;
then consider r being Element of (Polynom-Ring F) such that
A6: x = m2 * r ;
m2 divides x by A6;
hence ( x is Unit of (Polynom-Ring F) or x is_associated_to MinPoly (a,F) ) by B; :: thesis: verum

end;

suppose Ext_eval (y1,a) = 0. E ; :: thesis: ( b₁ is Unit of (Polynom-Ring F) or b₁ is_associated_to MinPoly (a,F) )

then y1 in {(MinPoly (a,F))} -Ideal by Z;
then y1 in { ((MinPoly (a,F)) * r) where r is Element of (Polynom-Ring F) : verum } by IDEAL_1:64;
then consider r being Element of (Polynom-Ring F) such that
A6: y1 = (MinPoly (a,F)) * r ;
reconsider r1 = r as Polynomial of F by POLYNOM3:def 10;
A8: x * r = x1 *' r1 by POLYNOM3:def 10;
(1. (Polynom-Ring F)) * (MinPoly (a,F)) = x * (r * (MinPoly (a,F))) by A6, A4, GROUP_1:def 12
.= (x * r) * (MinPoly (a,F)) by GROUP_1:def 3 ;
then (1_. F) *' m1 = (x1 *' r1) *' m1 by Z1, A8, POLYNOM3:def 10;
then 1_. F = x1 *' r1 by RATFUNC1:7
.= x * r by POLYNOM3:def 10 ;
then 1. (Polynom-Ring F) = x * r by POLYNOM3:def 10;
then x divides 1. (Polynom-Ring F) ;
hence ( x is Unit of (Polynom-Ring F) or x is_associated_to MinPoly (a,F) ) by GCD_1:def 20; :: thesis: verum

end;

end;

end;

hence MinPoly (a,F) is irreducible by A2, A3, RING_2:def 9; :: thesis: verum