let F be strong_polynomial_disjoint Field; 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); for E being Field st E = embField (emb p) holds
E is strong_polynomial_disjoint
let E be Field; ( E = embField (emb p) implies E is strong_polynomial_disjoint )
assume AS:
E = embField (emb p)
; 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 E is strong_polynomial_disjoint assume
not
E is
strong_polynomial_disjoint
;
contradictionthen 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;
suppose
o in the
carrier of
(KroneckerField (F,p)) \ (rng (emb p))
;
contradictionthen 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;
F:
now not i = {1}assume E3:
i = {1}
;
contradiction end; per cases
( [1,(a . 1)] = {i} or [1,(a . 1)] = {i,(q . i)} )
by E, TARSKI:def 2;
suppose
[1,(a . 1)] = {i,(q . i)}
;
contradictionthen 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;
per cases
( 1 = a . 1 or 1 <> a . 1 )
;
suppose G:
1
<> a . 1
;
contradictionG1:
a . 1
= 0
by F0, G, FIELD_3:2;
per cases
( [2,(a . 2)] = {i} or [2,(a . 2)] = {i,(q . i)} )
by E, TARSKI:def 2;
suppose
[2,(a . 2)] = {i}
;
contradictionthen 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;
verum end; end; end; end; end; end; end; end; end;
hence
E is strong_polynomial_disjoint
; verum