let L be comRing; for s being non empty finite Subset of L
for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = <%(- c),(1. L)%> ) holds
poly_with_roots ((s,1) -bag) = Product f
set cL = the carrier of L;
set cPRL = the carrier of (Polynom-Ring L);
let s be non empty finite Subset of the carrier of L; for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = <%(- c),(1. L)%> ) holds
poly_with_roots ((s,1) -bag) = Product f
let f be FinSequence of the carrier of (Polynom-Ring L); ( len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = (canFS s) . i holds
f . i = <%(- c),(1. L)%> ) implies poly_with_roots ((s,1) -bag) = Product f )
assume that
A1:
len f = card s
and
A2:
for i being Element of NAT
for c being Element of the carrier of L st i in dom f & c = (canFS s) . i holds
f . i = <%(- c),(1. L)%>
; poly_with_roots ((s,1) -bag) = Product f
set cs = canFS s;
A3:
rng (canFS s) = s
by FUNCT_2:def 3;
defpred S1[ Nat] means ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of (Polynom-Ring L) st
( t = rng ((canFS s) | (Seg $1)) & g = f | (Seg $1) & poly_with_roots ((t,1) -bag) = Product g );
A4:
len (canFS s) = card s
by FINSEQ_1:93;
then A5:
dom f = dom (canFS s)
by A1, FINSEQ_3:29;
A6:
for j being Element of NAT st 1 <= j & j < len f & S1[j] holds
S1[j + 1]
proof
let j be
Element of
NAT ;
( 1 <= j & j < len f & S1[j] implies S1[j + 1] )
assume that A7:
1
<= j
and A8:
j < len f
;
( not S1[j] or S1[j + 1] )
reconsider g1 =
f | (Seg (j + 1)) as
FinSequence of the
carrier of
(Polynom-Ring L) by FINSEQ_1:18;
A9:
j + 1
<= len f
by A8, NAT_1:13;
then
ex
l being
Nat st
len f = (j + 1) + l
by NAT_1:10;
then A10:
len g1 = j + 1
by FINSEQ_3:53;
1
<= j + 1
by A7, NAT_1:13;
then A11:
j + 1
in dom (canFS s)
by A1, A4, A9, FINSEQ_3:25;
then
(canFS s) . (j + 1) in s
by FINSEQ_2:11;
then reconsider csj1 =
(canFS s) . (j + 1) as
Element of the
carrier of
L ;
A12:
g1 . (j + 1) =
f . (j + 1)
by FINSEQ_1:4, FUNCT_1:49
.=
<%(- csj1),(1. L)%>
by A2, A5, A11
;
reconsider csja1 =
(canFS s) | (Seg (j + 1)) as
FinSequence of
s by FINSEQ_1:18;
reconsider csja =
(canFS s) | (Seg j) as
FinSequence of
s by FINSEQ_1:18;
given t being
finite Subset of the
carrier of
L,
g being
FinSequence of the
carrier of
(Polynom-Ring L) such that A13:
t = rng ((canFS s) | (Seg j))
and A14:
g = f | (Seg j)
and A15:
poly_with_roots ((t,1) -bag) = Product g
;
S1[j + 1]
j <= j + 1
by NAT_1:12;
then
Seg j c= Seg (j + 1)
by FINSEQ_1:5;
then
g = g1 | (Seg j)
by A14, RELAT_1:74;
then A16:
g1 = g ^ <*<%(- csj1),(1. L)%>*>
by A10, A12, FINSEQ_3:55;
reconsider pt =
poly_with_roots ((t,1) -bag) as
Polynomial of
L ;
set t1 =
rng csja1;
Seg (j + 1) = (Seg j) \/ {(j + 1)}
by FINSEQ_1:9;
then A17:
csja1 = csja \/ ((canFS s) | {(j + 1)})
by RELAT_1:78;
(canFS s) | {(j + 1)} = (j + 1) .--> csj1
by A11, FUNCT_7:6;
then
rng ((canFS s) | {(j + 1)}) = {csj1}
by FUNCOP_1:8;
then A18:
rng csja1 = t \/ {csj1}
by A13, A17, RELAT_1:12;
reconsider epj1 =
<%(- csj1),(1. L)%> as
Element of the
carrier of
(Polynom-Ring L) by POLYNOM3:def 10;
reconsider pj1 =
poly_with_roots (({csj1},1) -bag) as
Polynomial of
L ;
A19:
pj1 = epj1
by Th58;
reconsider t1 =
rng csja1 as
finite Subset of the
carrier of
L by A18;
take
t1
;
ex g being FinSequence of the carrier of (Polynom-Ring L) st
( t1 = rng ((canFS s) | (Seg (j + 1))) & g = f | (Seg (j + 1)) & poly_with_roots ((t1,1) -bag) = Product g )
take
g1
;
( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) & poly_with_roots ((t1,1) -bag) = Product g1 )
thus
(
t1 = rng ((canFS s) | (Seg (j + 1))) &
g1 = f | (Seg (j + 1)) )
;
poly_with_roots ((t1,1) -bag) = Product g1
t misses {csj1}
proof
assume
not
t misses {csj1}
;
contradiction
then
t /\ {csj1} <> {}
by XBOOLE_0:def 7;
then consider x being
object such that A20:
x in t /\ {csj1}
by XBOOLE_0:def 1;
x in {csj1}
by A20, XBOOLE_0:def 4;
then A21:
x = csj1
by TARSKI:def 1;
x in t
by A20, XBOOLE_0:def 4;
then consider i being
object such that A22:
i in dom ((canFS s) | (Seg j))
and A23:
x = ((canFS s) | (Seg j)) . i
by A13, FUNCT_1:def 3;
A24:
i in Seg j
by A22, RELAT_1:57;
reconsider i =
i as
Element of
NAT by A22;
A25:
1
<= i
by A24, FINSEQ_1:1;
i <= j
by A24, FINSEQ_1:1;
then A26:
i < j + 1
by NAT_1:13;
x = (canFS s) . i
by A22, A23, FUNCT_1:47;
hence
contradiction
by A1, A4, A3, A9, A21, A25, A26, GRAPH_5:7;
verum
end;
then
(
t1,1)
-bag = ((t,1) -bag) + (({csj1},1) -bag)
by A18, Th7;
hence poly_with_roots ((t1,1) -bag) =
pt *' pj1
by Th61
.=
(Product g) * epj1
by A15, A19, POLYNOM3:def 10
.=
Product g1
by A16, GROUP_4:6
;
verum
end;
f | (Seg (len f)) is FinSequence
by FINSEQ_1:18;
then A27:
( (canFS s) | (Seg (len f)) is FinSequence & f | (Seg (len f)) = f )
by FINSEQ_1:18, FINSEQ_2:20;
A28:
0 + 1 <= len f
by A1, NAT_1:13;
A29:
S1[1]
proof
1
in dom (canFS s)
by A1, A4, A28, FINSEQ_3:25;
then reconsider cs1 =
(canFS s) . 1 as
Element of
s by FINSEQ_2:11;
reconsider g =
f | (Seg 1) as
FinSequence of the
carrier of
(Polynom-Ring L) by FINSEQ_1:18;
reconsider cs1a =
(canFS s) | (Seg 1) as
FinSequence of
s by FINSEQ_1:18;
A30:
cs1 in the
carrier of
L
;
A31:
1
in Seg 1
by FINSEQ_1:1;
then A32:
cs1a . 1
= cs1
by FUNCT_1:49;
reconsider cs1 =
(canFS s) . 1 as
Element of the
carrier of
L by A30;
reconsider t =
{cs1} as
finite Subset of the
carrier of
L ;
take
t
;
ex g being FinSequence of the carrier of (Polynom-Ring L) st
( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & poly_with_roots ((t,1) -bag) = Product g )
take
g
;
( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & poly_with_roots ((t,1) -bag) = Product g )
consider s1 being
Element of
s such that A33:
cs1a = <*s1*>
by A1, A4, A28, TREES_9:34;
thus
(
t = rng ((canFS s) | (Seg 1)) &
g = f | (Seg 1) )
by A33, A32, FINSEQ_1:39;
poly_with_roots ((t,1) -bag) = Product g
consider p1 being
Element of the
carrier of
(Polynom-Ring L) such that A34:
g = <*p1*>
by A28, TREES_9:34;
A35:
(
g . 1
= p1 &
Product g = p1 )
by A34, FINSOP_1:11;
A36:
1
in dom f
by A28, FINSEQ_3:25;
then reconsider f1 =
f . 1 as
Element of the
carrier of
(Polynom-Ring L) by FINSEQ_2:11;
A37:
g . 1
= f1
by A31, FUNCT_1:49;
f1 = <%(- cs1),(1. L)%>
by A2, A36;
hence
poly_with_roots ((t,1) -bag) = Product g
by A37, A35, Th58;
verum
end;
for i being Element of NAT st 1 <= i & i <= len f holds
S1[i]
from INT_1:sch 7(A29, A6);
then
ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of (Polynom-Ring L) st
( t = rng ((canFS s) | (Seg (len f))) & g = f | (Seg (len f)) & poly_with_roots ((t,1) -bag) = Product g )
by A28;
hence
poly_with_roots ((s,1) -bag) = Product f
by A1, A4, A27, A3, FINSEQ_2:20; verum