Metamath Proof Explorer

Definition df-cytp

Description: The Nthcyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Assertion df-cytp 
|- CytP = ( n e. NN |-> ( ( mulGrp ` ( Poly1 ` CCfld ) ) gsum ( r e. ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } ) |-> ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccytp 
 |-  CytP
1 vn 
 |-  n
2 cn 
 |-  NN
3 cmgp 
 |-  mulGrp
4 cpl1 
 |-  Poly1
5 ccnfld 
 |-  CCfld
6 5 4 cfv 
 |-  ( Poly1 ` CCfld )
7 6 3 cfv 
 |-  ( mulGrp ` ( Poly1 ` CCfld ) )
8 cgsu 
 |-  gsum
9 vr 
 |-  r
10 cod 
 |-  od
11 5 3 cfv 
 |-  ( mulGrp ` CCfld )
12 cress 
 |-  |`s
13 cc 
 |-  CC
14 cc0 
 |-  0
15 14 csn 
 |-  { 0 }
16 13 15 cdif 
 |-  ( CC \ { 0 } )
17 11 16 12 co 
 |-  ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
18 17 10 cfv 
 |-  ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
19 18 ccnv 
 |-  `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
20 1 cv 
 |-  n
21 20 csn 
 |-  { n }
22 19 21 cima 
 |-  ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } )
23 cv1 
 |-  var1
24 5 23 cfv 
 |-  ( var1 ` CCfld )
25 csg 
 |-  -g
26 6 25 cfv 
 |-  ( -g ` ( Poly1 ` CCfld ) )
27 cascl 
 |-  algSc
28 6 27 cfv 
 |-  ( algSc ` ( Poly1 ` CCfld ) )
29 9 cv 
 |-  r
30 29 28 cfv 
 |-  ( ( algSc ` ( Poly1 ` CCfld ) ) ` r )
31 24 30 26 co 
 |-  ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) )
32 9 22 31 cmpt 
 |-  ( r e. ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } ) |-> ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) )
33 7 32 8 co 
 |-  ( ( mulGrp ` ( Poly1 ` CCfld ) ) gsum ( r e. ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } ) |-> ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) ) )
34 1 2 33 cmpt 
 |-  ( n e. NN |-> ( ( mulGrp ` ( Poly1 ` CCfld ) ) gsum ( r e. ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } ) |-> ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) ) ) )
35 0 34 wceq 
 |-  CytP = ( n e. NN |-> ( ( mulGrp ` ( Poly1 ` CCfld ) ) gsum ( r e. ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } ) |-> ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) ) ) )