let F1 be Field; :: thesis: for E being FieldExtension of F1
for p being irreducible Element of the carrier of (Polynom-Ring F1)
for a, b being Element of E st a is_a_root_of p,E & b is_a_root_of p,E holds
FAdj (F1,{a}), FAdj (F1,{b}) are_isomorphic
let E1 be FieldExtension of F1; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F1)
for a, b being Element of E1 st a is_a_root_of p,E1 & b is_a_root_of p,E1 holds
FAdj (F1,{a}), FAdj (F1,{b}) are_isomorphic
let p be irreducible Element of the carrier of (Polynom-Ring F1); :: thesis: for a, b being Element of E1 st a is_a_root_of p,E1 & b is_a_root_of p,E1 holds
FAdj (F1,{a}), FAdj (F1,{b}) are_isomorphic
let a, b be Element of E1; :: thesis: ( a is_a_root_of p,E1 & b is_a_root_of p,E1 implies FAdj (F1,{a}), FAdj (F1,{b}) are_isomorphic )
assume ( a is_a_root_of p,E1 & b is_a_root_of p,E1 ) ; :: thesis: FAdj (F1,{a}), FAdj (F1,{b}) are_isomorphic
then B: ( Ext_eval (p,a) = 0. E1 & Ext_eval (p,b) = 0. E1 ) by FIELD_4:def 2;
then reconsider a1 = a as F1 -algebraic Element of E1 by FIELD_6:43;
id F1 is isomorphism ;
then reconsider F2 = F1 as F1 -isomorphic Field by RING_3:def 4;
reconsider E2 = E1 as FieldExtension of F2 ;
reconsider h = id F1 as Isomorphism of F1,F2 ;
reconsider b1 = b as F2 -algebraic Element of E2 by B, FIELD_6:43;
now :: thesis: for i being Element of NAT holds ((PolyHom h) . p) . i = p . i
let i be Element of NAT ; :: thesis: ((PolyHom h) . p) . i = p . i
thus ((PolyHom h) . p) . i = h . (p . i) by FIELD_1:def 2
.= p . i ; :: thesis: verum
end;
then (PolyHom h) . p = p ;
then ( Psi (a1,b1,h,p) is h -extending & Psi (a1,b1,h,p) is isomorphism ) by B, unique1;
hence FAdj (F1,{a}), FAdj (F1,{b}) are_isomorphic ; :: thesis: verum