let F be polynomial_disjoint 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 h = KroneckerIsop * (emb p);

reconsider h = KroneckerIsop * (emb p) as Function of F,(Polynom-Ring p) by FUNCT_2:13;

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

then reconsider h = h as Monomorphism of F,(Polynom-Ring p) ;

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

emb_iso h is onto by A1, FIELD_2:15;

then reconsider embisoh = (emb_iso h) " as Function of (Polynom-Ring p),E by FUNCT_2:25;

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

then reconsider P = Polynom-Ring p as E -isomorphic Field by RING_3:def 4;

reconsider embisoh = embisoh as Isomorphism of P,E by A5, RING_3:73;

set iso = embisoh * KroneckerIsop;

set u = KrRoot p;

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

A6: iso is RingHomomorphism by 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 A6;

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

then A7: 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 Th4;

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 ; :: 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

A1: now :: thesis: ( not F, Polynom-Ring p are_disjoint implies for a being Element of the carrier of F /\ the carrier of (Polynom-Ring p) holds contradiction )

reconsider KroneckerIsop = (KroneckerIso p) " as Isomorphism of (KroneckerField (F,p)),(Polynom-Ring p) by RING_3:73;assume
not F, Polynom-Ring p are_disjoint
; :: thesis: for a being Element of the carrier of F /\ the carrier of (Polynom-Ring p) holds contradiction

