Theorem cytpval

Description: Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cytpval.t	⊢ 𝑇 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
	cytpval.o	⊢ 𝑂 = ( od ‘ 𝑇 )
	cytpval.p	⊢ 𝑃 = ( Poly1 ‘ ℂfld )
	cytpval.x	⊢ 𝑋 = ( var1 ‘ ℂfld )
	cytpval.q	⊢ 𝑄 = ( mulGrp ‘ 𝑃 )
	cytpval.m	⊢ − = ( -g ‘ 𝑃 )
	cytpval.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion	cytpval	⊢ ( 𝑁 ∈ ℕ → ( CytP ‘ 𝑁 ) = ( 𝑄 Σg ( 𝑟 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↦ ( 𝑋 − ( 𝐴 ‘ 𝑟 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cytpval.t	⊢ 𝑇 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
2		cytpval.o	⊢ 𝑂 = ( od ‘ 𝑇 )
3		cytpval.p	⊢ 𝑃 = ( Poly1 ‘ ℂfld )
4		cytpval.x	⊢ 𝑋 = ( var1 ‘ ℂfld )
5		cytpval.q	⊢ 𝑄 = ( mulGrp ‘ 𝑃 )
6		cytpval.m	⊢ − = ( -g ‘ 𝑃 )
7		cytpval.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
8	3	eqcomi	⊢ ( Poly1 ‘ ℂfld ) = 𝑃
9	8	fveq2i	⊢ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) = ( mulGrp ‘ 𝑃 )
10	9 5	eqtr4i	⊢ ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) = 𝑄
11	10	a1i	⊢ ( 𝑛 = 𝑁 → ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) = 𝑄 )
12	1	fveq2i	⊢ ( od ‘ 𝑇 ) = ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
13	2 12	eqtri	⊢ 𝑂 = ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
14	13	cnveqi	⊢ ◡ 𝑂 = ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
15	14	imaeq1i	⊢ ( ◡ 𝑂 “ { 𝑛 } ) = ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } )
16		sneq	⊢ ( 𝑛 = 𝑁 → { 𝑛 } = { 𝑁 } )
17	16	imaeq2d	⊢ ( 𝑛 = 𝑁 → ( ◡ 𝑂 “ { 𝑛 } ) = ( ◡ 𝑂 “ { 𝑁 } ) )
18	15 17	eqtr3id	⊢ ( 𝑛 = 𝑁 → ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } ) = ( ◡ 𝑂 “ { 𝑁 } ) )
19	3	fveq2i	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ ( Poly1 ‘ ℂfld ) )
20	7 19	eqtri	⊢ 𝐴 = ( algSc ‘ ( Poly1 ‘ ℂfld ) )
21	20	fveq1i	⊢ ( 𝐴 ‘ 𝑟 ) = ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 )
22	3	fveq2i	⊢ ( -g ‘ 𝑃 ) = ( -g ‘ ( Poly1 ‘ ℂfld ) )
23	6 22	eqtri	⊢ − = ( -g ‘ ( Poly1 ‘ ℂfld ) )
24	4 21 23	oveq123i	⊢ ( 𝑋 − ( 𝐴 ‘ 𝑟 ) ) = ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) )
25	24	eqcomi	⊢ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) = ( 𝑋 − ( 𝐴 ‘ 𝑟 ) )
26	25	a1i	⊢ ( 𝑛 = 𝑁 → ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) = ( 𝑋 − ( 𝐴 ‘ 𝑟 ) ) )
27	18 26	mpteq12dv	⊢ ( 𝑛 = 𝑁 → ( 𝑟 ∈ ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } ) ↦ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) ) = ( 𝑟 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↦ ( 𝑋 − ( 𝐴 ‘ 𝑟 ) ) ) )
28	11 27	oveq12d	⊢ ( 𝑛 = 𝑁 → ( ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) Σg ( 𝑟 ∈ ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } ) ↦ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) ) ) = ( 𝑄 Σg ( 𝑟 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↦ ( 𝑋 − ( 𝐴 ‘ 𝑟 ) ) ) ) )
29		df-cytp	⊢ CytP = ( 𝑛 ∈ ℕ ↦ ( ( mulGrp ‘ ( Poly1 ‘ ℂfld ) ) Σg ( 𝑟 ∈ ( ◡ ( od ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) “ { 𝑛 } ) ↦ ( ( var1 ‘ ℂfld ) ( -g ‘ ( Poly1 ‘ ℂfld ) ) ( ( algSc ‘ ( Poly1 ‘ ℂfld ) ) ‘ 𝑟 ) ) ) ) )
30		ovex	⊢ ( 𝑄 Σg ( 𝑟 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↦ ( 𝑋 − ( 𝐴 ‘ 𝑟 ) ) ) ) ∈ V
31	28 29 30	fvmpt	⊢ ( 𝑁 ∈ ℕ → ( CytP ‘ 𝑁 ) = ( 𝑄 Σg ( 𝑟 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↦ ( 𝑋 − ( 𝐴 ‘ 𝑟 ) ) ) ) )