:: Splitting Fields
:: by Christoph Schwarzweller
::
:: Copyright (c) 2021 Association of Mizar Users

theorem DZIW: :: FIELD_8:1
for R being Ring
for p being Polynomial of R
for q being Element of the carrier of () st p = q holds
- p = - q
proof end;

poly0: for R being Ring
for a being Element of R holds
( (a | R) . 0 = a & ( for n being Element of NAT st n <> 0 holds
(a | R) . n = 0. R ) )

proof end;

theorem poly1: :: FIELD_8:2
for R being Ring
for p being Polynomial of R
for a being Element of R holds a * p = (a | R) *' p
proof end;

theorem hcon2: :: FIELD_8:3
for R being Ring
for a being Element of R holds LC (a | R) = a
proof end;

Th14: for A, B being Ring
for F being FinSequence of A
for G being FinSequence of B st A is Subring of B & F = G holds
In ((),B) = Product G

proof end;

theorem u5: :: FIELD_8:4
for R being Ring
for S being Subring of R
for F being FinSequence of R
for G being FinSequence of S st F = G holds
Product F = Product G
proof end;

registration
let F be Field;
existence
ex b1 being Field st
( b1 is F -homomorphic & b1 is F -monomorphic & b1 is F -isomorphic )
proof end;
end;

registration
let R be Ring;
coherence
for b1 being R -isomorphic Ring holds
( b1 is R -homomorphic & b1 is R -monomorphic )
;
end;

registration
let R be Ring;
let S be R -homomorphic Ring;
coherence
proof end;
end;

registration
let F1 be Field;
let F2 be F1 -homomorphic F1 -isomorphic Field;
coherence
proof end;
end;

theorem lemma2e: :: FIELD_8:5
for R being non degenerated Ring
for S being RingExtension of R
for p being Polynomial of R
for q being Polynomial of S st p = q holds
LC p = LC q
proof end;

theorem lemma7b: :: FIELD_8:6
for F being Field
for p being Element of the carrier of ()
for E being FieldExtension of F
for q being Element of the carrier of () st p = q holds
for U being b3 -extending FieldExtension of F
for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)
proof end;

theorem m4spl: :: FIELD_8:7
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of ()
for q being Element of the carrier of () st p = q holds
for T1 being RingExtension of S
for T2 being RingExtension of R st T1 = T2 holds
Roots (T2,p) = Roots (T1,q)
proof end;

theorem lemppoly: :: FIELD_8:8
for R being domRing
for F being non empty FinSequence of ()
for p being Polynomial of R st p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) holds
deg p = len F
proof end;

theorem lemppolspl2: :: FIELD_8:9
for F being Field
for p being Polynomial of F
for a being non zero Element of F holds
( a * p splits_in F iff p splits_in F )
proof end;

lemppolspl: for F being Field
for p being Ppoly of F holds p splits_in F

proof end;

lemppolspl3b: for F being Field
for p being non constant monic Polynomial of F
for a being Element of F st (rpoly (1,a)) *' p is Ppoly of F holds
p is Ppoly of F

proof end;

theorem lemppolspl3a: :: FIELD_8:10
for F being Field
for p being non constant monic Polynomial of F
for q being non zero Polynomial of F st p *' q is Ppoly of F holds
p is Ppoly of F
proof end;

theorem lemppolspl3: :: FIELD_8:11
for F being Field
for p being non constant Polynomial of F
for q being non zero Polynomial of F st p *' q splits_in F holds
p splits_in F
proof end;

theorem lemppolspl1: :: FIELD_8:12
for F being Field
for p, q being Polynomial of F st p splits_in F & q splits_in F holds
p *' q splits_in F
proof end;

theorem hcon: :: FIELD_8:13
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for a being Element of R holds () . (a | R) = (h . a) | S
proof end;

theorem uu0: :: FIELD_8:14
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for p, q being Element of the carrier of () holds
( p divides q iff () . p divides () . q )
proof end;

