set cMGFC = the carrier of (MultGroup F_Complex);
let n be non zero Element of NAT ; for f being FinSequence of the carrier of (Polynom-Ring F_Complex) st len f = n & ( for i being non zero Element of NAT st i in dom f holds
( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) ) holds
unital_poly (F_Complex,n) = Product f
let f be FinSequence of the carrier of (Polynom-Ring F_Complex); ( len f = n & ( for i being non zero Element of NAT st i in dom f holds
( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) ) implies unital_poly (F_Complex,n) = Product f )
assume that
A1:
len f = n
and
A2:
for i being non zero Element of NAT st i in dom f holds
( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) )
; unital_poly (F_Complex,n) = Product f
defpred S1[ Nat, set ] means for fi being FinSequence of the carrier of (Polynom-Ring F_Complex) st fi = f | (Seg $1) holds
$2 = Product fi;
set nr1 = n -roots_of_1 ;
deffunc H1( Nat) -> set = { y where y is Element of (MultGroup F_Complex) : ( y in n -roots_of_1 & ord y <= $1 ) } ;
consider F being FinSequence of (Polynom-Ring F_Complex) such that
dom F = Seg (len f)
and
A4:
for i being Nat st i in Seg (len f) holds
S1[i,F . i]
from FINSEQ_1:sch 5(A3);
defpred S2[ Nat] means ex t being finite Subset of F_Complex st
( t = H1($1) & F . $1 = poly_with_roots ((t,1) -bag) );
then reconsider sB = H1(n) as finite Subset of F_Complex ;
A6:
n -roots_of_1 = { x where x is Element of (MultGroup F_Complex) : ord x divides n }
by Th35;
A7:
for i being Element of NAT st 1 <= i & i < len f & S2[i] holds
S2[i + 1]
proof
let i be
Element of
NAT ;
( 1 <= i & i < len f & S2[i] implies S2[i + 1] )
assume that A8:
1
<= i
and A9:
i < len f
and A10:
S2[
i]
;
S2[i + 1]
reconsider fi =
f | (Seg i) as
FinSequence of the
carrier of
(Polynom-Ring F_Complex) by FINSEQ_1:18;
i in Seg (len f)
by A8, A9, FINSEQ_1:1;
then A11:
F . i = Product fi
by A4;
reconsider fi1 =
f | (Seg (i + 1)) as
FinSequence of the
carrier of
(Polynom-Ring F_Complex) by FINSEQ_1:18;
A12:
i + 1
<= len f
by A9, NAT_1:13;
then
i + 1
= min (
(i + 1),
(len f))
by XXREAL_0:def 9;
then A13:
len fi1 = i + 1
by FINSEQ_2:21;
1
<= i + 1
by A8, NAT_1:13;
then A14:
i + 1
in Seg (len f)
by A12, FINSEQ_1:1;
then A15:
i + 1
in dom f
by FINSEQ_1:def 3;
i + 1
in NAT
by ORDINAL1:def 12;
then reconsider sB =
H1(
i + 1) as
finite Subset of
F_Complex by A5;
take
sB
;
( sB = H1(i + 1) & F . (i + 1) = poly_with_roots ((sB,1) -bag) )
thus
sB = H1(
i + 1)
;
F . (i + 1) = poly_with_roots ((sB,1) -bag)
set B = (
sB,1)
-bag ;
consider sb being
finite Subset of
F_Complex such that A16:
sb = H1(
i)
and A17:
F . i = poly_with_roots ((sb,1) -bag)
by A10;
A18:
(f | (Seg (i + 1))) . (i + 1) = f . (i + 1)
by FINSEQ_1:4, FUNCT_1:49;
then reconsider fi1d1 =
fi1 . (i + 1) as
Element of the
carrier of
(Polynom-Ring F_Complex) by A15, FINSEQ_2:11;
set b = (
sb,1)
-bag ;
reconsider fi1d1p =
fi1d1 as
Polynomial of
F_Complex by POLYNOM3:def 10;
fi = fi1 | (Seg i)
by Lm2, NAT_1:12;
then
fi1 = fi ^ <*fi1d1*>
by A13, FINSEQ_3:55;
then A19:
Product fi1 =
(Product fi) * fi1d1
by GROUP_4:6
.=
(poly_with_roots ((sb,1) -bag)) *' fi1d1p
by A17, A11, POLYNOM3:def 10
;
per cases
( not i + 1 divides n or i + 1 divides n )
;
suppose A27:
i + 1
divides n
;
F . (i + 1) = poly_with_roots ((sB,1) -bag)consider scb being non
empty finite Subset of
F_Complex such that A28:
scb = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = i + 1 }
and A29:
cyclotomic_poly (i + 1) = poly_with_roots ((scb,1) -bag)
by Def5;
now for x being object holds
( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies x in sB ) )let x be
object ;
( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies b1 in sB ) )hereby ( x in sb \/ scb implies b1 in sB )
end; assume A33:
x in sb \/ scb
;
b1 in sB end; then A38:
sB = sb \/ scb
by TARSKI:2;
set cb = (
scb,1)
-bag ;
A39:
sb misses scb
f . (i + 1) = poly_with_roots ((scb,1) -bag)
by A2, A15, A27, A29;
hence F . (i + 1) =
(poly_with_roots ((sb,1) -bag)) *' (poly_with_roots ((scb,1) -bag))
by A4, A14, A18, A19
.=
poly_with_roots (((sb,1) -bag) + ((scb,1) -bag))
by UPROOTS:64
.=
poly_with_roots ((sB,1) -bag)
by A38, A39, UPROOTS:10
;
verum end;
end;
A42:
0 + 1 <= n
by NAT_1:13;
A43:
S2[1]
proof
reconsider t =
H1(1) as
finite Subset of
F_Complex by A5;
take
t
;
( t = H1(1) & F . 1 = poly_with_roots ((t,1) -bag) )
thus
t = H1(1)
;
F . 1 = poly_with_roots ((t,1) -bag)
reconsider f1 =
f | (Seg 1) as
FinSequence of the
carrier of
(Polynom-Ring F_Complex) by FINSEQ_1:18;
A44:
( 1
in dom f & 1
divides n )
by A1, A42, FINSEQ_3:25, NAT_D:6;
A45:
1
in Seg (len f)
by A1, A42, FINSEQ_1:1;
then
1
in dom f
by FINSEQ_1:def 3;
then reconsider fd1 =
f . 1 as
Element of the
carrier of
(Polynom-Ring F_Complex) by FINSEQ_2:11;
f1 = <*(f . 1)*>
by A1, A42, Th1;
then F . 1 =
Product <*fd1*>
by A4, A45
.=
fd1
by FINSOP_1:11
.=
cyclotomic_poly 1
by A2, A44
;
then consider sB being non
empty finite Subset of
F_Complex such that A46:
sB = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = 1 }
and A47:
F . 1
= poly_with_roots ((sB,1) -bag)
by Def5;
now for x being object holds
( ( x in H1(1) implies x in sB ) & ( x in sB implies x in H1(1) ) )end;
hence
F . 1
= poly_with_roots ((t,1) -bag)
by A47, TARSKI:2;
verum
end;
for i being Element of NAT st 1 <= i & i <= len f holds
S2[i]
from INT_1:sch 7(A43, A7);
then A53:
ex t being finite Subset of F_Complex st
( t = H1( len f) & F . (len f) = poly_with_roots ((t,1) -bag) )
by A1, A42;
set b = ((n -roots_of_1),1) -bag ;
A54:
f = f | (Seg (len f))
by FINSEQ_3:49;
then A58:
n -roots_of_1 = sB
by TARSKI:2;
thus unital_poly (F_Complex,n) =
poly_with_roots (((n -roots_of_1),1) -bag)
by Th46
.=
Product f
by A1, A4, A58, A53, A54, FINSEQ_1:3
; verum