let F be Field; :: thesis: for E being FieldExtension of F
for a, b being F -algebraic Element of E holds
( Phi (a,b) is F -isomorphism iff MinPoly (a,F) = MinPoly (b,F) )
let E be FieldExtension of F; :: thesis: for a, b being F -algebraic Element of E holds
( Phi (a,b) is F -isomorphism iff MinPoly (a,F) = MinPoly (b,F) )
let a, b be F -algebraic Element of E; :: thesis: ( Phi (a,b) is F -isomorphism iff MinPoly (a,F) = MinPoly (b,F) )
set Fa = FAdj (F,{a});
set Fb = FAdj (F,{b});
I1: FAdj (F,{a}) = RAdj (F,{a}) by FIELD_6:56;
I2: FAdj (F,{b}) = RAdj (F,{b}) by FIELD_6:56;
I4: F is Subring of E by FIELD_4:def 1;

A: now :: thesis: ( MinPoly (a,F) = MinPoly (b,F) implies Phi (a,b) is F -isomorphism )

assume AS: MinPoly (a,F) = MinPoly (b,F) ; :: thesis: Phi (a,b) is F -isomorphism

now :: thesis: for x, y1, y2 being object st [x,y1] in Phi (a,b) & [x,y2] in Phi (a,b) holds
y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in Phi (a,b) & [x,y2] in Phi (a,b) implies y1 = y2 )
assume A1: ( [x,y1] in Phi (a,b) & [x,y2] in Phi (a,b) ) ; :: thesis: y1 = y2
then consider p being Polynomial of F such that
A2: [x,y1] = [(Ext_eval (p,a)),(Ext_eval (p,b))] ;
A3: ( x = Ext_eval (p,a) & y1 = Ext_eval (p,b) ) by A2, XTUPLE_0:1;
consider q being Polynomial of F such that
A4: [x,y2] = [(Ext_eval (q,a)),(Ext_eval (q,b))] by A1;
A5: ( x = Ext_eval (q,a) & y2 = Ext_eval (q,b) ) by A4, XTUPLE_0:1;
A6: for r being Polynomial of F st Ext_eval (r,a) = 0. E holds
Ext_eval (r,b) = 0. E

proof

let r be Polynomial of F; :: thesis: ( Ext_eval (r,a) = 0. E implies Ext_eval (r,b) = 0. E )
A8: r is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
assume Ext_eval (r,a) = 0. E ; :: thesis: Ext_eval (r,b) = 0. E
then MinPoly (b,F) divides r by AS, A8, FIELD_6:53;
hence Ext_eval (r,b) = 0. E by A8, FIELD_6:53; :: thesis: verum

end;

Ext_eval (p,a) = Ext_eval (q,a) by A2, XTUPLE_0:1, A5;
then 0. E = (Ext_eval (p,a)) - (Ext_eval (q,a)) by RLVECT_1:15
.= Ext_eval ((p - q),a) by FIELD_6:27 ;
then 0. E = Ext_eval ((p - q),b) by A6
.= (Ext_eval (p,b)) - (Ext_eval (q,b)) by FIELD_6:27 ;
hence y1 = y2 by A5, A3, RLVECT_1:21; :: thesis: verum

end;

then reconsider g = Phi (a,b) as Function of the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{b})) by FUNCT_1:def 1;

H: now :: thesis: for p being Polynomial of F holds g . (Ext_eval (p,a)) = Ext_eval (p,b)

let p be Polynomial of F; :: thesis: g . (Ext_eval (p,a)) = Ext_eval (p,b)
[(Ext_eval (p,a)),(Ext_eval (p,b))] in Phi (a,b) ;
hence g . (Ext_eval (p,a)) = Ext_eval (p,b) by FUNCT_1:1; :: thesis: verum

end;

I: g . (1. (FAdj (F,{a}))) = g . (Ext_eval ((1_. F),a)) by u1
.= Ext_eval ((1_. F),b) by H
.= 1. (FAdj (F,{b})) by u1 ;

now :: thesis: for x, y being Element of (FAdj (F,{a})) holds g . (x * y) = (g . x) * (g . y)