theorem uu4: :: FIELD_8:15
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for p being irreducible Element of the carrier of () st Ext_eval (p,a) = 0. E holds
MinPoly (a,F) = NormPolynomial p
proof end;

theorem uu5: :: FIELD_8:16
for F1 being Field
for F2 being b1 -homomorphic b1 -monomorphic Field
for h being Monomorphism of F1,F2
for p being Element of the carrier of () holds NormPolynomial (() . p) = () . ()
proof end;

registration
let F1 be Field;
let F2 be F1 -homomorphic F1 -isomorphic Field;
let h be Isomorphism of F1,F2;
let p be constant Element of the carrier of ();
cluster () . p -> constant for Element of the carrier of ();
coherence
for b1 being Element of the carrier of () st b1 = () . p holds
b1 is constant
proof end;
end;

registration
let F1 be Field;
let F2 be F1 -homomorphic F1 -isomorphic Field;
let h be Isomorphism of F1,F2;
let p be non constant Element of the carrier of ();
cluster () . p -> non constant for Element of the carrier of ();
coherence
for b1 being Element of the carrier of () st b1 = () . p holds
not b1 is constant
proof end;
end;

registration
let F1 be Field;
let F2 be F1 -homomorphic F1 -isomorphic Field;
let h be Isomorphism of F1,F2;
let p be irreducible Element of the carrier of ();
cluster () . p -> irreducible for Element of the carrier of ();
coherence
for b1 being Element of the carrier of () st b1 = () . p holds
b1 is irreducible
proof end;
end;

lemma6a: for F1 being Field
for p being non constant Element of the carrier of ()
for F2 being b1 -isomorphic Field
for h being Isomorphism of F1,F2 st p splits_in F1 holds
() . p splits_in F2

proof end;

theorem :: FIELD_8:17
for F1 being Field
for p being non constant Element of the carrier of ()
for F2 being b1 -isomorphic Field
for h being Isomorphism of F1,F2 holds
( p splits_in F1 iff () . p splits_in F2 )
proof end;

theorem lemma7: :: FIELD_8:18
for F being Field
for p being Element of the carrier of ()
for E being FieldExtension of F
for U being b3 -extending FieldExtension of F holds Roots (E,p) c= Roots (U,p)
proof end;

lemmapp: for F being Field
for E being FieldExtension of F
for p being Ppoly of F holds p is Ppoly of E

proof end;

theorem :: FIELD_8:19
for F being Field
for p being non constant Element of the carrier of ()
for E being FieldExtension of F
for U being FieldExtension of E st p splits_in E holds
p splits_in U
proof end;

theorem lemma2y: :: FIELD_8:20
for F being Field
for G being non empty FinSequence of the carrier of () st ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) holds
G is Factorization of Product G
proof end;

theorem lemma2z: :: FIELD_8:21
for F being Field
for G1, G2 being non empty FinSequence of () st ( for i being Nat st i in dom G1 holds
ex a being Element of F st G1 . i = rpoly (1,a) ) & ( for i being Nat st i in dom G2 holds
ex a being Element of F st G2 . i = rpoly (1,a) ) & Product G1 = Product G2 holds
for a being Element of F holds
( ex i being Nat st
( i in dom G1 & G1 . i = rpoly (1,a) ) iff ex i being Nat st
( i in dom G2 & G2 . i = rpoly (1,a) ) )
proof end;

theorem lemma2u: :: FIELD_8:22
for F being Field
for E being FieldExtension of F
for G1 being non empty FinSequence of () st ( for i being Nat st i in dom G1 holds
ex a being Element of F st G1 . i = rpoly (1,a) ) holds
for G2 being non empty FinSequence of () st ( for i being Nat st i in dom G2 holds
ex a being Element of E st G2 . i = rpoly (1,a) ) & Product G1 = Product G2 holds
for a being Element of E holds
( ex i being Nat st
( i in dom G1 & G1 . i = rpoly (1,a) ) iff ex i being Nat st
( i in dom G2 & G2 . i = rpoly (1,a) ) )
proof end;

