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 = ( 𝑛 ∈ ℕ ↦ ( ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) Σg ( 𝑟 ∈ ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } ) ↦ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccytp ⊢ CytP
1 vn ⊢ 𝑛
2 cn ⊢ ℕ
3 cmgp ⊢ mulGrp
4 cpl1 ⊢ Poly1
5 ccnfld ⊢ ℂfld
6 5 4 cfv ⊢ ( Poly1 ‘ ℂfld )
7 6 3 cfv ⊢ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) )
8 cgsu ⊢ Σg
9 vr ⊢ 𝑟
10 cod ⊢ od
11 5 3 cfv ⊢ ( mulGrp ‘ ℂfld )
12 cress ⊢ ↾s
13 cc ⊢ ℂ
14 cc0 ⊢ 0
15 14 csn ⊢ { 0 }
16 13 15 cdif ⊢ ( ℂ ∖ { 0 } )
17 11 16 12 co ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
18 17 10 cfv ⊢ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
19 18 ccnv ⊢ ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
20 1 cv ⊢ 𝑛
21 20 csn ⊢ { 𝑛 }
22 19 21 cima ⊢ ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } )
23 cv1 ⊢ var1
24 5 23 cfv ⊢ ( var1 ‘ ℂfld )
25 csg ⊢ -g
26 6 25 cfv ⊢ ( -g ‘ ( Poly1 ‘ ℂfld ) )
27 cascl ⊢ algSc
28 6 27 cfv ⊢ ( algSc ‘ ( Poly1 ‘ ℂfld ) )
29 9 cv ⊢ 𝑟
30 29 28 cfv ⊢ ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 )
31 24 30 26 co ⊢ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) )
32 9 22 31 cmpt ⊢ ( 𝑟 ∈ ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } ) ↦ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) )
33 7 32 8 co ⊢ ( ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) Σg ( 𝑟 ∈ ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } ) ↦ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) ) )
34 1 2 33 cmpt ⊢ ( 𝑛 ∈ ℕ ↦ ( ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) Σg ( 𝑟 ∈ ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } ) ↦ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) ) ) )
35 0 34 wceq ⊢ CytP = ( 𝑛 ∈ ℕ ↦ ( ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) Σg ( 𝑟 ∈ ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } ) ↦ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) ) ) )