let F be Field; :: thesis: for E being Polynom-Ring F -homomorphic FieldExtension of F
for a being non zero Element of E holds
( a is F -algebraic iff a " in RAdj (F,{a}) )
let E be Polynom-Ring F -homomorphic FieldExtension of F; :: thesis: for a being non zero Element of E holds
( a is F -algebraic iff a " in RAdj (F,{a}) )
let a be non zero Element of E; :: thesis: ( a is F -algebraic iff a " in RAdj (F,{a}) )
X: F is Subring of E by FIELD_4:def 1;

A: now :: thesis: ( a is F -algebraic implies a " in RAdj (F,{a}) )

assume a is F -algebraic ; :: thesis: a " in RAdj (F,{a})
then A1: FAdj (F,{a}) = RAdj (F,{a}) by ch1;
A2: {a} is Subset of (FAdj (F,{a})) by FAt;
a in {a} by TARSKI:def 1;
then reconsider b = a as Element of the carrier of (FAdj (F,{a})) by A2;
b " in the carrier of (FAdj (F,{a})) ;
hence a " in RAdj (F,{a}) by A1, Th19f; :: thesis: verum

end;

now :: thesis: ( a " in RAdj (F,{a}) implies a is F -algebraic )

assume a " in RAdj (F,{a}) ; :: thesis: a is F -algebraic
then a " in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by lemphi5;
then consider p being Polynomial of F such that
A1: a " = Ext_eval (p,a) ;
set r = (- (1. F)) | F;
set q = ((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F);
- (0. F) = 0. F ;
then - (1. F) <> 0. F ;
then B0: deg ((- (1. F)) | F) = 0 by RING_4:21;
B5: deg (rpoly (1,(0. F))) = 1 by HURWITZ:27;
not ((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F) is zero

proof

per cases ( p = 0_. F or p <> 0_. F ) ;

suppose p = 0_. F ; :: thesis: not ((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F) is zero

hence not ((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F) is zero by B0, HURWITZ:20; :: thesis: verum

end;

suppose B3: p <> 0_. F ; :: thesis: not ((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F) is zero

then reconsider degp = deg p as Element of NAT by FIELD_1:1;
B4: deg ((rpoly (1,(0. F))) *' p) = (deg (rpoly (1,(0. F)))) + degp by B3, HURWITZ:23;
deg (((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F)) = max (((deg (rpoly (1,(0. F)))) + (deg p)),0) by B0, B4, B5, HURWITZ:21
.= (deg (rpoly (1,(0. F)))) + degp by XXREAL_0:def 10 ;
then ((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F) <> 0_. F by HURWITZ:20;
hence not ((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F) is zero by UPROOTS:def 5; :: thesis: verum

end;

end;

end;

then reconsider q = ((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F) as non zero Polynomial of F ;
1. E = 1. F by X, C0SP1:def 3;
then A2: - (1. E) = (- (1. F)) * (1. F) by X, Th19
.= (- (1. F)) * (LC (1_. F)) by RATFUNC1:def 7
.= LC ((- (1. F)) * (1_. F)) by RATFUNC1:18
.= LC ((- (1. F)) | F) by RING_4:16 ;
A3: 0. E = 0. F by X, C0SP1:def 3;
reconsider rpE = rpoly (1,(0. E)) as Element of the carrier of (Polynom-Ring E) by POLYNOM3:def 10;
reconsider rpF = rpoly (1,(0. F)) as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
A5: a <> 0. E ;
Ext_eval (q,a) = (Ext_eval (((rpoly (1,(0. F))) *' p),a)) + (Ext_eval (((- (1. F)) | F),a)) by X, ALGNUM_1:15
.= ((Ext_eval ((rpoly (1,(0. F))),a)) * (a ")) + (Ext_eval (((- (1. F)) | F),a)) by X, A1, ALGNUM_1:20
.= ((Ext_eval (rpF,a)) * (a ")) + (- (1. E)) by A2, exevalconst
.= ((eval (rpE,a)) * (a ")) + (- (1. E)) by A3, FIELD_4:21, FIELD_4:26
.= ((a - (0. E)) * (a ")) + (- (1. E)) by HURWITZ:29
.= ((a ") * a) + (- (1. E)) by GROUP_1:def 12
.= (1. E) + (- (1. E)) by A5, VECTSP_1:def 10
.= 0. E by RLVECT_1:5 ;
hence a is F -algebraic by alg00; :: thesis: verum

end;

hence ( a is F -algebraic iff a " in RAdj (F,{a}) ) by A; :: thesis: verum