theorem u6: :: FIELD_8:23
for F being Field
for p being Ppoly of F
for a being Element of F holds LC (a * p) = a
proof end;

theorem :: FIELD_8:24
for F being Field
for E being FieldExtension of F
for p being Ppoly of F holds p is Ppoly of E by lemmapp;

theorem lemma2d: :: FIELD_8:25
for F being Field
for E being FieldExtension of F
for a being non zero Element of F
for b being non zero Element of E
for p being Ppoly of F
for q being Ppoly of E st a * p = b * q holds
( a = b & p = q )
proof end;

theorem u8: :: FIELD_8:26
for F being Field
for E being FieldExtension of F
for G being non empty FinSequence of the carrier of () st ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) holds
Product G is Ppoly of F
proof end;

lemma2: for F being Field
for p being non constant Element of the carrier of ()
for U being FieldExtension of F
for E being b3 -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff for a being Element of E st a is_a_root_of p,E holds
a in U )

proof end;

theorem lemma6: :: FIELD_8:27
for F being Field
for p being non constant Element of the carrier of ()
for U being FieldExtension of F
for E being b3 -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) c= the carrier of U )
proof end;

theorem lemma3: :: FIELD_8:28
for F being Field
for p being non constant Element of the carrier of ()
for U being FieldExtension of F
for E being b3 -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) c= Roots (U,p) )
proof end;

theorem :: FIELD_8:29
for F being Field
for p being non constant Element of the carrier of ()
for U being FieldExtension of F
for E being b3 -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) = Roots (U,p) )
proof end;

theorem lemma5: :: FIELD_8:30
for F being Field
for p being non constant Element of the carrier of ()
for E being FieldExtension of F st p splits_in E holds
proof end;

definition
let F be Field;
let p be non constant Element of the carrier of ();
mode SplittingField of p -> FieldExtension of F means :defspl: :: FIELD_8:def 1
( p splits_in it & ( for E being FieldExtension of F st p splits_in E & E is Subfield of it holds
E == it ) );
existence
ex b1 being FieldExtension of F st
( p splits_in b1 & ( for E being FieldExtension of F st p splits_in E & E is Subfield of b1 holds
E == b1 ) )
proof end;
end;

:: deftheorem defspl defines SplittingField FIELD_8:def 1 :
for F being Field
for p being non constant Element of the carrier of ()
for b3 being FieldExtension of F holds
( b3 is SplittingField of p iff ( p splits_in b3 & ( for E being FieldExtension of F st p splits_in E & E is Subfield of b3 holds
E == b3 ) ) );

theorem :: FIELD_8:31
for F being Field
for p being non constant Element of the carrier of () ex E being FieldExtension of F st E is SplittingField of p
proof end;

theorem spl0: :: FIELD_8:32
for F being Field
for p being non constant Element of the carrier of () ex E being FieldExtension of F st FAdj (F,(Roots (E,p))) is SplittingField of p
proof end;

theorem spl1: :: FIELD_8:33
for F being Field
for p being non constant Element of the carrier of ()
for E being FieldExtension of F st p splits_in E holds
FAdj (F,(Roots (E,p))) is SplittingField of p
proof end;

theorem XX: :: FIELD_8:34
for F being Field
for p being non constant Element of the carrier of ()
for E being SplittingField of p holds E == FAdj (F,(Roots (E,p)))
proof end;

registration
let F be Field;
let p be non constant Element of the carrier of ();
existence
ex b1 being SplittingField of p st b1 is strict
proof end;
end;

registration
let F be Field;
let p be non constant Element of the carrier of ();
cluster -> F -finite for SplittingField of p;
coherence
for b1 being SplittingField of p holds b1 is F -finite
proof end;
end;

registration
let R be Ring;
cluster V1() V4( the carrier of R) V5( the carrier of R) Function-like non empty total quasi_total isomorphism for Element of bool [: the carrier of R, the carrier of R:];
existence
ex b1 being Function of R,R st b1 is isomorphism
proof end;
end;

definition end;

