let F be strong_polynomial_disjoint Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F)

for E being Field st E = embField (emb p) holds

E is strong_polynomial_disjoint

let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for E being Field st E = embField (emb p) holds

E is strong_polynomial_disjoint

let E be Field; :: thesis: ( E = embField (emb p) implies E is strong_polynomial_disjoint )

assume AS: E = embField (emb p) ; :: thesis: E is strong_polynomial_disjoint

set FX = Polynom-Ring F;

set EX = Polynom-Ring E;

set f = emb p;

set Kr = KroneckerField (F,p);

X: ( [#] F = the carrier of F & [#] (KroneckerField (F,p)) = the carrier of (KroneckerField (F,p)) ) ;

H: the carrier of E = carr (emb p) by AS, FIELD_2:def 7

.= ( the carrier of (KroneckerField (F,p)) \ (rng (emb p))) \/ the carrier of F by X, FIELD_2:def 2 ;

for E being Field st E = embField (emb p) holds

E is strong_polynomial_disjoint

let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for E being Field st E = embField (emb p) holds

E is strong_polynomial_disjoint

let E be Field; :: thesis: ( E = embField (emb p) implies E is strong_polynomial_disjoint )

assume AS: E = embField (emb p) ; :: thesis: E is strong_polynomial_disjoint

set FX = Polynom-Ring F;

set EX = Polynom-Ring E;

set f = emb p;

set Kr = KroneckerField (F,p);

X: ( [#] F = the carrier of F & [#] (KroneckerField (F,p)) = the carrier of (KroneckerField (F,p)) ) ;

H: the carrier of E = carr (emb p) by AS, FIELD_2:def 7

.= ( the carrier of (KroneckerField (F,p)) \ (rng (emb p))) \/ the carrier of F by X, FIELD_2:def 2 ;

now :: thesis: E is strong_polynomial_disjoint

hence
E is strong_polynomial_disjoint
; :: thesis: verumassume
not E is strong_polynomial_disjoint
; :: thesis: contradiction

then consider o being Element of E, S being Ring, q being Element of the carrier of (Polynom-Ring S) such that

K: o = q ;

set SX = Polynom-Ring S;

end;then consider o being Element of E, S being Ring, q being Element of the carrier of (Polynom-Ring S) such that

K: o = q ;

set SX = Polynom-Ring S;

per cases
( o in the carrier of F or o in the carrier of (KroneckerField (F,p)) \ (rng (emb p)) )
by H, XBOOLE_0:def 3;

end;

suppose
o in the carrier of (KroneckerField (F,p)) \ (rng (emb p))
; :: thesis: contradiction

then reconsider o = o as Element of ((Polynom-Ring F) / ({p} -Ideal)) ;

consider a being Element of (Polynom-Ring F) such that

B: o = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),a) by RING_1:11;

reconsider q = q as Polynomial of S ;

a - a = 0. (Polynom-Ring F) by RLVECT_1:15;

then D0: a in q by K, B, RING_1:5, IDEAL_1:3;

then consider i, z being object such that

D1: ( i in NAT & z in the carrier of S & a = [i,z] ) by ZFMISC_1:def 2;

D2: z = q . i by D0, D1, FUNCT_1:1;

reconsider i = i as Element of NAT by D1;

reconsider a = a as Polynomial of F by POLYNOM3:def 10;

dom a = NAT by FUNCT_2:def 1;

then ( [1,(a . 1)] in a & [2,(a . 2)] in a ) by FUNCT_1:1;

then E: ( [1,(a . 1)] in {{i},{i,(q . i)}} & [2,(a . 2)] in {{i},{i,(q . i)}} ) by D1, D2, TARSKI:def 5;

end;consider a being Element of (Polynom-Ring F) such that

B: o = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),a) by RING_1:11;

reconsider q = q as Polynomial of S ;

a - a = 0. (Polynom-Ring F) by RLVECT_1:15;

then D0: a in q by K, B, RING_1:5, IDEAL_1:3;

then consider i, z being object such that

D1: ( i in NAT & z in the carrier of S & a = [i,z] ) by ZFMISC_1:def 2;

D2: z = q . i by D0, D1, FUNCT_1:1;

reconsider i = i as Element of NAT by D1;

reconsider a = a as Polynomial of F by POLYNOM3:def 10;

dom a = NAT by FUNCT_2:def 1;

then ( [1,(a . 1)] in a & [2,(a . 2)] in a ) by FUNCT_1:1;

then E: ( [1,(a . 1)] in {{i},{i,(q . i)}} & [2,(a . 2)] in {{i},{i,(q . i)}} ) by D1, D2, TARSKI:def 5;

F: now :: thesis: not i = {1}

assume E3:
i = {1}
; :: thesis: contradiction

end;per cases
( [2,(a . 2)] = {i} or [2,(a . 2)] = {i,(q . i)} )
by E, TARSKI:def 2;

end;

suppose
[2,(a . 2)] = {i}
; :: thesis: contradiction

then F1:
{i} = {{2},{2,(a . 2)}}
by TARSKI:def 5;

{2} in {{2},{2,(a . 2)}} by TARSKI:def 2;

then F3: {2} = {1} by E3, F1, TARSKI:def 1;

2 in {2} by TARSKI:def 1;

hence contradiction by F3, TARSKI:def 1; :: thesis: verum

end;{2} in {{2},{2,(a . 2)}} by TARSKI:def 2;

