let F be Field; :: thesis: for f being non constant Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st f splits_in E

let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ex E being FieldExtension of F st f splits_in E

defpred S_{1}[ Nat] means for F being Field

for f being non constant Element of the carrier of (Polynom-Ring F) st deg f = $1 holds

ex E being FieldExtension of F st f splits_in E;

IA: S_{1}[1]
_{1}[k]
from NAT_1:sch 10(IA, IS);

consider n being Nat such that

H: deg f = n ;

n + 1 > 0 + 1 by H, RING_4:def 4, XREAL_1:6;

hence ex E being FieldExtension of F st f splits_in E by I, H; :: thesis: verum

let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ex E being FieldExtension of F st f splits_in E

defpred S

for f being non constant Element of the carrier of (Polynom-Ring F) st deg f = $1 holds

ex E being FieldExtension of F st f splits_in E;

IA: S

proof

let F be Field; :: thesis: for f being non constant Element of the carrier of (Polynom-Ring F) st deg f = 1 holds

ex E being FieldExtension of F st f splits_in E

let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( deg f = 1 implies ex E being FieldExtension of F st f splits_in E )

assume A: deg f = 1 ; :: thesis: ex E being FieldExtension of F st f splits_in E

reconsider E = F as FieldExtension of F by FIELD_4:6;

take E ; :: thesis: f splits_in E

thus f splits_in E by FIELD_4:29, A; :: thesis: verum

end;ex E being FieldExtension of F st f splits_in E

let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( deg f = 1 implies ex E being FieldExtension of F st f splits_in E )

assume A: deg f = 1 ; :: thesis: ex E being FieldExtension of F st f splits_in E

reconsider E = F as FieldExtension of F by FIELD_4:6;

take E ; :: thesis: f splits_in E

thus f splits_in E by FIELD_4:29, A; :: thesis: verum

IS: now :: thesis: for k being non zero Nat st S_{1}[k] holds

S_{1}[k + 1]

I:
for k being non zero Nat holds SS

let k be non zero Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume IV: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume IV: S

now :: thesis: for F being Field

for f being non constant Element of the carrier of (Polynom-Ring F) st deg f = k + 1 holds

ex E being FieldExtension of F st f splits_in E

hence
Sfor f being non constant Element of the carrier of (Polynom-Ring F) st deg f = k + 1 holds

ex E being FieldExtension of F st f splits_in E

let F be Field; :: thesis: for f being non constant Element of the carrier of (Polynom-Ring F) st deg f = k + 1 holds

ex E being FieldExtension of E st b_{3} splits_in b_{4}

let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( deg f = k + 1 implies ex E being FieldExtension of E st b_{2} splits_in b_{3} )

assume AS2: deg f = k + 1 ; :: thesis: ex E being FieldExtension of E st b_{2} splits_in b_{3}

consider E1 being FieldExtension of F such that

A: f is_with_roots_in E1 by main;

reconsider f1 = f as Polynomial of E1 by FIELD_4:8;

reconsider f1 = f1 as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;

consider a being Element of E1 such that

B: a is_a_root_of f,E1 by A, FIELD_4:def 3;

reconsider h = rpoly (1,a) as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;

reconsider q = rpoly (1,a) as Ppoly of E1 by RING_5:51;

Ext_eval (f,a) = 0. E1 by B, FIELD_4:def 2;

then 0. E1 = eval (f1,a) by FIELD_4:26;

then consider g2 being Polynomial of E1 such that

C1: f1 = h *' g2 by RING_4:1, RING_5:11;

reconsider g = g2 as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;

C: f1 = h * g by C1, POLYNOM3:def 10;

end;ex E being FieldExtension of E st b