let x, y be Element of (FAdj (F,{a})); :: thesis: g . (x * y) = (g . x) * (g . y)
x in the carrier of (FAdj (F,{a})) ;
then x in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by I1, FIELD_6:45;
then consider p being Polynomial of F such that
A1: x = Ext_eval (p,a) ;
y in the carrier of (FAdj (F,{a})) ;
then y in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by I1, FIELD_6:45;
then consider q being Polynomial of F such that
A2: y = Ext_eval (q,a) ;
B: ( g . x = Ext_eval (p,b) & g . y = Ext_eval (q,b) ) by A1, A2, H;
( g . x in the carrier of (FAdj (F,{b})) & g . y in the carrier of (FAdj (F,{b})) ) ;
then ( g . x in carrierFA {b} & g . y in carrierFA {b} ) by FIELD_6:def 6;
then C: [(g . x),(g . y)] in [:(carrierFA {b}),(carrierFA {b}):] by ZFMISC_1:def 2;
x * y = Ext_eval ((p *' q),a) by A1, A2, u2;
hence g . (x * y) = Ext_eval ((p *' q),b) by H
.= (Ext_eval (p,b)) * (Ext_eval (q,b)) by I4, ALGNUM_1:20
.= ( the multF of E || (carrierFA {b})) . ((g . x),(g . y)) by B, C, FUNCT_1:49
.= (g . x) * (g . y) by FIELD_6:def 6 ;
:: thesis: verum

end;

then B: g is multiplicative ;

now :: thesis: for x, y being Element of (FAdj (F,{a})) holds g . (x + y) = (g . x) + (g . y)

let x, y be Element of (FAdj (F,{a})); :: thesis: g . (x + y) = (g . x) + (g . y)
x in the carrier of (FAdj (F,{a})) ;
then x in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by I1, FIELD_6:45;
then consider p being Polynomial of F such that
A1: x = Ext_eval (p,a) ;
y in the carrier of (FAdj (F,{a})) ;
then y in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by I1, FIELD_6:45;
then consider q being Polynomial of F such that
A2: y = Ext_eval (q,a) ;
B: ( g . x = Ext_eval (p,b) & g . y = Ext_eval (q,b) ) by A1, A2, H;
( g . x in the carrier of (FAdj (F,{b})) & g . y in the carrier of (FAdj (F,{b})) ) ;
then ( g . x in carrierFA {b} & g . y in carrierFA {b} ) by FIELD_6:def 6;
then C: [(g . x),(g . y)] in [:(carrierFA {b}),(carrierFA {b}):] by ZFMISC_1:def 2;
x + y = Ext_eval ((p + q),a) by A1, A2, u2;
hence g . (x + y) = Ext_eval ((p + q),b) by H
.= (Ext_eval (p,b)) + (Ext_eval (q,b)) by I4, ALGNUM_1:15
.= ( the addF of E || (carrierFA {b})) . ((g . x),(g . y)) by B, C, FUNCT_1:49
.= (g . x) + (g . y) by FIELD_6:def 6 ;
:: thesis: verum

end;

then g is additive ;
then D: g is monomorphism by I, B, RING_2:11;
X: g is onto

proof

E1: now :: thesis: for o being object st o in rng g holds
o in the carrier of (FAdj (F,{b}))

let o be object ; :: thesis: ( o in rng g implies o in the carrier of (FAdj (F,{b})) )
assume E2: o in rng g ; :: thesis: o in the carrier of (FAdj (F,{b}))
rng g c= the carrier of (FAdj (F,{b})) by RELAT_1:def 19;
hence o in the carrier of (FAdj (F,{b})) by E2; :: thesis: verum

end;

now :: thesis: for o being object st o in the carrier of (FAdj (F,{b})) holds
o in rng g

let o be object ; :: thesis: ( o in the carrier of (FAdj (F,{b})) implies o in rng g )
assume o in the carrier of (FAdj (F,{b})) ; :: thesis: o in rng g
then o in { (Ext_eval (p,b)) where p is Polynomial of F : verum } by I2, FIELD_6:45;
then consider p being Polynomial of F such that
E2: o = Ext_eval (p,b) ;
Ext_eval (p,a) in { (Ext_eval (p,a)) where p is Polynomial of F : verum } ;
then Ext_eval (p,a) in the carrier of (FAdj (F,{a})) by I1, FIELD_6:45;
then E3: Ext_eval (p,a) in dom g by FUNCT_2:def 1;
g . (Ext_eval (p,a)) = o by E2, H;
hence o in rng g by E3, FUNCT_1:def 3; :: thesis: verum

end;

hence g is onto by E1, TARSKI:2; :: thesis: verum

end;

now :: thesis: for x being Element of F holds g . x = x

let x be Element of F; :: thesis: g . x = x
x = Ext_eval ((x | F),a) by u3;
then g . x = Ext_eval ((x | F),b) by H;
hence g . x = x by u3; :: thesis: verum

end;

then g is F -fixing ;
hence Phi (a,b) is F -isomorphism by X, D, deffixiso; :: thesis: verum

end;

now :: thesis: ( Phi (a,b) is F -isomorphism implies MinPoly (a,F) = MinPoly (b,F) )

assume Phi (a,b) is F -isomorphism ; :: thesis: MinPoly (a,F) = MinPoly (b,F)
then consider g being Function of (FAdj (F,{a})),(FAdj (F,{b})) such that
B1: ( g = Phi (a,b) & g is F -isomorphism ) ;
set h = g * (hom_Ext_eval (a,F));
rng (hom_Ext_eval (a,F)) c= dom g

proof

now :: thesis: for o being object st o in rng (hom_Ext_eval (a,F)) holds
o in dom g

let o be object ; :: thesis: ( o in rng (hom_Ext_eval (a,F)) implies o in dom g )
assume B2: o in rng (hom_Ext_eval (a,F)) ; :: thesis: o in dom g
reconsider E1 = E as Polynom-Ring F -homomorphic Field ;
reconsider f = hom_Ext_eval (a,F) as Homomorphism of (Polynom-Ring F),E1 ;
RAdj (F,{a}) = Image f by FIELD_6:44;
then B3: rng f = the carrier of (RAdj (F,{a})) by RING_2:def 6;
RAdj (F,{a}) is Subring of FAdj (F,{a}) by FIELD_6:39;
then the carrier of (RAdj (F,{a})) c= the carrier of (FAdj (F,{a})) by C0SP1:def 3;
then o in the carrier of (FAdj (F,{a})) by B2, B3;
hence o in dom g by FUNCT_2:def 1; :: thesis: verum

end;

hence rng (hom_Ext_eval (a,F)) c= dom g ; :: thesis: verum

end;

then C1: dom (g * (hom_Ext_eval (a,F))) = dom (hom_Ext_eval (a,F)) by RELAT_1:27
.= the carrier of (Polynom-Ring F) by FUNCT_2:def 1 ;

CX: now :: thesis: for p being Polynomial of F holds g . (Ext_eval (p,a)) = Ext_eval (p,b)

let p be Polynomial of F; :: thesis: g . (Ext_eval (p,a)) = Ext_eval (p,b)
[(Ext_eval (p,a)),(Ext_eval (p,b))] in Phi (a,b) ;
hence g . (Ext_eval (p,a)) = Ext_eval (p,b) by B1, FUNCT_1:1; :: thesis: verum

end;

C0: now :: thesis: for x being object st x in dom (g * (hom_Ext_eval (a,F))) holds
(g * (hom_Ext_eval (a,F))) . x = (hom_Ext_eval (b,F)) . x

let x be object ; :: thesis: ( x in dom (g * (hom_Ext_eval (a,F))) implies (g * (hom_Ext_eval (a,F))) . x = (hom_Ext_eval (b,F)) . x )
assume C2: x in dom (g * (hom_Ext_eval (a,F))) ; :: thesis: (g * (hom_Ext_eval (a,F))) . x = (hom_Ext_eval (b,F)) . x
then reconsider p = x as Polynomial of F by POLYNOM3:def 10;
thus (g * (hom_Ext_eval (a,F))) . x = g . ((hom_Ext_eval (a,F)) . p) by C2, FUNCT_1:12
.= g . (Ext_eval (p,a)) by ALGNUM_1:def 11
.= Ext_eval (p,b) by CX
.= (hom_Ext_eval (b,F)) . x by ALGNUM_1:def 11 ; :: thesis: verum

end;

B2: g * (hom_Ext_eval (a,F)) = hom_Ext_eval (b,F) by C0, C1, FUNCT_2:def 1;
then reconsider h = g * (hom_Ext_eval (a,F)) as Function of (Polynom-Ring F),E ;
B7: ( ker g = {(0. (FAdj (F,{a})))} & g . (0. (FAdj (F,{a}))) = 0. (FAdj (F,{b})) )

proof

B8: g is isomorphism by B1, deffixiso;
then reconsider Fb1 = FAdj (F,{b}) as FAdj (F,{a}) -monomorphic Field by RING_3:def 3;
reconsider g1 = g as Monomorphism of (FAdj (F,{a})),Fb1 by B8;
ker g1 = {(0. (FAdj (F,{a})))} by RING_2:12;
hence ker g = {(0. (FAdj (F,{a})))} ; :: thesis: g . (0. (FAdj (F,{a}))) = 0. (FAdj (F,{b}))
g1 . (0. (FAdj (F,{a}))) = 0. (FAdj (F,{b})) by RING_2:6;
hence g . (0. (FAdj (F,{a}))) = 0. (FAdj (F,{b})) ; :: thesis: verum

end;

ker h = ker (hom_Ext_eval (a,F))

proof

D: now :: thesis: for o being object st o in ker h holds
o in ker (hom_Ext_eval (a,F))

let o be object ; :: thesis: ( o in ker h implies o in ker (hom_Ext_eval (a,F)) )
assume o in ker h ; :: thesis: o in ker (hom_Ext_eval (a,F))
then o in { v where v is Element of (Polynom-Ring F) : h . v = 0. E } by VECTSP10:def 9;
then consider p being Element of (Polynom-Ring F) such that
D1: ( o = p & h . p = 0. E ) ;
D2: g . ((hom_Ext_eval (a,F)) . p) = 0. E by C1, D1, FUNCT_1:12
.= 0. (FAdj (F,{b})) by FIELD_6:def 6 ;
(hom_Ext_eval (a,F)) . p is Element of (FAdj (F,{a}))

proof

reconsider E1 = E as Polynom-Ring F -homomorphic Field ;
reconsider f = hom_Ext_eval (a,F) as Homomorphism of (Polynom-Ring F),E1 ;
RAdj (F,{a}) = Image f by FIELD_6:44;
then B3: rng f = the carrier of (RAdj (F,{a})) by RING_2:def 6;
RAdj (F,{a}) is Subring of FAdj (F,{a}) by FIELD_6:39;
then B4: the carrier of (RAdj (F,{a})) c= the carrier of (FAdj (F,{a})) by C0SP1:def 3;
dom (hom_Ext_eval (a,F)) = the carrier of (Polynom-Ring F) by FUNCT_2:def 1;
hence (hom_Ext_eval (a,F)) . p is Element of (FAdj (F,{a})) by B3, B4, FUNCT_1:3; :: thesis: verum

end;

then (hom_Ext_eval (a,F)) . p in { v where v is Element of (FAdj (F,{a})) : g . v = 0. (FAdj (F,{b})) } by D2;
then (hom_Ext_eval (a,F)) . p in ker g by VECTSP10:def 9;
then (hom_Ext_eval (a,F)) . p = 0. (FAdj (F,{a})) by B7, TARSKI:def 1
.= 0. E by FIELD_6:def 6 ;
then p in { v where v is Element of (Polynom-Ring F) : (hom_Ext_eval (a,F)) . v = 0. E } ;
hence o in ker (hom_Ext_eval (a,F)) by D1, VECTSP10:def 9; :: thesis: verum

end;

now :: thesis: for o being object st o in ker (hom_Ext_eval (a,F)) holds
o in ker h

let o be object ; :: thesis: ( o in ker (hom_Ext_eval (a,F)) implies o in ker h )
assume D1: o in ker (hom_Ext_eval (a,F)) ; :: thesis: o in ker h
ker (hom_Ext_eval (a,F)) = { v where v is Element of (Polynom-Ring F) : (hom_Ext_eval (a,F)) . v = 0. E } by VECTSP10:def 9;
then consider p being Element of (Polynom-Ring F) such that
D2: ( o = p & (hom_Ext_eval (a,F)) . p = 0. E ) by D1;
dom (hom_Ext_eval (a,F)) = the carrier of (Polynom-Ring F) by FUNCT_2:def 1;
then D3: h . p = g . ((hom_Ext_eval (a,F)) . p) by FUNCT_1:13
.= g . (0. (FAdj (F,{a}))) by D2, FIELD_6:def 6
.= 0. E by B7, FIELD_6:def 6 ;
ker h = { v where v is Element of (Polynom-Ring F) : h . v = 0. E } by VECTSP10:def 9;
hence o in ker h by D2, D3; :: thesis: verum

end;

hence ker h = ker (hom_Ext_eval (a,F)) by D, TARSKI:2; :: thesis: verum

end;

then ker (hom_Ext_eval (a,F)) = {(MinPoly (b,F))} -Ideal by B2, FIELD_6:50;
hence MinPoly (a,F) = MinPoly (b,F) by FIELD_6:50; :: thesis: verum

end;

hence ( Phi (a,b) is F -isomorphism iff MinPoly (a,F) = MinPoly (b,F) ) by A; :: thesis: verum