let F be Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st p is_with_roots_in E

let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: ex E being FieldExtension of F st p is_with_roots_in E

set KF = KroneckerField (F,p);

set u = KrRoot p;

consider FP being Field such that

X1: ( KroneckerField (F,p),FP are_isomorphic & the carrier of FP /\ ( the carrier of (KroneckerField (F,p)) \/ the carrier of F) = {} ) by thisofield;

X: ( [#] F = the carrier of F & [#] FP = the carrier of FP ) ;

X2: F,FP are_disjoint

X3: phi is isomorphism by X1;

reconsider KroneckerIsop = (KroneckerIso p) " as Isomorphism of (KroneckerField (F,p)),(Polynom-Ring p) by RING_3:73;

set h = phi * (emb p);

reconsider h = phi * (emb p) as Function of F,FP by FUNCT_2:13;

X4: ( h is linear & h is one-to-one ) by X3, RINGCAT1:1;

then reconsider FP = FP as F -monomorphic Field by RING_3:def 3;

reconsider h = h as Monomorphism of F,FP by X4;

reconsider E = embField h as Field by X2, FIELD_2:12;

emb_iso h is onto by X2, FIELD_2:15;

then reconsider embisoh = (emb_iso h) " as Function of FP,E by FUNCT_2:25;

Y: ( emb_iso h is linear & emb_iso h is one-to-one & emb_iso h is onto ) by X2, FIELD_2:13, FIELD_2:14, FIELD_2:15;

then reconsider FP = FP as E -isomorphic Field by RING_3:def 4;

reconsider embisoh = embisoh as Isomorphism of FP,E by Y, RING_3:73;

set iso = embisoh * phi;

reconsider iso = embisoh * phi as Function of (KroneckerField (F,p)),E by FUNCT_2:13;

X5: iso is RingHomomorphism by X3, RINGCAT1:1;

then reconsider E = E as KroneckerField (F,p) -homomorphic Field by RING_2:def 4;

reconsider iso = iso as Homomorphism of (KroneckerField (F,p)),E by X5;

KrRoot p is_a_root_of emb (p,p) by FIELD_1:42;

then Z: eval (((PolyHom iso) . (emb (p,p))),(iso . (KrRoot p))) = 0. E by FIELD_1:33, POLYNOM5:def 7;

F is Subfield of E by FIELD_2:17;

then reconsider E = E as FieldExtension of F by FIELD_4:7;

take E ; :: thesis: p is_with_roots_in E

reconsider a = iso . (KrRoot p) as Element of E ;

(PolyHom iso) . (emb (p,p)) = p

hence p is_with_roots_in E by FIELD_4:def 3, FIELD_4:def 2; :: thesis: verum

let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: ex E being FieldExtension of F st p is_with_roots_in E

set KF = KroneckerField (F,p);

set u = KrRoot p;

consider FP being Field such that

X1: ( KroneckerField (F,p),FP are_isomorphic & the carrier of FP /\ ( the carrier of (KroneckerField (F,p)) \/ the carrier of F) = {} ) by thisofield;

X: ( [#] F = the carrier of F & [#] FP = the carrier of FP ) ;

X2: F,FP are_disjoint

proof

end;

consider phi being Function of (KroneckerField (F,p)),FP such that now :: thesis: not the carrier of F /\ the carrier of FP <> {}

hence
F,FP are_disjoint
by X, FIELD_2:def 1; :: thesis: verumassume A:
the carrier of F /\ the carrier of FP <> {}
; :: thesis: contradiction

set x = the Element of the carrier of F /\ the carrier of FP;

B: ( the Element of the carrier of F /\ the carrier of FP in the carrier of F & the Element of the carrier of F /\ the carrier of FP in the carrier of FP ) by A, XBOOLE_0:def 4;

then the Element of the carrier of F /\ the carrier of FP in the carrier of (KroneckerField (F,p)) \/ the carrier of F by XBOOLE_0:def 3;

hence contradiction by B, X1, XBOOLE_0:def 4; :: thesis: verum

end;set x = the Element of the carrier of F /\ the carrier of FP;

B: ( the Element of the carrier of F /\ the carrier of FP in the carrier of F & the Element of the carrier of F /\ the carrier of FP in the carrier of FP ) by A, XBOOLE_0:def 4;

then the Element of the carrier of F /\ the carrier of FP in the carrier of (KroneckerField (F,p)) \/ the carrier of F by XBOOLE_0:def 3;

hence contradiction by B, X1, XBOOLE_0:def 4; :: thesis: verum

X3: phi is isomorphism by X1;

reconsider KroneckerIsop = (KroneckerIso p) " as Isomorphism of (KroneckerField (F,p)),(Polynom-Ring p) by RING_3:73;

set h = phi * (emb p);

reconsider h = phi * (emb p) as Function of F,FP by FUNCT_2:13;

X4: ( h is linear & h is one-to-one ) by X3, RINGCAT1:1;

then reconsider FP = FP as F -monomorphic Field by RING_3:def 3;

reconsider h = h as Monomorphism of F,FP by X4;

reconsider E = embField h as Field by X2, FIELD_2:12;

emb_iso h is onto by X2, FIELD_2:15;

then reconsider embisoh = (emb_iso h) " as Function of FP,E by FUNCT_2:25;

Y: ( emb_iso h is linear & emb_iso h is one-to-one & emb_iso h is onto ) by X2, FIELD_2:13, FIELD_2:14, FIELD_2:15;

then reconsider FP = FP as E -isomorphic Field by RING_3:def 4;

reconsider embisoh = embisoh as Isomorphism of FP,E by Y, RING_3:73;

set iso = embisoh * phi;

reconsider iso = embisoh * phi as Function of (KroneckerField (F,p)),E by FUNCT_2:13;

X5: iso is RingHomomorphism by X3, RINGCAT1:1;

then reconsider E = E as KroneckerField (F,p) -homomorphic Field by RING_2:def 4;

reconsider iso = iso as Homomorphism of (KroneckerField (F,p)),E by X5;

KrRoot p is_a_root_of emb (p,p) by FIELD_1:42;

then Z: eval (((PolyHom iso) . (emb (p,p))),(iso . (KrRoot p))) = 0. E by FIELD_1:33, POLYNOM5:def 7;

F is Subfield of E by FIELD_2:17;

then reconsider E = E as FieldExtension of F by FIELD_4:7;

take E ; :: thesis: p is_with_roots_in E

reconsider a = iso . (KrRoot p) as Element of E ;

(PolyHom iso) . (emb (p,p)) = p

proof

then
Ext_eval (p,a) = 0. E
by Z, FIELD_4:26;
set g = (PolyHom iso) . (emb (p,p));

A: for a being Element of F holds iso . ((emb p) . a) = a

end;A: for a being Element of F holds iso . ((emb p) . a) = a

proof

let a be Element of F; :: thesis: iso . ((emb p) . a) = a

reconsider b = a | F as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

reconsider v = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b) as Element of (KroneckerField (F,p)) by RING_1:12;

dom (emb p) = the carrier of F by FUNCT_2:def 1;

then C: h . a = phi . ((emb p) . a) by FUNCT_1:13

.= phi . v by FIELD_1:39 ;

the carrier of (embField h) = carr h by FIELD_2:def 7

.= (([#] FP) \ (rng h)) \/ ([#] F) by FIELD_2:def 2

.= ( the carrier of FP \ (rng h)) \/ the carrier of F ;

then reconsider a1 = a as Element of (embField h) by XBOOLE_0:def 3;

a in F ;

then D: (emb_iso h) . a1 = phi . v by C, FIELD_2:def 8;

A1: dom phi = the carrier of (KroneckerField (F,p)) by FUNCT_2:def 1;

A3: dom (emb_iso h) = the carrier of E by FUNCT_2:def 1;

thus iso . ((emb p) . a) = (embisoh * phi) . v by FIELD_1:39

.= ((emb_iso h) ") . (phi . v) by A1, FUNCT_1:13

.= a by D, A3, FUNCT_1:34 ; :: thesis: verum

end;reconsider b = a | F as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

reconsider v = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b) as Element of (KroneckerField (F,p)) by RING_1:12;

dom (emb p) = the carrier of F by FUNCT_2:def 1;

then C: h . a = phi . ((emb p) . a) by FUNCT_1:13

.= phi . v by FIELD_1:39 ;

the carrier of (embField h) = carr h by FIELD_2:def 7

.= (([#] FP) \ (rng h)) \/ ([#] F) by FIELD_2:def 2

.= ( the carrier of FP \ (rng h)) \/ the carrier of F ;

then reconsider a1 = a as Element of (embField h) by XBOOLE_0:def 3;

a in F ;

then D: (emb_iso h) . a1 = phi . v by C, FIELD_2:def 8;

A1: dom phi = the carrier of (KroneckerField (F,p)) by FUNCT_2:def 1;

A3: dom (emb_iso h) = the carrier of E by FUNCT_2:def 1;

thus iso . ((emb p) . a) = (embisoh * phi) . v by FIELD_1:39

.= ((emb_iso h) ") . (phi . v) by A1, FUNCT_1:13

.= a by D, A3, FUNCT_1:34 ; :: thesis: verum

now :: thesis: for x being object st x in NAT holds

((PolyHom iso) . (emb (p,p))) . x = p . x

hence
(PolyHom iso) . (emb (p,p)) = p
; :: thesis: verum((PolyHom iso) . (emb (p,p))) . x = p . x

let x be object ; :: thesis: ( x in NAT implies ((PolyHom iso) . (emb (p,p))) . x = p . x )

assume x in NAT ; :: thesis: ((PolyHom iso) . (emb (p,p))) . x = p . x

then reconsider i = x as Element of NAT ;

((PolyHom iso) . (emb (p,p))) . i = iso . ((emb (p,p)) . i) by FIELD_1:def 2

.= iso . (Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),((p . i) | F))) by FIELD_1:40

.= iso . ((emb p) . (p . i)) by FIELD_1:39 ;

hence ((PolyHom iso) . (emb (p,p))) . x = p . x by A; :: thesis: verum

end;assume x in NAT ; :: thesis: ((PolyHom iso) . (emb (p,p))) . x = p . x

then reconsider i = x as Element of NAT ;

((PolyHom iso) . (emb (p,p))) . i = iso . ((emb (p,p)) . i) by FIELD_1:def 2

.= iso . (Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),((p . i) | F))) by FIELD_1:40

.= iso . ((emb p) . (p . i)) by FIELD_1:39 ;

hence ((PolyHom iso) . (emb (p,p))) . x = p . x by A; :: thesis: verum

hence p is_with_roots_in E by FIELD_4:def 3, FIELD_4:def 2; :: thesis: verum