let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( deg f = k + 1 implies ex E being FieldExtension of E st b

assume AS2: deg f = k + 1 ; :: thesis: ex E being FieldExtension of E st b

consider E1 being FieldExtension of F such that

A: f is_with_roots_in E1 by main;

reconsider f1 = f as Polynomial of E1 by FIELD_4:8;

reconsider f1 = f1 as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;

consider a being Element of E1 such that

B: a is_a_root_of f,E1 by A, FIELD_4:def 3;

reconsider h = rpoly (1,a) as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;

reconsider q = rpoly (1,a) as Ppoly of E1 by RING_5:51;

Ext_eval (f,a) = 0. E1 by B, FIELD_4:def 2;

then 0. E1 = eval (f1,a) by FIELD_4:26;

then consider g2 being Polynomial of E1 such that

C1: f1 = h *' g2 by RING_4:1, RING_5:11;

reconsider g = g2 as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;

C: f1 = h * g by C1, POLYNOM3:def 10;

per cases
( g is constant or not g is constant )
;

end;

suppose
g is constant
; :: thesis: ex E being FieldExtension of E st b_{2} splits_in b_{3}

then consider e being Element of E1 such that

D: g = e | E1 by RING_4:20;

f = (rpoly (1,a)) *' (e * (1_. E1)) by D, C1, RING_4:16

.= e * ((rpoly (1,a)) *' (1_. E1)) by RING_4:10

.= e * q ;

hence ex E being FieldExtension of F st f splits_in E by FIELD_4:def 5; :: thesis: verum

end;D: g = e | E1 by RING_4:20;

now :: thesis: not e is zero

then reconsider e = e as non zero Element of E1 ;assume
e is zero
; :: thesis: contradiction

then g = 0_. E1 by D, RING_4:13;

then f = 0_. F by C1, FIELD_4:12;

hence contradiction ; :: thesis: verum

end;then g = 0_. E1 by D, RING_4:13;

then f = 0_. F by C1, FIELD_4:12;

hence contradiction ; :: thesis: verum

f = (rpoly (1,a)) *' (e * (1_. E1)) by D, C1, RING_4:16

.= e * ((rpoly (1,a)) *' (1_. E1)) by RING_4:10

.= e * q ;

hence ex E being FieldExtension of F st f splits_in E by FIELD_4:def 5; :: thesis: verum

suppose I:
not g is constant
; :: thesis: ex E being FieldExtension of E st b_{2} splits_in b_{3}

deg g = k

E: g splits_in E2 by I, IV;

reconsider E2 = E2 as FieldExtension of F ;

consider e being non zero Element of E2, r being Ppoly of E2 such that

F: g = e * r by E, FIELD_4:def 5;

E1 is Subring of E2 by FIELD_4:def 1;

then the carrier of E1 c= the carrier of E2 by C0SP1:def 3;

then reconsider a1 = a as Element of E2 ;

rpoly (1,a1) is Ppoly of E2 by RING_5:51;

then reconsider u = (rpoly (1,a1)) *' r as Ppoly of E2 by RING_5:52;

reconsider q = rpoly (1,a) as Polynomial of E2 by FIELD_4:8;

reconsider q1 = q as Element of the carrier of (Polynom-Ring E2) by POLYNOM3:def 10;

reconsider eg = e * r as Element of the carrier of (Polynom-Ring E2) by POLYNOM3:def 10;

Y: q = rpoly (1,a1) by FIELD_4:21;

Z1: [h,g] in [: the carrier of (Polynom-Ring E1), the carrier of (Polynom-Ring E1):] by ZFMISC_1:def 2;

the multF of (Polynom-Ring E2) || the carrier of (Polynom-Ring E1) = the multF of (Polynom-Ring E1) by FIELD_4:18;

then f = q1 * eg by F, C, Z1, FUNCT_1:49

.= q *' (e * r) by POLYNOM3:def 10

.= e * u by Y, RING_4:10 ;

hence ex E being FieldExtension of F st f splits_in E by FIELD_4:def 5; :: thesis: verum

end;proof

then consider E2 being FieldExtension of E1 such that
reconsider g1 = g as Polynomial of E1 ;

g1 <> 0_. E1 by I;

then D: deg f1 = (deg (rpoly (1,a))) + (deg g1) by C1, HURWITZ:23

.= 1 + (deg g1) by HURWITZ:27 ;

deg f1 = k + 1 by AS2, FIELD_4:20;

hence deg g = k by D; :: thesis: verum

end;g1 <> 0_. E1 by I;

then D: deg f1 = (deg (rpoly (1,a))) + (deg g1) by C1, HURWITZ:23

.= 1 + (deg g1) by HURWITZ:27 ;

deg f1 = k + 1 by AS2, FIELD_4:20;

hence deg g = k by D; :: thesis: verum

E: g splits_in E2 by I, IV;

reconsider E2 = E2 as FieldExtension of F ;

consider e being non zero Element of E2, r being Ppoly of E2 such that

F: g = e * r by E, FIELD_4:def 5;

E1 is Subring of E2 by FIELD_4:def 1;

then the carrier of E1 c= the carrier of E2 by C0SP1:def 3;

then reconsider a1 = a as Element of E2 ;

rpoly (1,a1) is Ppoly of E2 by RING_5:51;

then reconsider u = (rpoly (1,a1)) *' r as Ppoly of E2 by RING_5:52;

reconsider q = rpoly (1,a) as Polynomial of E2 by FIELD_4:8;

reconsider q1 = q as Element of the carrier of (Polynom-Ring E2) by POLYNOM3:def 10;

reconsider eg = e * r as Element of the carrier of (Polynom-Ring E2) by POLYNOM3:def 10;

Y: q = rpoly (1,a1) by FIELD_4:21;

Z1: [h,g] in [: the carrier of (Polynom-Ring E1), the carrier of (Polynom-Ring E1):] by ZFMISC_1:def 2;

the multF of (Polynom-Ring E2) || the carrier of (Polynom-Ring E1) = the multF of (Polynom-Ring E1) by FIELD_4:18;

then f = q1 * eg by F, C, Z1, FUNCT_1:49

.= q *' (e * r) by POLYNOM3:def 10

.= e * u by Y, RING_4:10 ;

hence ex E being FieldExtension of F st f splits_in E by FIELD_4:def 5; :: thesis: verum

consider n being Nat such that

H: deg f = n ;

n + 1 > 0 + 1 by H, RING_4:def 4, XREAL_1:6;

hence ex E being FieldExtension of F st f splits_in E by I, H; :: thesis: verum