then A2: ([#] F) /\ ([#] (Polynom-Ring p)) <> {} by FIELD_2:def 1;

let a be Element of the carrier of F /\ the carrier of (Polynom-Ring p); :: thesis: contradiction

A3: ( a in the carrier of F & a in the carrier of (Polynom-Ring p) ) by A2, XBOOLE_0:def 4;

the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;

then consider q being Polynomial of F such that

A4: ( a = q & deg q < deg p ) by A3;

a in the carrier of (Polynom-Ring F) by A4, POLYNOM3:def 10;

then a in ([#] F) /\ ([#] (Polynom-Ring F)) by A3, XBOOLE_0:def 4;

hence contradiction by FIELD_3:def 3; :: thesis: verum

end;then A2: ([#] F) /\ ([#] (Polynom-Ring p)) <> {} by FIELD_2:def 1;

let a be Element of the carrier of F /\ the carrier of (Polynom-Ring p); :: thesis: contradiction

A3: ( a in the carrier of F & a in the carrier of (Polynom-Ring p) ) by A2, XBOOLE_0:def 4;

the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;

then consider q being Polynomial of F such that

A4: ( a = q & deg q < deg p ) by A3;

a in the carrier of (Polynom-Ring F) by A4, POLYNOM3:def 10;

then a in ([#] F) /\ ([#] (Polynom-Ring F)) by A3, XBOOLE_0:def 4;

hence contradiction by FIELD_3:def 3; :: thesis: verum

set h = KroneckerIsop * (emb p);

reconsider h = KroneckerIsop * (emb p) as Function of F,(Polynom-Ring p) by FUNCT_2:13;

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

then reconsider h = h as Monomorphism of F,(Polynom-Ring p) ;

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

emb_iso h is onto by A1, FIELD_2:15;

then reconsider embisoh = (emb_iso h) " as Function of (Polynom-Ring p),E by FUNCT_2:25;

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

then reconsider P = Polynom-Ring p as E -isomorphic Field by RING_3:def 4;

reconsider embisoh = embisoh as Isomorphism of P,E by A5, RING_3:73;

set iso = embisoh * KroneckerIsop;

set u = KrRoot p;

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

A6: iso is RingHomomorphism by 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 A6;

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

then A7: 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 Th4;

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
a is_a_root_of p,E
by A7, Th15;
set g = (PolyHom iso) . (emb (p,p));

A8: KroneckerField (F,p) = (Polynom-Ring F) / ({p} -Ideal) by FIELD_1:def 3;

A9: for a being Element of F holds h . a = a | F

end;A8: KroneckerField (F,p) = (Polynom-Ring F) / ({p} -Ideal) by FIELD_1:def 3;

A9: for a being Element of F holds h . a = a | F

proof

A13:
for a being Element of F holds iso . ((emb p) . a) = a
let a be Element of F; :: thesis: h . a = a | F

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

then A10: h . a = KroneckerIsop . ((emb p) . a) by FUNCT_1:13

.= KroneckerIsop . (Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(a | F))) by FIELD_1:39 ;

A11: the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;

( deg (a | F) <= 0 & deg p > 0 ) by RATFUNC1:def 2, RING_4:def 4;

then a | F in the carrier of (Polynom-Ring p) by A11;

then reconsider b1 = a | F as Element of (Polynom-Ring p) ;

A12: dom (KroneckerIso p) = the carrier of (Polynom-Ring p) by FUNCT_2:def 1;

(KroneckerIso p) . b1 = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b1) by Def8;

hence h . a = a | F by A12, A10, FUNCT_1:32; :: thesis: verum

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

then A10: h . a = KroneckerIsop . ((emb p) . a) by FUNCT_1:13

.= KroneckerIsop . (Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(a | F))) by FIELD_1:39 ;

A11: the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;

( deg (a | F) <= 0 & deg p > 0 ) by RATFUNC1:def 2, RING_4:def 4;

then a | F in the carrier of (Polynom-Ring p) by A11;

then reconsider b1 = a | F as Element of (Polynom-Ring p) ;

A12: dom (KroneckerIso p) = the carrier of (Polynom-Ring p) by FUNCT_2:def 1;

(KroneckerIso p) . b1 = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b1) by Def8;

hence h . a = a | F by A12, A10, FUNCT_1:32; :: thesis: verum

proof

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

rng (KroneckerIso p) = the carrier of (KroneckerField (F,p)) by FUNCT_2:def 3;

then A14: dom KroneckerIsop = the carrier of (KroneckerField (F,p)) by FUNCT_1:33;

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

A15: the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;

( deg (a | F) <= 0 & deg p > 0 ) by RATFUNC1:def 2, RING_4:def 4;

then a | F in the carrier of (Polynom-Ring p) by A15;

then reconsider b1 = a | F as Element of (Polynom-Ring p) ;

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

A16: (KroneckerIso p) . b1 = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b1) by Def8;

A17: dom (KroneckerIso p) = the carrier of (Polynom-Ring p) by FUNCT_2:def 1;

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

.= (([#] (Polynom-Ring p)) \ (rng h)) \/ ([#] F) by FIELD_2:def 2 ;

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

a in F ;

then A18: (emb_iso h) . a1 = h . a by FIELD_2:def 8

.= a | F by A9 ;

A19: dom (emb_iso h) = the carrier of (embField h) by FUNCT_2:def 1;

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

.= embisoh . (KroneckerIsop . v) by A14, FUNCT_1:13

.= embisoh . b by A16, A17, FUNCT_1:32

.= a by A18, A19, FUNCT_1:32 ; :: thesis: verum

end;rng (KroneckerIso p) = the carrier of (KroneckerField (F,p)) by FUNCT_2:def 3;

then A14: dom KroneckerIsop = the carrier of (KroneckerField (F,p)) by FUNCT_1:33;

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

A15: the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;

( deg (a | F) <= 0 & deg p > 0 ) by RATFUNC1:def 2, RING_4:def 4;

then a | F in the carrier of (Polynom-Ring p) by A15;

then reconsider b1 = a | F as Element of (Polynom-Ring p) ;

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

A16: (KroneckerIso p) . b1 = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b1) by Def8;

A17: dom (KroneckerIso p) = the carrier of (Polynom-Ring p) by FUNCT_2:def 1;

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

.= (([#] (Polynom-Ring p)) \ (rng h)) \/ ([#] F) by FIELD_2:def 2 ;

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

a in F ;

then A18: (emb_iso h) . a1 = h . a by FIELD_2:def 8

.= a | F by A9 ;

A19: dom (emb_iso h) = the carrier of (embField h) by FUNCT_2:def 1;

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

.= embisoh . (KroneckerIsop . v) by A14, FUNCT_1:13

.= embisoh . b by A16, A17, FUNCT_1:32

.= a by A18, A19, FUNCT_1:32 ; :: 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 A13; :: 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 A13; :: thesis: verum

hence p is_with_roots_in E ; :: thesis: verum