definition
let R, S2 be Ring;
let S1 be RingExtension of R;
let h be Function of S1,S2;
attr h is R -fixing means :deffix: :: FIELD_8:def 2
for a being Element of R holds h . a = a;
end;

:: deftheorem deffix defines -fixing FIELD_8:def 2 :
for R, S2 being Ring
for S1 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -fixing iff for a being Element of R holds h . a = a );

theorem e0: :: FIELD_8:35
for R, S2 being Ring
for S1 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -fixing iff h | R = id R )
proof end;

theorem lintrans: :: FIELD_8:36
for F being Field
for E1 being FieldExtension of F
for E2 being b2 -homomorphic FieldExtension of F
for h being Homomorphism of E1,E2 holds
( h is F -fixing iff h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F)) )
proof end;

theorem :: FIELD_8:37
for F being Field
for E being FieldExtension of F
for E1, E2 being b2 -extending FieldExtension of F
for h being Function of E1,E2 st h is E -fixing holds
h is F -fixing
proof end;

definition
let R be Ring;
let S1, S2 be RingExtension of R;
let h be Function of S1,S2;
attr h is R -homomorphism means :: FIELD_8:def 3
( h is R -fixing & h is additive & h is multiplicative & h is unity-preserving );
attr h is R -monomorphism means :: FIELD_8:def 4
( h is R -fixing & h is monomorphism );
attr h is R -isomorphism means :deffixiso: :: FIELD_8:def 5
( h is R -fixing & h is isomorphism );
end;

:: deftheorem defines -homomorphism FIELD_8:def 3 :
for R being Ring
for S1, S2 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -homomorphism iff ( h is R -fixing & h is additive & h is multiplicative & h is unity-preserving ) );

:: deftheorem defines -monomorphism FIELD_8:def 4 :
for R being Ring
for S1, S2 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -monomorphism iff ( h is R -fixing & h is monomorphism ) );

:: deftheorem deffixiso defines -isomorphism FIELD_8:def 5 :
for R being Ring
for S1, S2 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -isomorphism iff ( h is R -fixing & h is isomorphism ) );

registration
let R be Ring;
let S be RingExtension of R;
existence
ex b1 being Automorphism of S st b1 is R -fixing
proof end;
end;

theorem prm: :: FIELD_8:38
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of ()
for h being b1 -fixing Monomorphism of S
for a being Element of S holds
( a in Roots (S,p) iff h . a in Roots (S,p) )
proof end;

theorem :: FIELD_8:39
for R being domRing
for S being domRingExtension of R
for p being non zero Element of the carrier of ()
for h being b1 -fixing Monomorphism of S holds h | (Roots (S,p)) is Permutation of (Roots (S,p))
proof end;

definition
let R1, R2, S2 be Ring;
let S1 be RingExtension of R1;
let h1 be Function of R1,R2;
let h2 be Function of S1,S2;
attr h2 is h1 -extending means :: FIELD_8:def 6
for a being Element of R1 holds h2 . a = h1 . a;
end;

:: deftheorem defines -extending FIELD_8:def 6 :
for R1, R2, S2 being Ring
for S1 being RingExtension of R1
for h1 being Function of R1,R2
for h2 being Function of S1,S2 holds
( h2 is h1 -extending iff for a being Element of R1 holds h2 . a = h1 . a );

theorem e1: :: FIELD_8:40
for R1, R2, S2 being Ring
for S1 being RingExtension of R1
for h1 being Function of R1,R2
for h2 being Function of S1,S2 holds
( h2 is h1 -extending iff h2 | R1 = h1 )
proof end;

registration
let R be Ring;
let S be RingExtension of R;
cluster Function-like quasi_total RingIsomorphism R -fixing -> id R -extending for Element of bool [: the carrier of S, the carrier of S:];
coherence
for b1 being Automorphism of S st b1 is R -fixing holds
b1 is id R -extending
;
cluster Function-like quasi_total RingIsomorphism id R -extending -> R -fixing for Element of bool [: the carrier of S, the carrier of S:];
coherence
for b1 being Automorphism of S st b1 is id R -extending holds
b1 is R -fixing
proof end;
end;

