Theorem aks6d1c7lem3

Description: Remove lots of hypotheses now that we have the AKS contradiction. (Contributed by metakunt, 16-May-2025)

	Ref	Expression
Hypotheses	aks6d1c7.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \forall y\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(y\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}y\right)\right)\right\}$$
	aks6d1c7.2	$$⊢P=\mathrm{chr}\left(K\right)$$
	aks6d1c7.3	$$⊢\phi \to K\in \mathrm{Field}$$
	aks6d1c7.4	$$⊢\phi \to P\in \mathbb{P}$$
	aks6d1c7.5	$$⊢\phi \to R\in \mathbb{N}$$
	aks6d1c7.6	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
	aks6d1c7.7	$$⊢\phi \to P\parallel N$$
	aks6d1c7.8	$$⊢\phi \to N\gcd R=1$$
	aks6d1c7.9	$$⊢A=⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
	aks6d1c7.10	$$⊢\phi \to {{\log }_{2}N}^2<{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
	aks6d1c7.11	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K⟼P{\cdot }_{{\mathrm{mulGrp}}_K}x\right)\in \left(K\mathrm{RingIso}K\right)$$
	aks6d1c7.12	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
	aks6d1c7.13	$$⊢\phi \to \forall b\in \left(1\dots A\right)b\gcd N=1$$
	aks6d1c7.14	$$⊢\phi \to \forall a\in \left(1\dots A\right)N\underset{\dot{}}{\sim }\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(a\right)\right)\right)$$
	aks6d1c7lem3.1	$$⊢\phi \to \left(Q\in \mathbb{P}\wedge Q\parallel N\right)$$
