let F be polynomial_disjoint Field; for p being irreducible Element of the carrier of (Polynom-Ring F) holds
( embField (canHomP p) is polynomial_disjoint iff p is linear )
let p be irreducible Element of the carrier of (Polynom-Ring F); ( embField (canHomP p) is polynomial_disjoint iff p is linear )
set FP = Polynom-Ring p;
set K = embField (canHomP p);
set X = <%(0. F),(1. F)%>;
X:
( [#] F = the carrier of F & [#] (Polynom-Ring p) = the carrier of (Polynom-Ring p) )
;
A:
now ( deg p > 1 implies not embField (canHomP p) is polynomial_disjoint )assume AS:
deg p > 1
;
not embField (canHomP p) is polynomial_disjoint H:
the
carrier of
(Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p }
by RING_4:def 8;
len <%(0. F),(1. F)%> = 2
by POLYNOM5:40;
then D:
deg <%(0. F),(1. F)%> = 2
- 1
by HURWITZ:def 2;
then C:
<%(0. F),(1. F)%> in the
carrier of
(Polynom-Ring p)
by H, AS;
then
<%(0. F),(1. F)%> in the
carrier of
(Polynom-Ring p) \ (rng (canHomP p))
by C, XBOOLE_0:def 5;
then
<%(0. F),(1. F)%> in ( the carrier of (Polynom-Ring p) \ (rng (canHomP p))) \/ the
carrier of
F
by XBOOLE_0:def 3;
then
<%(0. F),(1. F)%> in carr (canHomP p)
by X, FIELD_2:def 2;
then A:
<%(0. F),(1. F)%> in the
carrier of
(embField (canHomP p))
by FIELD_2:def 7;
then
<%(0. F),(1. F)%> = <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%>
;
then
<%(0. F),(1. F)%> in the
carrier of
(Polynom-Ring (embField (canHomP p)))
by POLYNOM3:def 10;
then
<%(0. F),(1. F)%> in ([#] (embField (canHomP p))) /\ ([#] (Polynom-Ring (embField (canHomP p))))
by A, XBOOLE_0:def 4;
hence
not
embField (canHomP p) is
polynomial_disjoint
by FIELD_3:def 3;
verum end;
H:
0. (embField (canHomP p)) = 0. F
by FIELD_2:def 7;
hence
( embField (canHomP p) is polynomial_disjoint iff p is linear )
by B; verum