set cMGFC = the carrier of (MultGroup F_Complex);

let n be non zero Element of NAT ; :: thesis: 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); :: 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 = <%(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 ) ) ; :: thesis: unital_poly (F_Complex,n) = Product f

defpred S_{1}[ 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 H_{1}( Nat) -> set = { y where y is Element of (MultGroup F_Complex) : ( y in n -roots_of_1 & ord y <= $1 ) } ;

dom F = Seg (len f) and

A4: for i being Nat st i in Seg (len f) holds

S_{1}[i,F . i]
from FINSEQ_1:sch 5(A3);

defpred S_{2}[ Nat] means ex t being finite Subset of F_Complex st

( t = H_{1}($1) & F . $1 = poly_with_roots ((t,1) -bag) );

_{1}(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 & S_{2}[i] holds

S_{2}[i + 1]

A43: S_{2}[1]

S_{2}[i]
from INT_1:sch 7(A43, A7);

then A53: ex t being finite Subset of F_Complex st

( t = H_{1}( 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;

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 ; :: thesis: verum

let n be non zero Element of NAT ; :: thesis: 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); :: 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 = <%(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 ) ) ; :: thesis: unital_poly (F_Complex,n) = Product f

defpred S

$2 = Product fi;

set nr1 = n -roots_of_1 ;

deffunc H

A3: now :: thesis: for i being Nat st i in Seg (len f) holds

ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[i,x]

consider F being FinSequence of (Polynom-Ring F_Complex) such that ex x being Element of the carrier of (Polynom-Ring F_Complex) st S

let i be Nat; :: thesis: ( i in Seg (len f) implies ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[i,x] )

assume i in Seg (len f) ; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[i,x]

reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

set x = Product fi;

take x = Product fi; :: thesis: S_{1}[i,x]

thus S_{1}[i,x]
; :: thesis: verum

end;assume i in Seg (len f) ; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S

reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

set x = Product fi;

take x = Product fi; :: thesis: S

thus S

dom F = Seg (len f) and

A4: for i being Nat st i in Seg (len f) holds

S

defpred S

( t = H

A5: now :: thesis: for i being Element of NAT holds H_{1}(i) is finite Subset of F_Complex

then reconsider sB = Hlet i be Element of NAT ; :: thesis: H_{1}(i) is finite Subset of F_Complex

H_{1}(i) c= n -roots_of_1
_{1}(i) is finite Subset of F_Complex
by XBOOLE_1:1; :: thesis: verum

end;H

proof

hence
H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H_{1}(i) or x in n -roots_of_1 )

assume x in H_{1}(i)
; :: thesis: x in n -roots_of_1

then ex y being Element of the carrier of (MultGroup F_Complex) st

( x = y & y in n -roots_of_1 & ord y <= i ) ;

hence x in n -roots_of_1 ; :: thesis: verum

end;assume x in H

then ex y being Element of the carrier of (MultGroup F_Complex) st

( x = y & y in n -roots_of_1 & ord y <= i ) ;

hence x in n -roots_of_1 ; :: thesis: verum

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 & S

S

proof

A42:
0 + 1 <= n
by NAT_1:13;
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f & S_{2}[i] implies S_{2}[i + 1] )

assume that

A8: 1 <= i and

A9: i < len f and

A10: S_{2}[i]
; :: thesis: S_{2}[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 = H_{1}(i + 1) as finite Subset of F_Complex by A5;

take sB ; :: thesis: ( sB = H_{1}(i + 1) & F . (i + 1) = poly_with_roots ((sB,1) -bag) )

thus sB = H_{1}(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 = H_{1}(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 ;

end;assume that

A8: 1 <= i and

A9: i < len f and

A10: S

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 = H

take sB ; :: thesis: ( sB = H

thus sB = H

set B = (sB,1) -bag ;

consider sb being finite Subset of F_Complex such that

A16: sb = H

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 )
;

end;

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;

f . (i + 1) = <%(1_ F_Complex)%> by A2, A15, A20

.= poly_with_roots (EmptyBag the carrier of F_Complex) by UPROOTS:60 ;

hence F . (i + 1) = (poly_with_roots ((sb,1) -bag)) *' (poly_with_roots (EmptyBag the carrier of F_Complex)) by A4, A14, A18, A19

.= poly_with_roots (((sb,1) -bag) + (EmptyBag the carrier of F_Complex)) by UPROOTS:64

.= poly_with_roots ((sB,1) -bag) by A26, PRE_POLY:53 ;

:: thesis: verum

end;now :: thesis: for x being object holds

( ( x in sB implies x in sb ) & ( x in sb implies x in sB ) )

then A26:
sB = sb
by TARSKI:2;( ( 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 ) )

then consider y being Element of the carrier of (MultGroup F_Complex) such that

A24: ( x = y & y in n -roots_of_1 ) and

A25: ord y <= i by A16;

ord y <= i + 1 by A25, NAT_1:12;

hence x in sB by A24; :: thesis: verum

end;hereby :: thesis: ( x in sb implies x in sB )

assume
x in sb
; :: thesis: x in sBassume
x in sB
; :: thesis: x in sb

then consider y being Element of (MultGroup F_Complex) such that

A21: x = y and

A22: y in n -roots_of_1 and

A23: ord y <= i + 1 ;

ord y divides n by A22, Th34;

then ord y < i + 1 by A20, A23, XXREAL_0:1;

then ord y <= i by NAT_1:13;

hence x in sb by A16, A21, A22; :: thesis: verum

end;then consider y being Element of (MultGroup F_Complex) such that

A21: x = y and

A22: y in n -roots_of_1 and

A23: ord y <= i + 1 ;

ord y divides n by A22, Th34;

then ord y < i + 1 by A20, A23, XXREAL_0:1;

then ord y <= i by NAT_1:13;

hence x in sb by A16, A21, A22; :: thesis: verum

then consider y being Element of the carrier of (MultGroup F_Complex) such that

A24: ( x = y & y in n -roots_of_1 ) and

A25: ord y <= i by A16;

ord y <= i + 1 by A25, NAT_1:12;

hence x in sB by A24; :: thesis: verum

f . (i + 1) = <%(1_ F_Complex)%> by A2, A15, A20

.= poly_with_roots (EmptyBag the carrier of F_Complex) by UPROOTS:60 ;

hence F . (i + 1) = (poly_with_roots ((sb,1) -bag)) *' (poly_with_roots (EmptyBag the carrier of F_Complex)) by A4, A14, A18, A19

.= poly_with_roots (((sb,1) -bag) + (EmptyBag the carrier of F_Complex)) by UPROOTS:64

.= poly_with_roots ((sB,1) -bag) by A26, PRE_POLY:53 ;

:: thesis: verum

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 (MultGroup F_Complex) : ord y = i + 1 } and

A29: cyclotomic_poly (i + 1) = poly_with_roots ((scb,1) -bag) by Def5;

set cb = (scb,1) -bag ;

A39: sb misses scb

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 ;

:: thesis: verum

end;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 :: thesis: for x being object holds

( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies x in sB ) )

then A38:
sB = sb \/ scb
by TARSKI:2;( ( 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 b_{1} in sB ) )

_{1} in sB

end;hereby :: thesis: ( x in sb \/ scb implies b_{1} in sB )

assume A33:
x in sb \/ scb
; :: thesis: bassume
x in sB
; :: thesis: x in sb \/ scb

then consider y being Element of the carrier of (MultGroup F_Complex) 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 A32, NAT_1:8;

then ( y in sb or y in scb ) by A16, A28, A31;

hence x in sb \/ scb by A30, XBOOLE_0:def 3; :: thesis: verum

end;then consider y being Element of the carrier of (MultGroup F_Complex) 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 A32, NAT_1:8;

then ( y in sb or y in scb ) by A16, A28, A31;

hence x in sb \/ scb by A30, XBOOLE_0:def 3; :: thesis: verum

per cases
( x in sb or x in scb )
by A33, XBOOLE_0:def 3;

end;

set cb = (scb,1) -bag ;

A39: sb misses scb

proof

f . (i + 1) = poly_with_roots ((scb,1) -bag)
by A2, A15, A27, A29;
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 A40, XBOOLE_0:def 4;

then A41: ex y2 being Element of the carrier of (MultGroup F_Complex) st

( x = y2 & ord y2 = i + 1 ) by A28;

x in sb by A40, XBOOLE_0:def 4;

then ex y1 being Element of the carrier of (MultGroup F_Complex) st

( x = y1 & y1 in n -roots_of_1 & ord y1 <= i ) by A16;

hence contradiction by A41, NAT_1:13; :: thesis: verum

end;then consider x being object such that

A40: x in sb /\ scb by XBOOLE_0:def 1;

x in scb by A40, XBOOLE_0:def 4;

then A41: ex y2 being Element of the carrier of (MultGroup F_Complex) st

( x = y2 & ord y2 = i + 1 ) by A28;

x in sb by A40, XBOOLE_0:def 4;

then ex y1 being Element of the carrier of (MultGroup F_Complex) st

( x = y1 & y1 in n -roots_of_1 & ord y1 <= i ) by A16;

hence contradiction by A41, NAT_1:13; :: thesis: verum

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 ;

:: thesis: verum

A43: S

proof

for i being Element of NAT st 1 <= i & i <= len f holds
reconsider t = H_{1}(1) as finite Subset of F_Complex by A5;

take t ; :: thesis: ( t = H_{1}(1) & F . 1 = poly_with_roots ((t,1) -bag) )

thus t = H_{1}(1)
; :: thesis: 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;

end;take t ; :: thesis: ( t = H

thus t = H

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 :: thesis: for x being object holds

( ( x in H_{1}(1) implies x in sB ) & ( x in sB implies x in H_{1}(1) ) )

hence
F . 1 = poly_with_roots ((t,1) -bag)
by A47, TARSKI:2; :: thesis: verum( ( x in H

let x be object ; :: thesis: ( ( x in H_{1}(1) implies x in sB ) & ( x in sB implies x in H_{1}(1) ) )

_{1}(1)

then consider y being Element of the carrier of (MultGroup F_Complex) such that

A51: x = y and

A52: ord y = 1 by A46;

ord y divides n by A52, NAT_D:6;

then y in n -roots_of_1 by A6;

hence x in H_{1}(1)
by A51, A52; :: thesis: verum

end;hereby :: thesis: ( x in sB implies x in H_{1}(1) )

assume
x in sB
; :: thesis: x in Hassume
x in H_{1}(1)
; :: thesis: x in sB

then consider y being Element of the carrier of (MultGroup F_Complex) 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 A49, Th30;

then ord y <> 0 by GROUP_1:def 11;

then 0 + 1 <= ord y by NAT_1:13;

then ord y = 1 by A50, XXREAL_0:1;

hence x in sB by A46, A48; :: thesis: verum

end;then consider y being Element of the carrier of (MultGroup F_Complex) 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 A49, Th30;

then ord y <> 0 by GROUP_1:def 11;

then 0 + 1 <= ord y by NAT_1:13;

then ord y = 1 by A50, XXREAL_0:1;

hence x in sB by A46, A48; :: thesis: verum

then consider y being Element of the carrier of (MultGroup F_Complex) such that

A51: x = y and

A52: ord y = 1 by A46;

ord y divides n by A52, NAT_D:6;

then y in n -roots_of_1 by A6;

hence x in H

S

then A53: ex t being finite Subset of F_Complex st

( t = H

set b = ((n -roots_of_1),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 ) )

then A58:
n -roots_of_1 = sB
by TARSKI:2;( ( 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 ) )

then ex y being Element of (MultGroup F_Complex) st

( y = x & y in n -roots_of_1 & ord y <= n ) ;

hence x in n -roots_of_1 ; :: thesis: verum

end;hereby :: thesis: ( x in sB implies x in n -roots_of_1 )

assume
x in sB
; :: thesis: x in n -roots_of_1 assume A55:
x in n -roots_of_1
; :: thesis: x in sB

then consider y being Element of (MultGroup F_Complex) such that

A56: x = y and

A57: ord y divides n by A6;

ord y <= n by A57, NAT_D:7;

hence x in sB by A55, A56; :: thesis: verum

end;then consider y being Element of (MultGroup F_Complex) such that

A56: x = y and

A57: ord y divides n by A6;

ord y <= n by A57, NAT_D:7;

hence x in sB by A55, A56; :: thesis: verum

then ex y being Element of (MultGroup F_Complex) st

( y = x & y in n -roots_of_1 & ord y <= n ) ;

hence x in n -roots_of_1 ; :: thesis: verum

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 ; :: thesis: verum