let F be Field; for p being non constant monic Polynomial of F
for q being non zero Polynomial of F st p *' q is Ppoly of F holds
p is Ppoly of F
let p be non constant monic Polynomial of F; for q being non zero Polynomial of F st p *' q is Ppoly of F holds
p is Ppoly of F
let q be non zero Polynomial of F; ( p *' q is Ppoly of F implies p is Ppoly of F )
assume AS:
p *' q is Ppoly of F
; p is Ppoly of F
( p <> 0_. F & q <> 0_. F )
;
then A1:
deg (p *' q) = (deg p) + (deg q)
by HURWITZ:23;
deg p > 0
by RATFUNC1:def 2;
then A:
deg (p *' q) >= 1 + 0
by A1, NAT_1:14;
defpred S1[ Nat] means for p being non constant monic Polynomial of F
for q being non zero Polynomial of F st deg (p *' q) = $1 & p *' q is Ppoly of F holds
p is Ppoly of F;
now for p being non constant monic Polynomial of F
for q being non zero Polynomial of F st deg (p *' q) = 1 & p *' q is Ppoly of F holds
p is Ppoly of Flet p be non
constant monic Polynomial of
F;
for q being non zero Polynomial of F st deg (p *' q) = 1 & p *' q is Ppoly of F holds
p is Ppoly of Flet q be non
zero Polynomial of
F;
( deg (p *' q) = 1 & p *' q is Ppoly of F implies p is Ppoly of F )assume B:
(
deg (p *' q) = 1 &
p *' q is
Ppoly of
F )
;
p is Ppoly of F
(
p <> 0_. F &
q <> 0_. F )
;
then
deg (p *' q) = (deg p) + (deg q)
by HURWITZ:23;
then B1:
deg p <= deg (p *' q)
by NAT_1:12;
deg p > 0
by RATFUNC1:def 2;
then
deg p >= deg (p *' q)
by B, NAT_1:14;
then consider x,
z being
Element of
F such that A3:
(
x <> 0. F &
p = x * (rpoly (1,z)) )
by B, B1, XXREAL_0:1, HURWITZ:28;
x * (LC (rpoly (1,z))) =
LC (x * (rpoly (1,z)))
by RING_5:5
.=
1. F
by A3, RATFUNC1:def 7
;
then
x * (1. F) = 1. F
by RATFUNC1:def 7;
hence
p is
Ppoly of
F
by A3, RING_5:51;
verum end;
then IA:
S1[1]
;
IS:
now for k being Nat st 1 <= k & S1[k] holds
S1[k + 1]let k be
Nat;
( 1 <= k & S1[k] implies S1[k + 1] )assume BB:
1
<= k
;
( S1[k] implies S1[k + 1] )assume IV:
S1[
k]
;
S1[k + 1]now for p being non constant monic Polynomial of F
for q being non zero Polynomial of F st deg (p *' q) = k + 1 & p *' q is Ppoly of F holds
p is Ppoly of Flet p be non
constant monic Polynomial of
F;
for q being non zero Polynomial of F st deg (p *' q) = k + 1 & p *' q is Ppoly of F holds
b2 is Ppoly of Flet q be non
zero Polynomial of
F;
( deg (p *' q) = k + 1 & p *' q is Ppoly of F implies b1 is Ppoly of F )assume B:
(
deg (p *' q) = k + 1 &
p *' q is
Ppoly of
F )
;
b1 is Ppoly of Fthen
(
LC p = 1. F &
LC (p *' q) = 1. F )
by RATFUNC1:def 7;
then B0:
1. F = (1. F) * (LC q)
by NIVEN:46;
then B0a:
q is
monic
by RATFUNC1:def 7;
consider a being
Element of
F such that B1:
a is_a_root_of p *' q
by B, POLYNOM5:def 8;
0. F =
eval (
(p *' q),
a)
by B1, POLYNOM5:def 7
.=
(eval (p,a)) * (eval (q,a))
by POLYNOM4:24
;
per cases then
( eval (q,a) = 0. F or eval (p,a) = 0. F )
by VECTSP_2:def 1;
suppose
eval (
q,
a)
= 0. F
;
b1 is Ppoly of Fthen consider s being
Polynomial of
F such that B2:
q = (rpoly (1,a)) *' s
by HURWITZ:33, POLYNOM5:def 7;
B3:
not
s is
zero
by B2;
B6:
(
s <> 0_. F &
p <> 0_. F )
by B2;
then deg q =
(deg (rpoly (1,a))) + (deg s)
by B2, HURWITZ:23
.=
1
+ (deg s)
by HURWITZ:27
;
then B4:
deg (p *' s) =
(deg p) + ((deg q) - 1)
by B6, HURWITZ:23
.=
((deg p) + (deg q)) - 1
.=
(deg (p *' q)) - 1
by B6, HURWITZ:23
.=
k
by B
;
1. F =
(LC (rpoly (1,a))) * (LC s)
by B0, B2, NIVEN:46
.=
(1. F) * (LC s)
by RING_5:9
;
then
s is
monic
by RATFUNC1:def 7;
then B5:
( not
p *' s is
constant &
p *' s is
monic )
by BB, B4, RATFUNC1:def 2;
p *' q = (rpoly (1,a)) *' (p *' s)
by B2, POLYNOM3:33;
then
p *' s is
Ppoly of
F
by B, B5, lemppolspl3b;
hence
p is
Ppoly of
F
by B3, B4, IV;
verum end; suppose
eval (
p,
a)
= 0. F
;
b1 is Ppoly of Fthen consider s being
Polynomial of
F such that B2:
p = (rpoly (1,a)) *' s
by POLYNOM5:def 7, HURWITZ:33;
reconsider s =
s as non
zero Polynomial of
F by B2;
B6:
s <> 0_. F
;
then deg p =
(deg (rpoly (1,a))) + (deg s)
by B2, HURWITZ:23
.=
1
+ (deg s)
by HURWITZ:27
;
then B4:
deg (q *' s) =
(deg q) + ((deg p) - 1)
by B6, HURWITZ:23
.=
((deg p) + (deg q)) - 1
.=
(deg (p *' q)) - 1
by B6, HURWITZ:23
.=
k
by B
;
B5:
p *' q = (rpoly (1,a)) *' (s *' q)
by B2, POLYNOM3:33;
B7b:
1. F =
LC p
by RATFUNC1:def 7
.=
(LC (rpoly (1,a))) * (LC s)
by B2, NIVEN:46
.=
(1. F) * (LC s)
by RING_5:9
;
then B7a:
s is
monic
by RATFUNC1:def 7;
reconsider s1 =
s as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
per cases
( deg s >= 1 or deg s < 1 )
;
suppose K:
deg s >= 1
;
b1 is Ppoly of Fthen B8a:
not
s is
constant
by RATFUNC1:def 2;
deg (s *' q) = (deg s) + (deg q)
by B6, HURWITZ:23;
then
not
s *' q is
constant
by K, RATFUNC1:def 2;
then
s *' q is
Ppoly of
F
by B, B5, B7a, B0a, lemppolspl3b;
then B9:
s is
Ppoly of
F
by B4, B7a, B8a, IV;
rpoly (1,
a) is
Ppoly of
F
by RING_5:51;
hence
p is
Ppoly of
F
by B9, B2, RING_5:52;
verum end; end; end; hence
S1[
k + 1]
;
verum end;
for i being Nat st 1 <= i holds
S1[i]
from NAT_1:sch 8(IA, IS);
hence
p is Ppoly of F
by A, AS; verum