let F be polynomial_disjoint Field; :: thesis: 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); :: thesis: ( 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) ) ;

( embField (canHomP p) is polynomial_disjoint iff p is linear )

let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: ( 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 :: thesis: ( deg p > 1 implies not embField (canHomP p) is polynomial_disjoint )

H:
0. (embField (canHomP p)) = 0. F
by FIELD_2:def 7;assume AS:
deg p > 1
; :: thesis: 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))) \/ 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)%> 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; :: thesis: verum

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

now :: thesis: not <%(0. F),(1. F)%> in rng (canHomP p)

then
<%(0. F),(1. F)%> in the carrier of (Polynom-Ring p) \ (rng (canHomP p))
by C, XBOOLE_0:def 5;assume
<%(0. F),(1. F)%> in rng (canHomP p)
; :: thesis: contradiction

then consider o being object such that

B1: ( o in dom (canHomP p) & (canHomP p) . o = <%(0. F),(1. F)%> ) by FUNCT_1:def 3;

reconsider a = o as Element of F by B1;

<%(0. F),(1. F)%> = a | F by B1, defch;

hence contradiction by D, RATFUNC1:def 2; :: thesis: verum

end;then consider o being object such that

B1: ( o in dom (canHomP p) & (canHomP p) . o = <%(0. F),(1. F)%> ) by FUNCT_1:def 3;

reconsider a = o as Element of F by B1;

<%(0. F),(1. F)%> = a | F by B1, defch;

hence contradiction by D, RATFUNC1:def 2; :: thesis: verum

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;

now :: thesis: for n being Element of NAT holds <%(0. F),(1. F)%> . n = <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%> . n

then
<%(0. F),(1. F)%> = <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%>
;let n be Element of NAT ; :: thesis: <%(0. F),(1. F)%> . b_{1} = <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%> . b_{1}

end;per cases
( n = 0 or n = 1 or n >= 2 )
by NAT_1:23;

end;

suppose B:
n = 0
; :: thesis: <%(0. F),(1. F)%> . b_{1} = <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%> . b_{1}

hence <%(0. F),(1. F)%> . n =
0. F
by POLYNOM5:38

.= 0. (embField (canHomP p)) by FIELD_2:def 7

.= <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%> . n by B, POLYNOM5:38 ;

:: thesis: verum

end;.= 0. (embField (canHomP p)) by FIELD_2:def 7

.= <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%> . n by B, POLYNOM5:38 ;

:: thesis: verum

suppose B:
n = 1
; :: thesis: <%(0. F),(1. F)%> . b_{1} = <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%> . b_{1}

hence <%(0. F),(1. F)%> . n =
1. F
by POLYNOM5:38

.= 1. (embField (canHomP p)) by FIELD_2:def 7

.= <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%> . n by B, POLYNOM5:38 ;

:: thesis: verum

end;.= 1. (embField (canHomP p)) by FIELD_2:def 7

.= <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%> . n by B, POLYNOM5:38 ;

:: thesis: verum

suppose B:
n >= 2
; :: thesis: <%(0. F),(1. F)%> . b_{1} = <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%> . b_{1}

hence <%(0. F),(1. F)%> . n =
0. F
by POLYNOM5:38

.= 0. (embField (canHomP p)) by FIELD_2:def 7

.= <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%> . n by B, POLYNOM5:38 ;

:: thesis: verum

end;.= 0. (embField (canHomP p)) by FIELD_2:def 7

.= <%(0. (embField (canHomP p))),(1. (embField (canHomP p)))%> . n by B, POLYNOM5:38 ;

:: thesis: verum

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

B: now :: thesis: ( p is linear implies embField (canHomP p) is polynomial_disjoint )

assume C:
p is linear
; :: thesis: embField (canHomP p) is polynomial_disjoint

then D: [#] (Polynom-Ring (embField (canHomP p))) = [#] (Polynom-Ring F) by H, lempk, polyd;

[#] (embField (canHomP p)) = [#] F by C, polyd;

then ([#] (embField (canHomP p))) /\ ([#] (Polynom-Ring (embField (canHomP p)))) = {} by D, FIELD_3:def 3;

hence embField (canHomP p) is polynomial_disjoint by FIELD_3:def 3; :: thesis: verum

end;then D: [#] (Polynom-Ring (embField (canHomP p))) = [#] (Polynom-Ring F) by H, lempk, polyd;

[#] (embField (canHomP p)) = [#] F by C, polyd;

then ([#] (embField (canHomP p))) /\ ([#] (Polynom-Ring (embField (canHomP p)))) = {} by D, FIELD_3:def 3;

hence embField (canHomP p) is polynomial_disjoint by FIELD_3:def 3; :: thesis: verum

now :: thesis: ( embField (canHomP p) is polynomial_disjoint implies p is linear )

hence
( embField (canHomP p) is polynomial_disjoint iff p is linear )
by B; :: thesis: verumassume C:
embField (canHomP p) is polynomial_disjoint
; :: thesis: p is linear

deg p >= 0 + 1 by INT_1:7, RING_4:def 4;

hence p is linear by A, C, XXREAL_0:1; :: thesis: verum

end;deg p >= 0 + 1 by INT_1:7, RING_4:def 4;

hence p is linear by A, C, XXREAL_0:1; :: thesis: verum