theorem e1a: :: FIELD_8:41
for F1, F2 being Field
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for K1 being b3 -extending FieldExtension of F1
for K2 being b4 -extending FieldExtension of F2
for h1 being Function of F1,F2
for h2 being Function of E1,E2
for h3 being Function of K1,K2 st h2 is h1 -extending & h3 is h2 -extending holds
h3 is h1 -extending
proof end;

definition
let F be Field;
let E1, E2 be FieldExtension of F;
pred E1,E2 are_isomorphic_over F means :: FIELD_8:def 7
ex i being Function of E1,E2 st i is F -isomorphism ;
end;

:: deftheorem defines are_isomorphic_over FIELD_8:def 7 :
for F being Field
for E1, E2 being FieldExtension of F holds
( E1,E2 are_isomorphic_over F iff ex i being Function of E1,E2 st i is F -isomorphism );

theorem :: FIELD_8:42
for F being Field
for E being FieldExtension of F holds E,E are_isomorphic_over F
proof end;

theorem :: FIELD_8:43
for F being Field
for E1, E2 being FieldExtension of F st E1,E2 are_isomorphic_over F holds
E2,E1 are_isomorphic_over F
proof end;

theorem :: FIELD_8:44
for F being Field
for E1, E2, E3 being FieldExtension of F st E1,E2 are_isomorphic_over F & E2,E3 are_isomorphic_over F holds
E1,E3 are_isomorphic_over F
proof end;

theorem :: FIELD_8:45
for F being Field
for E1 being b1 -finite FieldExtension of F
for E2 being FieldExtension of F st E1,E2 are_isomorphic_over F holds
( E2 is F -finite & deg (E1,F) = deg (E2,F) )
proof end;

definition
let R be Ring;
let S1, S2 be RingExtension of R;
let h be Relation of the carrier of S1, the carrier of S2;
attr h is R -isomorphism means :: FIELD_8:def 8
ex g being Function of S1,S2 st
( g = h & g is R -isomorphism );
end;

:: deftheorem defines -isomorphism FIELD_8:def 8 :
for R being Ring
for S1, S2 being RingExtension of R
for h being Relation of the carrier of S1, the carrier of S2 holds
( h is R -isomorphism iff ex g being Function of S1,S2 st
( g = h & g is R -isomorphism ) );

theorem u1: :: FIELD_8:46
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E holds
( 0. (FAdj (F,{a})) = Ext_eval ((0_. F),a) & 1. (FAdj (F,{a})) = Ext_eval ((1_. F),a) )
proof end;

