let L be comRing; :: thesis: 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; :: thesis: 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); :: thesis: ( 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)%>
; :: thesis: poly_with_roots (s,1 -bag ) = Product f
set cs = canFS s;
A3:
len (canFS s) = card s
by Def1;
A4:
0 + 1 <= len f
by A1, NAT_1:13;
A5:
(canFS s) | (Seg (len f)) is FinSequence
by FINSEQ_1:23;
f | (Seg (len f)) is FinSequence
by FINSEQ_1:23;
then A6:
f | (Seg (len f)) = f
by FINSEQ_2:23;
A7:
rng (canFS s) = s
by FUNCT_2:def 3;
A8:
dom f = dom (canFS s)
by A1, A3, FINSEQ_3:31;
defpred S1[ Element of 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 );
A9:
S1[1]
proof
reconsider cs1a =
(canFS s) | (Seg 1) as
FinSequence of
s by FINSEQ_1:23;
reconsider g =
f | (Seg 1) as
FinSequence of the
carrier of
(Polynom-Ring L) by FINSEQ_1:23;
consider s1 being
Element of
s such that A10:
cs1a = <*s1*>
by A1, A3, A4, QC_LANG4:7;
A11:
1
in Seg 1
by FINSEQ_1:3;
1
in dom (canFS s)
by A1, A3, A4, FINSEQ_3:27;
then reconsider cs1 =
(canFS s) . 1 as
Element of
s by FINSEQ_2:13;
A12:
cs1a . 1
= cs1
by A11, FUNCT_1:72;
cs1 in the
carrier of
L
;
then reconsider cs1 =
(canFS s) . 1 as
Element of the
carrier of
L ;
A13:
cs1a . 1
= s1
by A10, FINSEQ_1:57;
reconsider t =
{cs1} as
finite Subset of the
carrier of
L ;
consider p1 being
Element of the
carrier of
(Polynom-Ring L) such that A14:
g = <*p1*>
by A4, QC_LANG4:7;
A15:
1
in dom f
by A4, FINSEQ_3:27;
then reconsider f1 =
f . 1 as
Element of the
carrier of
(Polynom-Ring L) by FINSEQ_2:13;
A16:
g . 1
= f1
by A11, FUNCT_1:72;
A17:
g . 1
= p1
by A14, FINSEQ_1:57;
take
t
;
:: thesis: 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
;
:: thesis: ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & poly_with_roots (t,1 -bag ) = Product g )
thus
(
t = rng ((canFS s) | (Seg 1)) &
g = f | (Seg 1) )
by A10, A12, A13, FINSEQ_1:56;
:: thesis: poly_with_roots (t,1 -bag ) = Product g
A18:
Product g = p1
by A14, FINSOP_1:12;
f1 = <%(- cs1),(1. L)%>
by A2, A15;
hence
poly_with_roots (t,1 -bag ) = Product g
by A16, A17, A18, Th63;
:: thesis: verum
end;
A19:
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 ;
:: thesis: ( 1 <= j & j < len f & S1[j] implies S1[j + 1] )
assume that A20:
1
<= j
and A21:
j < len f
;
:: thesis: ( not S1[j] or S1[j + 1] )
reconsider csja =
(canFS s) | (Seg j) as
FinSequence of
s by FINSEQ_1:23;
reconsider csja1 =
(canFS s) | (Seg (j + 1)) as
FinSequence of
s by FINSEQ_1:23;
given t being
finite Subset of the
carrier of
L,
g being
FinSequence of the
carrier of
(Polynom-Ring L) such that A22:
t = rng ((canFS s) | (Seg j))
and A23:
g = f | (Seg j)
and A24:
poly_with_roots (t,1 -bag ) = Product g
;
:: thesis: S1[j + 1]
reconsider g1 =
f | (Seg (j + 1)) as
FinSequence of the
carrier of
(Polynom-Ring L) by FINSEQ_1:23;
set t1 =
rng csja1;
A25:
( 1
<= j + 1 &
j + 1
<= len f )
by A20, A21, NAT_1:13;
then A26:
j + 1
in dom (canFS s)
by A1, A3, FINSEQ_3:27;
then
(canFS s) . (j + 1) in s
by FINSEQ_2:13;
then reconsider csj1 =
(canFS s) . (j + 1) as
Element of the
carrier of
L ;
Seg (j + 1) = (Seg j) \/ {(j + 1)}
by FINSEQ_1:11;
then A27:
csja1 = csja \/ ((canFS s) | {(j + 1)})
by RELAT_1:107;
(canFS s) | {(j + 1)} = (j + 1) .--> csj1
by A26, FUNCT_7:6;
then
rng ((canFS s) | {(j + 1)}) = {csj1}
by FUNCOP_1:14;
then A28:
rng csja1 = t \/ {csj1}
by A22, A27, RELAT_1:26;
then reconsider t1 =
rng csja1 as
finite Subset of the
carrier of
L ;
take
t1
;
:: thesis: 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
;
:: thesis: ( 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)) )
;
:: thesis: poly_with_roots (t1,1 -bag ) = Product g1
reconsider pt =
poly_with_roots (t,1 -bag ) as
Polynomial of
L ;
reconsider pj1 =
poly_with_roots ({csj1},1 -bag ) as
Polynomial of
L ;
reconsider epj1 =
<%(- csj1),(1. L)%> as
Element of the
carrier of
(Polynom-Ring L) by POLYNOM3:def 12;
consider l being
Nat such that A29:
len f = (j + 1) + l
by A25, NAT_1:10;
A30:
len g1 = j + 1
by A29, FINSEQ_3:59;
j <= j + 1
by NAT_1:12;
then
Seg j c= Seg (j + 1)
by FINSEQ_1:7;
then A31:
g = g1 | (Seg j)
by A23, RELAT_1:103;
g1 . (j + 1) =
f . (j + 1)
by FINSEQ_1:6, FUNCT_1:72
.=
<%(- csj1),(1. L)%>
by A2, A8, A26
;
then A32:
g1 = g ^ <*<%(- csj1),(1. L)%>*>
by A30, A31, FINSEQ_3:61;
A33:
pj1 = epj1
by Th63;
t misses {csj1}
proof
assume
not
t misses {csj1}
;
:: thesis: contradiction
then
t /\ {csj1} <> {}
by XBOOLE_0:def 7;
then consider x being
set such that A34:
x in t /\ {csj1}
by XBOOLE_0:def 1;
A35:
(
x in t &
x in {csj1} )
by A34, XBOOLE_0:def 4;
then A36:
x = csj1
by TARSKI:def 1;
consider i being
set such that A37:
i in dom ((canFS s) | (Seg j))
and A38:
x = ((canFS s) | (Seg j)) . i
by A22, A35, FUNCT_1:def 5;
A39:
i in Seg j
by A37, RELAT_1:86;
reconsider i =
i as
Element of
NAT by A37;
A40:
( 1
<= i &
i <= j )
by A39, FINSEQ_1:3;
then A41:
i < j + 1
by NAT_1:13;
x = (canFS s) . i
by A37, A38, FUNCT_1:70;
hence
contradiction
by A1, A3, A7, A25, A36, A40, A41, GRAPH_5:10;
:: thesis: verum
end;
then
t1,1
-bag = (t,1 -bag ) + ({csj1},1 -bag )
by A28, Th12;
hence poly_with_roots (t1,1 -bag ) =
pt *' pj1
by Th66
.=
(Product g) * epj1
by A24, A33, POLYNOM3:def 12
.=
Product g1
by A32, GROUP_4:9
;
:: thesis: verum
end;
for i being Element of NAT st 1 <= i & i <= len f holds
S1[i]
from POLYNOM2:sch 4(A9, A19);
then consider t being finite Subset of the carrier of L, g being FinSequence of the carrier of (Polynom-Ring L) such that
A42:
t = rng ((canFS s) | (Seg (len f)))
and
A43:
g = f | (Seg (len f))
and
A44:
poly_with_roots (t,1 -bag ) = Product g
by A4;
thus
poly_with_roots (s,1 -bag ) = Product f
by A1, A3, A5, A6, A7, A42, A43, A44, FINSEQ_2:23; :: thesis: verum