Assertion	aks6d1c7lem3	$$⊢\phi \to P=Q$$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c7.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \forall y\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(y\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}y\right)\right)\right\}$$
2		aks6d1c7.2	$$⊢P=\mathrm{chr}\left(K\right)$$
3		aks6d1c7.3	$$⊢\phi \to K\in \mathrm{Field}$$
4		aks6d1c7.4	$$⊢\phi \to P\in \mathbb{P}$$
5		aks6d1c7.5	$$⊢\phi \to R\in \mathbb{N}$$
6		aks6d1c7.6	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
7		aks6d1c7.7	$$⊢\phi \to P\parallel N$$
8		aks6d1c7.8	$$⊢\phi \to N\gcd R=1$$
9		aks6d1c7.9	$$⊢A=⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
10		aks6d1c7.10	$$⊢\phi \to {{\log }_{2}N}^2<{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
11		aks6d1c7.11	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K⟼P{\cdot }_{{\mathrm{mulGrp}}_K}x\right)\in \left(K\mathrm{RingIso}K\right)$$
12		aks6d1c7.12	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
13		aks6d1c7.13	$$⊢\phi \to \forall b\in \left(1\dots A\right)b\gcd N=1$$
14		aks6d1c7.14	$$⊢\phi \to \forall a\in \left(1\dots A\right)N\underset{\dot{}}{\sim }\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(a\right)\right)\right)$$
15		aks6d1c7lem3.1	$$⊢\phi \to \left(Q\in \mathbb{P}\wedge Q\parallel N\right)$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}k{P}^i{\left(\frac{N}{P}\right)}^j$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}l{P}^i{\left(\frac{N}{P}\right)}^j$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}i{P}^k{\left(\frac{N}{P}\right)}^l$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}j{P}^k{\left(\frac{N}{P}\right)}^l$$
20		simpl	$$⊢\left(i=k\wedge j=l\right)\to i=k$$
21	20	oveq2d	$$⊢\left(i=k\wedge j=l\right)\to P^i=P^k$$
22		simpr	$$⊢\left(i=k\wedge j=l\right)\to j=l$$
23	22	oveq2d	$$⊢\left(i=k\wedge j=l\right)\to {\left(\frac{N}{P}\right)}^j={\left(\frac{N}{P}\right)}^l$$
24	21 23	oveq12d	$$⊢\left(i=k\wedge j=l\right)\to P^i{\left(\frac{N}{P}\right)}^j=P^k{\left(\frac{N}{P}\right)}^l$$
25	16 17 18 19 24	cbvmpo	$$⊢\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
26		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)=\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)$$
27		eqid	$$⊢\left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|=\left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
28		nfcv	$$⊢\underset{\_}{Ⅎ}v{\mathrm{eval}}_1\left(K\right)\left(\left(m\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{n=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)\right)\left(w\right)\right)\left(M\right)$$
29		nfcv	$$⊢\underset{\_}{Ⅎ}w{\mathrm{eval}}_1\left(K\right)\left(\left(m\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{n=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)\right)\left(v\right)\right)\left(M\right)$$
30		2fveq3	$$⊢w=v\to {\mathrm{eval}}_1\left(K\right)\left(\left(m\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{n=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)\right)\left(w\right)\right)={\mathrm{eval}}_1\left(K\right)\left(\left(m\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{n=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)\right)\left(v\right)\right)$$
31	30	fveq1d	$$⊢w=v\to {\mathrm{eval}}_1\left(K\right)\left(\left(m\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{n=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)\right)\left(w\right)\right)\left(M\right)={\mathrm{eval}}_1\left(K\right)\left(\left(m\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{n=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)\right)\left(v\right)\right)\left(M\right)$$
32	28 29 31	cbvmpt	$$⊢\left(w\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼{\mathrm{eval}}_1\left(K\right)\left(\left(m\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{n=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)\right)\left(w\right)\right)\left(M\right)\right)=\left(v\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼{\mathrm{eval}}_1\left(K\right)\left(\left(m\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{n=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)\right)\left(v\right)\right)\left(M\right)\right)$$
33		eqid	$$⊢⌊\sqrt{\left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋=⌊\sqrt{\left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋$$
34		eqid	$$⊢\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[\left(0\dots ⌊\sqrt{\left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\right)\times \left(0\dots ⌊\sqrt{\left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\right)\right]=\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[\left(0\dots ⌊\sqrt{\left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\right)\times \left(0\dots ⌊\sqrt{\left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|}⌋\right)\right]$$
35		nfcv	$$⊢\underset{\_}{Ⅎ}g\left(\underset{n=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}},\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)\right)$$
36		nfcv	$$⊢\underset{\_}{Ⅎ}m\left(\underset{h=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}},\left(g\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)\right)\right)$$
37		nfcv	$$⊢\underset{\_}{Ⅎ}h\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}n\left(m\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)\right)$$
39		fveq2	$$⊢n=h\to m\left(n\right)=m\left(h\right)$$
40		2fveq3	$$⊢n=h\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)$$
41	40	oveq2d	$$⊢n=h\to {\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)={\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)$$
42	39 41	oveq12d	$$⊢n=h\to m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)=m\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)$$
43	37 38 42	cbvmpt	$$⊢\left(n\in \left(0\dots A\right)⟼m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)=\left(h\in \left(0\dots A\right)⟼m\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)\right)$$
44	43	a1i	$$⊢m=g\to \left(n\in \left(0\dots A\right)⟼m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)=\left(h\in \left(0\dots A\right)⟼m\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)\right)$$
45		simpl	$$⊢\left(m=g\wedge h\in \left(0\dots A\right)\right)\to m=g$$
46	45	fveq1d	$$⊢\left(m=g\wedge h\in \left(0\dots A\right)\right)\to m\left(h\right)=g\left(h\right)$$
47	46	oveq1d	$$⊢\left(m=g\wedge h\in \left(0\dots A\right)\right)\to m\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)=g\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)$$
48	47	mpteq2dva	$$⊢m=g\to \left(h\in \left(0\dots A\right)⟼m\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)\right)=\left(h\in \left(0\dots A\right)⟼g\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)\right)$$
49	44 48	eqtrd	$$⊢m=g\to \left(n\in \left(0\dots A\right)⟼m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)=\left(h\in \left(0\dots A\right)⟼g\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)\right)$$
50	49	oveq2d	$$⊢m=g\to \underset{n=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)=\underset{h=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)\right)$$
51	35 36 50	cbvmpt	$$⊢\left(m\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{n=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(m\left(n\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(n\right)\right)\right)\right)\right)=\left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{h=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(h\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(h\right)\right)\right)\right)\right)$$
52		nfcv	$$⊢\underset{\_}{Ⅎ}u\left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)$$
53		nfcv	$$⊢\underset{\_}{Ⅎ}o\left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)$$
54		nfv	$$⊢Ⅎo\sum _{q=0}^{A}u\left(q\right)\le \left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1$$
55		nfv	$$⊢Ⅎu\sum _{p=0}^{A}o\left(p\right)\le \left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1$$
56		simpl	$$⊢\left(u=o\wedge q\in \left(0\dots A\right)\right)\to u=o$$
57	56	fveq1d	$$⊢\left(u=o\wedge q\in \left(0\dots A\right)\right)\to u\left(q\right)=o\left(q\right)$$
58	57	sumeq2dv	$$⊢u=o\to \sum _{q=0}^{A}u\left(q\right)=\sum _{q=0}^{A}o\left(q\right)$$
59		fveq2	$$⊢q=p\to o\left(q\right)=o\left(p\right)$$
60		nfcv	$$⊢\underset{\_}{Ⅎ}po\left(q\right)$$
61		nfcv	$$⊢\underset{\_}{Ⅎ}qo\left(p\right)$$
62	59 60 61	cbvsum	$$⊢\sum _{q=0}^{A}o\left(q\right)=\sum _{p=0}^{A}o\left(p\right)$$
63	62	a1i	$$⊢u=o\to \sum _{q=0}^{A}o\left(q\right)=\sum _{p=0}^{A}o\left(p\right)$$
64	58 63	eqtrd	$$⊢u=o\to \sum _{q=0}^{A}u\left(q\right)=\sum _{p=0}^{A}o\left(p\right)$$
65	25	eqcomi	$$⊢\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)=\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)$$
66	65	a1i	$$⊢u=o\to \left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)=\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)$$
67	66	imaeq1d	$$⊢u=o\to \left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]=\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]$$
68	67	imaeq2d	$$⊢u=o\to \mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]=\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]$$
69	68	fveq2d	$$⊢u=o\to \left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|=\left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
70	69	oveq1d	$$⊢u=o\to \left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1=\left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1$$
71	64 70	breq12d	$$⊢u=o\to \left(\sum _{q=0}^{A}u\left(q\right)\le \left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1\leftrightarrow \sum _{p=0}^{A}o\left(p\right)\le \left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1\right)$$
72	52 53 54 55 71	cbvrabw	$$⊢\left\{u\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)|\sum _{q=0}^{A}u\left(q\right)\le \left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1\right\}=\left\{o\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)|\sum _{p=0}^{A}o\left(p\right)\le \left|\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)\left[\left(i\in {\mathbb{N}}_0,j\in {\mathbb{N}}_0⟼P^i{\left(\frac{N}{P}\right)}^j\right)\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|-1\right\}$$
73	1 2 3 4 5 6 7 8 25 26 27 9 10 11 12 32 33 34 15 13 51 14 72	aks6d1c7lem2	$$⊢\phi \to P=Q$$