let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for f being F -fixing Automorphism of (FAdj (F,{a})) holds f . a in Roots ((FAdj (F,{a})),(MinPoly (a,F)))
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for f being F -fixing Automorphism of (FAdj (F,{a})) holds f . a in Roots ((FAdj (F,{a})),(MinPoly (a,F)))
let a be F -algebraic Element of E; :: thesis: for f being F -fixing Automorphism of (FAdj (F,{a})) holds f . a in Roots ((FAdj (F,{a})),(MinPoly (a,F)))
let f be F -fixing Automorphism of (FAdj (F,{a})); :: thesis: f . a in Roots ((FAdj (F,{a})),(MinPoly (a,F)))
set p = MinPoly (a,F);
( a in {a} & {a} is Subset of (FAdj (F,{a})) ) by TARSKI:def 1, FIELD_6:35;
then reconsider a1 = a as Element of (FAdj (F,{a})) ;
H1: ( E is FAdj (F,{a}) -extending & MinPoly (a,F) is Element of the carrier of (Polynom-Ring F) ) by FIELD_4:7;
H2: Roots ((FAdj (F,{a})),(MinPoly (a,F))) = { b where b is Element of (FAdj (F,{a})) : b is_a_root_of MinPoly (a,F), FAdj (F,{a}) } by FIELD_4:def 4;
0. (FAdj (F,{a})) = 0. E by FIELD_6:def 6
.= Ext_eval ((MinPoly (a,F)),a) by FIELD_6:52
.= Ext_eval ((MinPoly (a,F)),a1) by H1, FIELD_6:11 ;
then a1 is_a_root_of MinPoly (a,F), FAdj (F,{a}) by FIELD_4:def 2;
then a1 in Roots ((FAdj (F,{a})),(MinPoly (a,F))) by H2;
hence f . a in Roots ((FAdj (F,{a})),(MinPoly (a,F))) by FIELD_8:38; :: thesis: verum