let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E holds
( MinPoly (a,F) = rpoly (1,a) iff a in the carrier of F )
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E holds
( MinPoly (a,F) = rpoly (1,a) iff a in the carrier of F )
let a be F -algebraic Element of E; :: thesis: ( MinPoly (a,F) = rpoly (1,a) iff a in the carrier of F )
set ma = MinPoly (a,F);
set g = hom_Ext_eval (a,F);
X: F is Subring of E by FIELD_4:def 1;

A: now :: thesis: ( a in the carrier of F implies MinPoly (a,F) = rpoly (1,a) )

assume a in the carrier of F ; :: thesis: MinPoly (a,F) = rpoly (1,a)
then reconsider a1 = a as Element of F ;
reconsider p = rpoly (1,a1) as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
A3: rpoly (1,a) = rpoly (1,a1) by FIELD_4:21;
deg p = 1 by HURWITZ:27;
then A2: p is irreducible by RING_4:42;
Ext_eval (p,a) = eval (p,a1) by FIELD427
.= a1 - a1 by HURWITZ:29
.= 0. F by RLVECT_1:15
.= 0. E by X, C0SP1:def 3 ;
hence MinPoly (a,F) = rpoly (1,a) by A3, A2, mpol3; :: thesis: verum

end;

now :: thesis: ( MinPoly (a,F) = rpoly (1,a) implies a in the carrier of F )

assume MinPoly (a,F) = rpoly (1,a) ; :: thesis: a in the carrier of F
then reconsider p = rpoly (1,a) as Element of the carrier of (Polynom-Ring F) ;
- (p . 0) = - ((rpoly (1,a)) . 0) by X, Th19
.= - (- ((power E) . (a,(1 + 0)))) by HURWITZ:25
.= - (- (((power E) . (a,0)) * a)) by GROUP_1:def 7
.= - (- ((1_ E) * a)) by GROUP_1:def 7
.= a ;
hence a in the carrier of F ; :: thesis: verum

end;

hence ( MinPoly (a,F) = rpoly (1,a) iff a in the carrier of F ) by A; :: thesis: verum