theorem u2: :: FIELD_8:47
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for x, y being Element of (FAdj (F,{a}))
for p, q being Polynomial of F st x = Ext_eval (p,a) & y = Ext_eval (q,a) holds
( x + y = Ext_eval ((p + q),a) & x * y = Ext_eval ((p *' q),a) )
proof end;

theorem u3: :: FIELD_8:48
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for x being Element of F holds x = Ext_eval ((x | F),a)
proof end;

theorem u10: :: FIELD_8:49
for F being Field
for E being FieldExtension of F
for a being Element of E holds hom_Ext_eval (a,F) is Function of (),(RAdj (F,{a}))
proof end;

theorem :: FIELD_8:50
for F being Field
for E being FieldExtension of F
for a being Element of E holds hom_Ext_eval (a,F) is Function of (),(FAdj (F,{a}))
proof end;

theorem x1000: :: FIELD_8:51
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being b1 -algebraic Element of E1
for b being b2 -algebraic Element of E2
for p being irreducible Element of the carrier of () st Ext_eval (p,a) = 0. E1 & Ext_eval ((() . p),b) = 0. E2 holds
() . (MinPoly (a,F1)) = MinPoly (b,F2)
proof end;

theorem :: FIELD_8:52
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being b1 -algebraic Element of E1
for b being b2 -algebraic Element of E2 st Ext_eval ((() . (MinPoly (a,F1))),b) = 0. E2 holds
() . (MinPoly (a,F1)) = MinPoly (b,F2)
proof end;

theorem splift: :: FIELD_8:53
for F1 being Field
for p1 being non constant Element of the carrier of ()
for F2 being FieldExtension of F1
for p2 being non constant Element of the carrier of ()
for E being SplittingField of p1 st p2 = p1 & E is F2 -extending holds
E is SplittingField of p2
proof end;

definition
let F be Field;
let E be FieldExtension of F;
let a, b be F -algebraic Element of E;
func Phi (a,b) -> Relation of the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{b})) equals :: FIELD_8:def 9
{ [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } ;
coherence
{ [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } is Relation of the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{b}))
proof end;
end;

:: deftheorem defines Phi FIELD_8:def 9 :
for F being Field
for E being FieldExtension of F
for a, b being b1 -algebraic Element of E holds Phi (a,b) = { [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } ;

registration
let F be Field;
let E be FieldExtension of F;
let a, b be F -algebraic Element of E;
cluster Phi (a,b) -> quasi_total ;
coherence
Phi (a,b) is quasi_total
proof end;
end;

theorem :: FIELD_8:54
for F being Field
for E being FieldExtension of F
for a, b being b1 -algebraic Element of E holds
( Phi (a,b) is F -isomorphism iff MinPoly (a,F) = MinPoly (b,F) )
proof end;

definition
let F1 be Field;
let F2 be F1 -homomorphic F1 -isomorphic Field;
let h be Isomorphism of F1,F2;
let E1 be FieldExtension of F1;
let E2 be FieldExtension of F2;
let a be Element of E1;
let b be Element of E2;
let p be irreducible Element of the carrier of ();
assume AS: ( Ext_eval (p,a) = 0. E1 & Ext_eval ((() . p),b) = 0. E2 ) ;
func Psi (a,b,h,p) -> Function of (FAdj (F1,{a})),(FAdj (F2,{b})) means :psi: :: FIELD_8:def 10
for r being Element of the carrier of () holds it . (Ext_eval (r,a)) = Ext_eval ((() . r),b);
existence
for r being Element of the carrier of () holds b1 . (Ext_eval (r,a)) = Ext_eval ((() . r),b)
proof end;
uniqueness
for b1, b2 being Function of (FAdj (F1,{a})),(FAdj (F2,{b})) st ( for r being Element of the carrier of () holds b1 . (Ext_eval (r,a)) = Ext_eval ((() . r),b) ) & ( for r being Element of the carrier of () holds b2 . (Ext_eval (r,a)) = Ext_eval ((() . r),b) ) holds
b1 = b2
proof end;
end;

:: deftheorem psi defines Psi FIELD_8:def 10 :
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of () st Ext_eval (p,a) = 0. E1 & Ext_eval ((() . p),b) = 0. E2 holds
( b9 = Psi (a,b,h,p) iff for r being Element of the carrier of () holds b9 . (Ext_eval (r,a)) = Ext_eval ((() . r),b) );

theorem unique1: :: FIELD_8:55
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of () st Ext_eval (p,a) = 0. E1 & Ext_eval ((() . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
proof end;

theorem :: FIELD_8:56
for F being Field
for E being FieldExtension of F
for p being irreducible Element of the carrier of ()
for a, b being Element of E st a is_a_root_of p,E & b is_a_root_of p,E holds
proof end;

unique20: for F1, F2 being Field st F1 is Subfield of F2 & F2 is Subfield of F1 holds
for f being Function of F1,F2 st f = id F1 holds
f is isomorphism

proof end;

theorem unique2: :: FIELD_8:57
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of ()
for E1 being SplittingField of p
for E2 being SplittingField of () . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
proof end;

unique3: for F being Field
for p being non constant Element of the carrier of ()
for E1, E2 being SplittingField of p ex h being Function of E1,E2 st h is F -isomorphism

proof end;

theorem :: FIELD_8:58
for F being Field
for p being non constant Element of the carrier of ()
for E1, E2 being SplittingField of p holds E1,E2 are_isomorphic_over F
proof end;