let R be Field; for B1, B2 being non zero bag of the carrier of R
for p being Ppoly of R,B1
for q being Ppoly of R,B2 st B1 = B2 holds
p = q
let B1, B2 be non zero bag of the carrier of R; for p being Ppoly of R,B1
for q being Ppoly of R,B2 st B1 = B2 holds
p = q
let p be Ppoly of R,B1; for q being Ppoly of R,B2 st B1 = B2 holds
p = q
let q be Ppoly of R,B2; ( B1 = B2 implies p = q )
assume AS:
B1 = B2
; p = q
defpred S1[ Nat] means for B1, B2 being non zero bag of the carrier of R
for p being Ppoly of R,B1
for q being Ppoly of R,B2 st deg p = $1 & B1 = B2 holds
p = q;
IA:
S1[1]
proof
now for B1, B2 being non zero bag of the carrier of R
for p being Ppoly of R,B1
for q being Ppoly of R,B2 st deg p = 1 & B1 = B2 holds
p = qlet B1,
B2 be non
zero bag of the
carrier of
R;
for p being Ppoly of R,B1
for q being Ppoly of R,B2 st deg p = 1 & B1 = B2 holds
p = qlet p be
Ppoly of
R,
B1;
for q being Ppoly of R,B2 st deg p = 1 & B1 = B2 holds
p = qlet q be
Ppoly of
R,
B2;
( deg p = 1 & B1 = B2 implies p = q )assume A0:
(
deg p = 1 &
B1 = B2 )
;
p = q
B1 = BRoots p
by RING_5:55;
then
card B1 = 1
by A0, RING_5:56;
then consider a being
Element of
R such that A1:
B1 = Bag {a}
by bag2;
thus p =
rpoly (1,
a)
by A1, simpAgcd2
.=
q
by A0, A1, simpAgcd2
;
verum end;
hence
S1[1]
;
verum
end;
IS:
now for k being Nat st k >= 1 & S1[k] holds
S1[k + 1]let k be
Nat;
( k >= 1 & S1[k] implies S1[k + 1] )assume
k >= 1
;
( S1[k] implies S1[k + 1] )assume IV:
S1[
k]
;
S1[k + 1]now for B1, B2 being non zero bag of the carrier of R
for p being Ppoly of R,B1
for q being Ppoly of R,B2 st deg p = k + 1 & B1 = B2 holds
p = qlet B1,
B2 be non
zero bag of the
carrier of
R;
for p being Ppoly of R,B1
for q being Ppoly of R,B2 st deg p = k + 1 & B1 = B2 holds
b5 = b6let p be
Ppoly of
R,
B1;
for q being Ppoly of R,B2 st deg p = k + 1 & B1 = B2 holds
b4 = b5let q be
Ppoly of
R,
B2;
( deg p = k + 1 & B1 = B2 implies b3 = b4 )assume A0:
(
deg p = k + 1 &
B1 = B2 )
;
b3 = b4set a = the
Element of
support B1;
A1:
support B1 <> {}
by RING_5:24;
(
support B1 c= dom B1 &
dom B1 c= the
carrier of
R )
by PRE_POLY:37;
then reconsider a = the
Element of
support B1 as
Element of
R by A1;
B1 . a <> 0
by A1, PRE_POLY:def 7;
then reconsider m =
(B1 . a) - 1 as
Element of
NAT by INT_1:5, NAT_1:14;
consider u being
Polynomial of
R such that A2:
p = ((rpoly (1,a)) `^ (B1 . a)) *' u
by RING_4:1, RING_5:54;
set p1 =
((rpoly (1,a)) `^ m) *' u;
B1 . a = m + 1
;
then
(rpoly (1,a)) `^ (B1 . a) = (rpoly (1,a)) *' ((rpoly (1,a)) `^ m)
by POLYNOM5:19;
then A10:
p = (rpoly (1,a)) *' (((rpoly (1,a)) `^ m) *' u)
by A2, POLYNOM3:33;
consider v being
Polynomial of
R such that A4:
q = ((rpoly (1,a)) `^ (B1 . a)) *' v
by A0, RING_5:54, RING_4:1;
set q1 =
((rpoly (1,a)) `^ m) *' v;
B1 . a = m + 1
;
then
(rpoly (1,a)) `^ (B1 . a) = (rpoly (1,a)) *' ((rpoly (1,a)) `^ m)
by POLYNOM5:19;
then A5:
q = (rpoly (1,a)) *' (((rpoly (1,a)) `^ m) *' v)
by A4, POLYNOM3:33;
reconsider u =
u,
v =
v as non
zero monic Polynomial of
R by A2, A4, ZZ3y;
(
rpoly (1,
a)
<> 0_. R &
((rpoly (1,a)) `^ m) *' u <> 0_. R )
by A10;
then A8:
deg p =
(deg (rpoly (1,a))) + (deg (((rpoly (1,a)) `^ m) *' u))
by A10, HURWITZ:23
.=
1
+ (deg (((rpoly (1,a)) `^ m) *' u))
by HURWITZ:27
;
per cases
( u is constant or not u is constant )
;
suppose I:
not
u is
constant
;
b3 = b4now not v is constant assume
v is
constant
;
contradictionthen I0:
v =
1_. R
by lemconst
.=
(1. R) | R
by RING_4:14
;
1. R <> 0. R
;
then I5:
deg ((1. R) | R) = 0
by RING_4:21;
(
(rpoly (1,a)) `^ (B1 . a) <> 0_. R &
v <> 0_. R )
;
then I1:
deg q = (deg ((rpoly (1,a)) `^ (B1 . a))) + 0
by I0, I5, A4, HURWITZ:23;
(
(rpoly (1,a)) `^ (B1 . a) <> 0_. R &
u <> 0_. R )
;
then I3:
deg p = (deg ((rpoly (1,a)) `^ (B1 . a))) + (deg u)
by A2, HURWITZ:23;
I4:
(
B1 = BRoots p &
B2 = BRoots q )
by RING_5:55;
then deg p =
card B2
by A0, RING_5:56
.=
deg q
by I4, RING_5:56
;
hence
contradiction
by I3, I1, I, RATFUNC1:def 2;
verum end; then reconsider u =
u,
v =
v as non
constant monic Polynomial of
R by I;
reconsider u =
u,
v =
v as
Ppoly of
R by A2, A4, FIELD_8:10;
B1 =
BRoots p
by RING_5:55
.=
(BRoots ((rpoly (1,a)) `^ (B1 . a))) + (BRoots u)
by A2, UPROOTS:56
;
then (BRoots ((rpoly (1,a)) `^ (B1 . a))) + (BRoots u) =
BRoots q
by A0, RING_5:55
.=
(BRoots ((rpoly (1,a)) `^ (B1 . a))) + (BRoots v)
by A4, UPROOTS:56
;
then A7:
BRoots u =
((BRoots ((rpoly (1,a)) `^ (B1 . a))) + (BRoots v)) -' (BRoots ((rpoly (1,a)) `^ (B1 . a)))
by PRE_POLY:48
.=
BRoots v
by PRE_POLY:48
;
per cases
( m is zero or not m is zero )
;
suppose
not
m is
zero
;
b3 = b4then reconsider m =
m as non
zero Element of
NAT ;
(rpoly (1,a)) `^ m is
Ppoly of
R
by lemrpoly;
then A9:
(rpoly (1,a)) `^ m is
Ppoly of
R,
BRoots ((rpoly (1,a)) `^ m)
by RING_5:59;
u is
Ppoly of
R,
BRoots u
by RING_5:59;
then A6:
((rpoly (1,a)) `^ m) *' u is
Ppoly of
R,
(BRoots ((rpoly (1,a)) `^ m)) + (BRoots u)
by A9, RING_5:58;
v is
Ppoly of
R,
BRoots v
by RING_5:59;
then
((rpoly (1,a)) `^ m) *' v is
Ppoly of
R,
(BRoots ((rpoly (1,a)) `^ m)) + (BRoots v)
by A9, RING_5:58;
hence
p = q
by A0, A6, A7, A8, IV, A10, A5;
verum end; end; hence
S1[
k + 1]
;
verum end;
I:
for k being Nat st k >= 1 holds
S1[k]
from NAT_1:sch 8(IA, IS);
reconsider n = deg p as Element of NAT ;
n + 1 > 0 + 1
by RATFUNC1:def 2, XREAL_1:6;
then
n >= 1
by NAT_1:13;
hence
p = q
by I, AS; verum