Theorem cytpval

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

	Ref	Expression
Hypotheses	cytpval.t	$$⊢T={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
	cytpval.o	$$⊢O=\mathrm{od}\left(T\right)$$
	cytpval.p	$$⊢P={\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)$$
	cytpval.x	$$⊢X={\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right)$$
	cytpval.q	$$⊢Q={\mathrm{mulGrp}}_P$$
	cytpval.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	cytpval.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
Assertion	cytpval	$$⊢N\in \mathbb{N}\to \mathrm{CytP}\left(N\right)=\underset{r\in O^{-1}\left[\left\{N\right\}\right]}{{\sum }_Q}\left(X\underset{\dot{}}{-}A\left(r\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cytpval.t	$$⊢T={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
2		cytpval.o	$$⊢O=\mathrm{od}\left(T\right)$$
3		cytpval.p	$$⊢P={\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)$$
4		cytpval.x	$$⊢X={\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right)$$
5		cytpval.q	$$⊢Q={\mathrm{mulGrp}}_P$$
6		cytpval.m	$$⊢\underset{\dot{}}{-}={-}_P$$
7		cytpval.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
8	3	eqcomi	$$⊢{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)=P$$
9	8	fveq2i	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}={\mathrm{mulGrp}}_P$$
10	9 5	eqtr4i	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}=Q$$
11	10	a1i	$$⊢n=N\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}=Q$$
12	1	fveq2i	$$⊢\mathrm{od}\left(T\right)=\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
13	2 12	eqtri	$$⊢O=\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
14	13	cnveqi	$$⊢O^{-1}={\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}$$
15	14	imaeq1i	$$⊢O^{-1}\left[\left\{n\right\}\right]={\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]$$
16		sneq	$$⊢n=N\to \left\{n\right\}=\left\{N\right\}$$
17	16	imaeq2d	$$⊢n=N\to O^{-1}\left[\left\{n\right\}\right]=O^{-1}\left[\left\{N\right\}\right]$$
18	15 17	eqtr3id	$$⊢n=N\to {\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]=O^{-1}\left[\left\{N\right\}\right]$$
19	3	fveq2i	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)$$
20	7 19	eqtri	$$⊢A=\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)$$
21	20	fveq1i	$$⊢A\left(r\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)$$
22	3	fveq2i	$$⊢{-}_P={-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}$$
23	6 22	eqtri	$$⊢\underset{\dot{}}{-}={-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}$$
24	4 21 23	oveq123i	$$⊢X\underset{\dot{}}{-}A\left(r\right)={\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)$$
25	24	eqcomi	$$⊢{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)=X\underset{\dot{}}{-}A\left(r\right)$$
26	25	a1i	$$⊢n=N\to {\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)=X\underset{\dot{}}{-}A\left(r\right)$$
27	18 26	mpteq12dv	$$⊢n=N\to \left(r\in {\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]⟼{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)\right)=\left(r\in O^{-1}\left[\left\{N\right\}\right]⟼X\underset{\dot{}}{-}A\left(r\right)\right)$$
28	11 27	oveq12d	$$⊢n=N\to \underset{r\in {\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}}}\left({\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)\right)=\underset{r\in O^{-1}\left[\left\{N\right\}\right]}{{\sum }_Q}\left(X\underset{\dot{}}{-}A\left(r\right)\right)$$
29		df-cytp	$$⊢\mathrm{CytP}=\left(n\in \mathbb{N}⟼\underset{r\in {\mathrm{od}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}^{-1}\left[\left\{n\right\}\right]}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}}}\left({\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}\right){-}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}\right)\right)\left(r\right)\right)\right)$$
30		ovex	$$⊢\underset{r\in O^{-1}\left[\left\{N\right\}\right]}{{\sum }_Q}\left(X\underset{\dot{}}{-}A\left(r\right)\right)\in \mathrm{V}$$
31	28 29 30	fvmpt	$$⊢N\in \mathbb{N}\to \mathrm{CytP}\left(N\right)=\underset{r\in O^{-1}\left[\left\{N\right\}\right]}{{\sum }_Q}\left(X\underset{\dot{}}{-}A\left(r\right)\right)$$