set cMGFC = the carrier of ;
let n be non zero Element of NAT ; :: thesis: for f being FinSequence of the carrier of 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 = ) & ( 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 ; :: thesis: ( len f = n & ( for i being non zero Element of NAT st i in dom f holds
( ( not i divides n implies f . i = ) & ( 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 = ) & ( i divides n implies f . i = cyclotomic_poly i ) ) ; :: thesis:
defpred S1[ Nat, set ] means for fi being FinSequence of the carrier of 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 : ( y in n -roots_of_1 & ord y <= \$1 ) } ;
A3: now :: thesis: for i being Nat st i in Seg (len f) holds
ex x being Element of the carrier of st S1[i,x]
let i be Nat; :: thesis: ( i in Seg (len f) implies ex x being Element of the carrier of st S1[i,x] )
assume i in Seg (len f) ; :: thesis: ex x being Element of the carrier of st S1[i,x]
reconsider fi = f | (Seg i) as FinSequence of the carrier of by FINSEQ_1:18;
set x = Product fi;
take x = Product fi; :: thesis: S1[i,x]
thus S1[i,x] ; :: thesis: verum
end;
consider F being FinSequence of 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 defpred S2[ Nat] means ex t being finite Subset of F_Complex st
( t = H1(\$1) & F . \$1 = poly_with_roots ((t,1) -bag) );
A5: now :: thesis: for i being Element of NAT holds H1(i) is finite Subset of F_Complex
let i be Element of NAT ; :: thesis: H1(i) is finite Subset of F_Complex
H1(i) c= n -roots_of_1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(i) or x in n -roots_of_1 )
assume x in H1(i) ; :: thesis:
then ex y being Element of the carrier of st
( x = y & y in n -roots_of_1 & ord y <= i ) ;
hence x in n -roots_of_1 ; :: thesis: verum
end;
hence H1(i) is finite Subset of F_Complex by XBOOLE_1:1; :: thesis: verum
end;
then reconsider sB = H1(n) as finite Subset of F_Complex ;
A6: n -roots_of_1 = { x where x is Element of : 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 ; :: thesis: ( 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] ; :: thesis: S2[i + 1]
reconsider fi = f | (Seg i) as FinSequence of the carrier of by FINSEQ_1:18;
i in Seg (len f) by ;
then A11: F . i = Product fi by A4;
reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of by FINSEQ_1:18;
A12: i + 1 <= len f by ;
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 ;
then A14: i + 1 in Seg (len f) by ;
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 ; :: thesis: ( sB = H1(i + 1) & F . (i + 1) = poly_with_roots ((sB,1) -bag) )
thus sB = H1(i + 1) ; :: thesis: 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 ;
then reconsider fi1d1 = fi1 . (i + 1) as Element of the carrier of by ;
set b = (sb,1) -bag ;
reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;
fi = fi1 | (Seg i) by ;
then fi1 = fi ^ <*fi1d1*> by ;
then A19: Product fi1 = (Product fi) * fi1d1 by GROUP_4:6
.= (poly_with_roots ((sb,1) -bag)) *' fi1d1p by ;
per cases ( not i + 1 divides n or i + 1 divides n ) ;
suppose A20: not i + 1 divides n ; :: thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag)
set eb = EmptyBag the carrier of F_Complex;
now :: thesis: for x being object holds
( ( x in sB implies x in sb ) & ( x in sb implies x in sB ) )
let x be object ; :: thesis: ( ( x in sB implies x in sb ) & ( x in sb implies x in sB ) )
hereby :: thesis: ( x in sb implies x in sB )
assume x in sB ; :: thesis: x in sb
then consider y being Element of such that
A21: x = y and
A22: y in n -roots_of_1 and
A23: ord y <= i + 1 ;
ord y divides n by ;
then ord y < i + 1 by ;
then ord y <= i by NAT_1:13;
hence x in sb by ; :: thesis: verum
end;
assume x in sb ; :: thesis: x in sB
then consider y being Element of the carrier of such that
A24: ( x = y & y in n -roots_of_1 ) and
A25: ord y <= i by A16;
ord y <= i + 1 by ;
hence x in sB by A24; :: thesis: verum
end;
then A26: sB = sb by TARSKI:2;
f . (i + 1) = by A2, A15, A20
.= poly_with_roots () by UPROOTS:60 ;
hence F . (i + 1) = (poly_with_roots ((sb,1) -bag)) *' (poly_with_roots ()) by A4, A14, A18, A19
.= poly_with_roots (((sb,1) -bag) + ()) by UPROOTS:64
.= poly_with_roots ((sB,1) -bag) by ;
:: thesis: verum
end;
suppose A27: i + 1 divides n ; :: thesis: 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 : ord y = i + 1 } and
A29: cyclotomic_poly (i + 1) = poly_with_roots ((scb,1) -bag) by Def5;
now :: thesis: 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 ; :: thesis: ( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies b1 in sB ) )
hereby :: thesis: ( x in sb \/ scb implies b1 in sB )
assume x in sB ; :: thesis: x in sb \/ scb
then consider y being Element of the carrier of such that
A30: x = y and
A31: y in n -roots_of_1 and
A32: ord y <= i + 1 ;
( ord y <= i or ord y = i + 1 ) by ;
then ( y in sb or y in scb ) by ;
hence x in sb \/ scb by ; :: thesis: verum
end;
assume A33: x in sb \/ scb ; :: thesis: b1 in sB
per cases ( x in sb or x in scb ) by ;
suppose x in sb ; :: thesis: b1 in sB
then consider y being Element of the carrier of such that
A34: ( x = y & y in n -roots_of_1 ) and
A35: ord y <= i by A16;
ord y <= i + 1 by ;
hence x in sB by A34; :: thesis: verum
end;
suppose x in scb ; :: thesis: b1 in sB
then consider y being Element of the carrier of such that
A36: x = y and
A37: ord y = i + 1 by A28;
y in n -roots_of_1 by A6, A27, A37;
hence x in sB by ; :: thesis: verum
end;
end;
end;
then A38: sB = sb \/ scb by TARSKI:2;
set cb = (scb,1) -bag ;
A39: sb misses scb
proof
assume sb /\ scb <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being object such that
A40: x in sb /\ scb by XBOOLE_0:def 1;
x in scb by ;
then A41: ex y2 being Element of the carrier of st
( x = y2 & ord y2 = i + 1 ) by A28;
x in sb by ;
then ex y1 being Element of the carrier of st
( x = y1 & y1 in n -roots_of_1 & ord y1 <= i ) by A16;
hence contradiction by A41, NAT_1:13; :: thesis: verum
end;
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 ;
:: thesis: verum
end;
end;
end;
A42: 0 + 1 <= n by NAT_1:13;
A43: S2
proof
reconsider t = H1(1) as finite Subset of F_Complex by A5;
take t ; :: thesis: ( t = H1(1) & F . 1 = poly_with_roots ((t,1) -bag) )
thus t = H1(1) ; :: thesis: F . 1 = poly_with_roots ((t,1) -bag)
reconsider f1 = f | (Seg 1) as FinSequence of the carrier of by FINSEQ_1:18;
A44: ( 1 in dom f & 1 divides n ) by ;
A45: 1 in Seg (len f) by ;
then 1 in dom f by FINSEQ_1:def 3;
then reconsider fd1 = f . 1 as Element of the carrier of by FINSEQ_2:11;
f1 = <*(f . 1)*> by A1, A42, Th1;
then F . 1 = Product <*fd1*> by
.= fd1 by FINSOP_1:11
.= cyclotomic_poly 1 by ;
then consider sB being non empty finite Subset of F_Complex such that
A46: sB = { y where y is Element of the carrier of : ord y = 1 } and
A47: F . 1 = poly_with_roots ((sB,1) -bag) by Def5;
now :: thesis: for x being object holds
( ( x in H1(1) implies x in sB ) & ( x in sB implies x in H1(1) ) )
let x be object ; :: thesis: ( ( x in H1(1) implies x in sB ) & ( x in sB implies x in H1(1) ) )
hereby :: thesis: ( x in sB implies x in H1(1) )
assume x in H1(1) ; :: thesis: x in sB
then consider y being Element of the carrier of such that
A48: x = y and
A49: y in n -roots_of_1 and
A50: ord y <= 1 ;
not y is being_of_order_0 by ;
then ord y <> 0 by GROUP_1:def 11;
then 0 + 1 <= ord y by NAT_1:13;
then ord y = 1 by ;
hence x in sB by ; :: thesis: verum
end;
assume x in sB ; :: thesis: x in H1(1)
then consider y being Element of the carrier of such that
A51: x = y and
A52: ord y = 1 by A46;
ord y divides n by ;
then y in n -roots_of_1 by A6;
hence x in H1(1) by ; :: thesis: verum
end;
hence F . 1 = poly_with_roots ((t,1) -bag) by ; :: thesis: 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 ;
set b = ((),1) -bag ;
A54: f = f | (Seg (len f)) by FINSEQ_3:49;
now :: thesis: for x being object holds
( ( x in n -roots_of_1 implies x in sB ) & ( x in sB implies x in n -roots_of_1 ) )
let x be object ; :: thesis: ( ( x in n -roots_of_1 implies x in sB ) & ( x in sB implies x in n -roots_of_1 ) )
hereby :: thesis: ( x in sB implies x in n -roots_of_1 )
assume A55: x in n -roots_of_1 ; :: thesis: x in sB
then consider y being Element of such that
A56: x = y and
A57: ord y divides n by A6;
ord y <= n by ;
hence x in sB by ; :: thesis: verum
end;
assume x in sB ; :: thesis:
then ex y being Element of st
( y = x & y in n -roots_of_1 & ord y <= n ) ;
hence x in n -roots_of_1 ; :: thesis: verum
end;
then A58: n -roots_of_1 = sB by TARSKI:2;
thus unital_poly (F_Complex,n) = poly_with_roots (((),1) -bag) by Th46
.= Product f by ; :: thesis: verum