then F3: {2} = {1} by E3, F1, TARSKI:def 1;

2 in {2} by TARSKI:def 1;

hence contradiction by F3, TARSKI:def 1; :: thesis: verum

suppose
[2,(a . 2)] = {i,(q . i)}
; :: thesis: contradiction

then F1:
{i,(q . i)} = {{2},{2,(a . 2)}}
by TARSKI:def 5;

i in {i,(q . i)} by TARSKI:def 2;

end;i in {i,(q . i)} by TARSKI:def 2;

per cases
( [1,(a . 1)] = {i} or [1,(a . 1)] = {i,(q . i)} )
by E, TARSKI:def 2;

end;

suppose
[1,(a . 1)] = {i}
; :: thesis: contradiction

then E1:
{i} = {{1},{1,(a . 1)}}
by TARSKI:def 5;

( {1} in {{1},{1,(a . 1)}} & {1,(a . 1)} in {{1},{1,(a . 1)}} ) by TARSKI:def 2;

hence contradiction by F, E1, TARSKI:def 1; :: thesis: verum

end;( {1} in {{1},{1,(a . 1)}} & {1,(a . 1)} in {{1},{1,(a . 1)}} ) by TARSKI:def 2;

hence contradiction by F, E1, TARSKI:def 1; :: thesis: verum

suppose
[1,(a . 1)] = {i,(q . i)}
; :: thesis: contradiction

then E1:
{i,(q . i)} = {{1},{1,(a . 1)}}
by TARSKI:def 5;

i in {i,(q . i)} by TARSKI:def 2;

then F0: i = {1,(a . 1)} by F, E1, TARSKI:def 2;

end;i in {i,(q . i)} by TARSKI:def 2;

then F0: i = {1,(a . 1)} by F, E1, TARSKI:def 2;

per cases
( 1 = a . 1 or 1 <> a . 1 )
;

end;

suppose E3:
1 = a . 1
; :: thesis: contradiction

end;

per cases
( [2,(a . 2)] = {i} or [2,(a . 2)] = {i,(q . i)} )
by E, TARSKI:def 2;

end;

suppose
[2,(a . 2)] = {i}
; :: thesis: contradiction

then F1:
{i} = {{2},{2,(a . 2)}}
by TARSKI:def 5;

{2} in {{2},{2,(a . 2)}} by TARSKI:def 2;

then F3: {2} = i by F1, TARSKI:def 1

.= {1} by E3, F0, ENUMSET1:29 ;

2 in {2} by TARSKI:def 1;

hence contradiction by F3, TARSKI:def 1; :: thesis: verum

end;{2} in {{2},{2,(a . 2)}} by TARSKI:def 2;

then F3: {2} = i by F1, TARSKI:def 1

.= {1} by E3, F0, ENUMSET1:29 ;

2 in {2} by TARSKI:def 1;

hence contradiction by F3, TARSKI:def 1; :: thesis: verum

suppose
[2,(a . 2)] = {i,(q . i)}
; :: thesis: contradiction

then F1:
{i,(q . i)} = {{2},{2,(a . 2)}}
by TARSKI:def 5;

i in {i,(q . i)} by TARSKI:def 2;

end;i in {i,(q . i)} by TARSKI:def 2;

per cases then
( i = {2} or i = {2,(a . 2)} )
by F1, TARSKI:def 2;

end;

suppose
i = {2}
; :: thesis: contradiction

then F3:
{2} = {1}
by E3, F0, ENUMSET1:29;

2 in {2} by TARSKI:def 1;

hence contradiction by F3, TARSKI:def 1; :: thesis: verum

end;2 in {2} by TARSKI:def 1;

hence contradiction by F3, TARSKI:def 1; :: thesis: verum

suppose
i = {2,(a . 2)}
; :: thesis: contradiction

then F3:
{1} = {2,(a . 2)}
by E3, F0, ENUMSET1:29;

2 in {2,(a . 2)} by TARSKI:def 2;

hence contradiction by F3, TARSKI:def 1; :: thesis: verum

end;2 in {2,(a . 2)} by TARSKI:def 2;

hence contradiction by F3, TARSKI:def 1; :: thesis: verum

suppose G:
1 <> a . 1
; :: thesis: contradiction

G1:
a . 1 = 0
by F0, G, FIELD_3:2;

end;per cases
( [2,(a . 2)] = {i} or [2,(a . 2)] = {i,(q . i)} )
by E, TARSKI:def 2;

end;

suppose
[2,(a . 2)] = {i}
; :: thesis: contradiction

then F1:
{{1,(a . 1)}} = {{2},{2,(a . 2)}}
by F0, TARSKI:def 5;

( {2} in {{2},{2,(a . 2)}} & {2,(a . 2)} in {{2},{2,(a . 2)}} ) by TARSKI:def 2;

hence contradiction by G1, F1, CARD_1:50; :: thesis: verum

end;( {2} in {{2},{2,(a . 2)}} & {2,(a . 2)} in {{2},{2,(a . 2)}} ) by TARSKI:def 2;

hence contradiction by G1, F1, CARD_1:50; :: thesis: verum

suppose
[2,(a . 2)] = {i,(q . i)}
; :: thesis: contradiction

then F1:
{2,(q . i)} = {{2},{2,(a . 2)}}
by CARD_1:50, F0, G1, TARSKI:def 5;

2 in {2,(q . i)} by TARSKI:def 2;

end;2 in {2,(q . i)} by TARSKI:def 2;