Theorem aks6d1c1rh

Description: Claim 1 of AKS primality proof with collapsed definitions since their ease of use is no longer needed. (Contributed by metakunt, 1-May-2025)

	Ref	Expression
Hypotheses	aks6d1c1rh.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\}$$
	aks6d1c1rh.2	$$⊢P=\mathrm{chr}\left(K\right)$$
	aks6d1c1rh.3	$$⊢\phi \to K\in \mathrm{Field}$$
	aks6d1c1rh.4	$$⊢\phi \to P\in \mathbb{P}$$
	aks6d1c1rh.5	$$⊢\phi \to R\in \mathbb{N}$$
	aks6d1c1rh.6	$$⊢\phi \to N\in \mathbb{N}$$
	aks6d1c1rh.7	$$⊢\phi \to P\parallel N$$
	aks6d1c1rh.8	$$⊢\phi \to N\gcd R=1$$
	aks6d1c1rh.9	$$⊢\phi \to F:\left(0\dots A\right)⟶{\mathbb{N}}_0$$
	aks6d1c1rh.10	$$⊢G=\left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\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(i\right)\right)\right)\right)\right)$$
	aks6d1c1rh.11	$$⊢\phi \to A\in {\mathbb{N}}_0$$
	aks6d1c1rh.12	$$⊢\phi \to U\in {\mathbb{N}}_0$$
	aks6d1c1rh.13	$$⊢\phi \to L\in {\mathbb{N}}_0$$
	aks6d1c1rh.14	$$⊢E=P^U{\left(\frac{N}{P}\right)}^L$$
	aks6d1c1rh.15	$$⊢\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)$$
	aks6d1c1rh.16	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K⟼P{\cdot }_{{\mathrm{mulGrp}}_K}x\right)\in \left(K\mathrm{RingIso}K\right)$$
Assertion	aks6d1c1rh	$$⊢\phi \to E\underset{\dot{}}{\sim }G\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1rh.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		aks6d1c1rh.2	$$⊢P=\mathrm{chr}\left(K\right)$$
3		aks6d1c1rh.3	$$⊢\phi \to K\in \mathrm{Field}$$
4		aks6d1c1rh.4	$$⊢\phi \to P\in \mathbb{P}$$
5		aks6d1c1rh.5	$$⊢\phi \to R\in \mathbb{N}$$
6		aks6d1c1rh.6	$$⊢\phi \to N\in \mathbb{N}$$
7		aks6d1c1rh.7	$$⊢\phi \to P\parallel N$$
8		aks6d1c1rh.8	$$⊢\phi \to N\gcd R=1$$
9		aks6d1c1rh.9	$$⊢\phi \to F:\left(0\dots A\right)⟶{\mathbb{N}}_0$$
10		aks6d1c1rh.10	$$⊢G=\left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\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(i\right)\right)\right)\right)\right)$$
11		aks6d1c1rh.11	$$⊢\phi \to A\in {\mathbb{N}}_0$$
12		aks6d1c1rh.12	$$⊢\phi \to U\in {\mathbb{N}}_0$$
13		aks6d1c1rh.13	$$⊢\phi \to L\in {\mathbb{N}}_0$$
14		aks6d1c1rh.14	$$⊢E=P^U{\left(\frac{N}{P}\right)}^L$$
15		aks6d1c1rh.15	$$⊢\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)$$
16		aks6d1c1rh.16	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K⟼P{\cdot }_{{\mathrm{mulGrp}}_K}x\right)\in \left(K\mathrm{RingIso}K\right)$$
17		nfv	$$⊢Ⅎze{\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)$$
18		nfv	$$⊢Ⅎye{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(z\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}z\right)$$
19		fveq2	$$⊢y=z\to {\mathrm{eval}}_1\left(K\right)\left(f\right)\left(y\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(z\right)$$
20	19	oveq2d	$$⊢y=z\to e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(y\right)=e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(z\right)$$
21		oveq2	$$⊢y=z\to e{\cdot }_{{\mathrm{mulGrp}}_K}y=e{\cdot }_{{\mathrm{mulGrp}}_K}z$$
22	21	fveq2d	$$⊢y=z\to {\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}y\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}z\right)$$
23	20 22	eqeq12d	$$⊢y=z\to \left(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)\leftrightarrow e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(z\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}z\right)\right)$$
24	17 18 23	cbvralw	$$⊢\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)\leftrightarrow \forall z\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(z\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}z\right)$$
25	24	3anbi3i	$$⊢\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)\leftrightarrow \left(e\in \mathbb{N}\wedge f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \forall z\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(z\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}z\right)\right)$$
26	25	opabbii	$$⊢\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\}=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \forall z\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(z\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}z\right)\right)\right\}$$
27	1 26	eqtri	$$⊢\underset{\dot{}}{\sim }=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \forall z\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(z\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}z\right)\right)\right\}$$
28		eqid	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(K\right)$$
29		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
30		eqid	$$⊢{\mathrm{var}}_1\left(K\right)={\mathrm{var}}_1\left(K\right)$$
31		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}$$
32		eqid	$$⊢{\mathrm{mulGrp}}_K={\mathrm{mulGrp}}_K$$
33		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_K}={\cdot }_{{\mathrm{mulGrp}}_K}$$
34		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
35		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
36		eqid	$$⊢{\mathrm{eval}}_1\left(K\right)={\mathrm{eval}}_1\left(K\right)$$
37		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left(K\right)}={+}_{{\mathrm{Poly}}_1\left(K\right)}$$
38	27 28 29 30 31 32 33 34 35 2 36 37 3 4 5 6 7 8 9 10 11 12 13 14 15 16	aks6d1c1	$$⊢\phi \to E\underset{\dot{}}{\sim }G\left(F\right)$$