let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E holds
( not a in F iff for p being non zero Polynomial of F st Ext_eval (p,a) = 0. E holds
deg p >= 2 )
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E holds
( not a in F iff for p being non zero Polynomial of F st Ext_eval (p,a) = 0. E holds
deg p >= 2 )
let a be F -algebraic Element of E; :: thesis: ( not a in F iff for p being non zero Polynomial of F st Ext_eval (p,a) = 0. E holds
deg p >= 2 )
H2: F is Subfield of E by FIELD_4:7;
then H3: ( the carrier of F c= the carrier of E & 1. E = 1. F & 0. E = 0. F ) by EC_PF_1:def 1;

Z: now :: thesis: ( not a in F implies for p being non zero Polynomial of F st Ext_eval (p,a) = 0. E holds
deg p >= 2 )

assume AS: not a in F ; :: thesis: for p being non zero Polynomial of F st Ext_eval (p,a) = 0. E holds
deg p >= 2

now :: thesis: for p being non zero Polynomial of F st Ext_eval (p,a) = 0. E holds
deg p >= 2

let p be non zero Polynomial of F; :: thesis: ( Ext_eval (p,a) = 0. E implies deg p >= 2 )
assume A: Ext_eval (p,a) = 0. E ; :: thesis: deg p >= 2
reconsider q = p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

now :: thesis: not deg p < 2

assume deg p < 2 ; :: thesis: contradiction

per cases then ( deg p = 1 or deg p = 0 ) by NAT_1:23;

suppose deg p = 1 ; :: thesis: contradiction

then consider x, z being Element of F such that
A1: ( x <> 0. F & p = x * (rpoly (1,z)) ) by HURWITZ:28;
reconsider xE = x, zE = z as Element of E by H3;
A2: p is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider pE = p as Element of the carrier of (Polynom-Ring E) by A2;
A4: ( x | F = xE | E & rpoly (1,zE) = rpoly (1,z) ) by FIELD_4:21, FIELD_6:23;
A3: xE * (rpoly (1,zE)) = (xE | E) *' (rpoly (1,zE)) by FIELD_8:2
.= (x | F) *' (rpoly (1,z)) by A4, FIELD_4:17
.= x * (rpoly (1,z)) by FIELD_8:2 ;
A4: xE <> 0. E by A1, H2, EC_PF_1:def 1;
0. E = eval (pE,a) by A, A2, FIELD_4:26
.= xE * (eval ((rpoly (1,zE)),a)) by A1, A3, POLYNOM5:30 ;
then 0. E = eval ((rpoly (1,zE)),a) by A4, VECTSP_2:def 1
.= a - zE by HURWITZ:29 ;
then a = z by RLVECT_1:21;
hence contradiction by AS; :: thesis: verum

end;

suppose deg p = 0 ; :: thesis: contradiction

then consider b being Element of F such that
A1: q = b | F by RING_4:def 4, RING_4:20;
A2: b <> 0. F by A1;
reconsider bE = b as Element of E by H3;
A3: ( bE | E = q & bE | E is Element of the carrier of (Polynom-Ring E) ) by A1, FIELD_6:23, POLYNOM3:def 10;
A4: deg (bE | E) = 0 by A2, H3, RING_4:21;
0. E = eval ((bE | E),a) by A, A3, FIELD_4:26;
hence contradiction by A4, RATFUNC1:8; :: thesis: verum

end;

end;

end;

hence deg p >= 2 ; :: thesis: verum

end;

hence for p being non zero Polynomial of F st Ext_eval (p,a) = 0. E holds
deg p >= 2 ; :: thesis: verum

end;

now :: thesis: ( a in F implies ex p being non zero Polynomial of F st
( Ext_eval (p,a) = 0. E & deg p < 2 ) )

assume a in F ; :: thesis: ex p being non zero Polynomial of F st
( Ext_eval (p,a) = 0. E & deg p < 2 )
then reconsider b = a as Element of F ;
thus ex p being non zero Polynomial of F st
( Ext_eval (p,a) = 0. E & deg p < 2 ) :: thesis: verum

proof

take p = X- b; :: thesis: ( Ext_eval (p,a) = 0. E & deg p < 2 )
I: ( rpoly (1,a) is Element of the carrier of (Polynom-Ring E) & rpoly (1,b) is Element of the carrier of (Polynom-Ring F) ) by POLYNOM3:def 10;
thus Ext_eval (p,a) = Ext_eval ((rpoly (1,b)),a) by FIELD_9:def 2
.= eval ((rpoly (1,a)),a) by FIELD_4:21, I, FIELD_4:26
.= a - a by HURWITZ:29
.= 0. E by RLVECT_1:5 ; :: thesis: deg p < 2
deg p = deg (rpoly (1,b)) by FIELD_9:def 2
.= 1 by HURWITZ:27 ;
hence deg p < 2 ; :: thesis: verum

end;

end;

hence ( not a in F iff for p being non zero Polynomial of F st Ext_eval (p,a) = 0. E holds
deg p >= 2 ) by Z; :: thesis: verum