Theorem aks5lem4a

Description: Lemma for AKS section 5, reduce hypotheses. (Contributed by metakunt, 17-Jun-2025)

	Ref	Expression
Hypotheses	aks5lema.1	$$⊢\phi \to K\in \mathrm{Field}$$
	aks5lema.2	$$⊢P=\mathrm{chr}\left(K\right)$$
	aks5lema.3	$$⊢\phi \to \left(P\in \mathbb{P}\wedge N\in \mathbb{N}\wedge P\parallel N\right)$$
	aks5lema.9	$$⊢B=S{/}_{𝑠}\left(S{~}_{\mathit{QG}}L\right)$$
	aks5lema.10	$$⊢L=\mathrm{RSpan}\left(S\right)\left(\left\{\left(R{\cdot }_{{\mathrm{mulGrp}}_S}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){-}_S{1}_S\right\}\right)$$
	aks5lema.11	$$⊢\phi \to R\in \mathbb{N}$$
	aks5lema.14	$$⊢\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\}$$
	aks5lema.15	$$⊢S={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
	aks5lem4a.7	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
	aks5lem4a.12	$$⊢\phi \to A\in \mathbb{Z}$$
	aks5lem4a.13	$$⊢\phi \to \left[\left(N{\cdot }_{{\mathrm{mulGrp}}_S}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_S\mathrm{algSc}\left(S\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right]\left(S{~}_{\mathit{QG}}L\right)=\left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_S}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_S\mathrm{algSc}\left(S\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right]\left(S{~}_{\mathit{QG}}L\right)$$
Assertion	aks5lem4a	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_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(A\right)\right)\right)\left(M\right)={\mathrm{eval}}_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(A\right)\right)\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_K}M\right)$$

Proof

Step	Hyp	Ref	Expression
1		aks5lema.1	$$⊢\phi \to K\in \mathrm{Field}$$
2		aks5lema.2	$$⊢P=\mathrm{chr}\left(K\right)$$
3		aks5lema.3	$$⊢\phi \to \left(P\in \mathbb{P}\wedge N\in \mathbb{N}\wedge P\parallel N\right)$$
4		aks5lema.9	$$⊢B=S{/}_{𝑠}\left(S{~}_{\mathit{QG}}L\right)$$
5		aks5lema.10	$$⊢L=\mathrm{RSpan}\left(S\right)\left(\left\{\left(R{\cdot }_{{\mathrm{mulGrp}}_S}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){-}_S{1}_S\right\}\right)$$
6		aks5lema.11	$$⊢\phi \to R\in \mathbb{N}$$
7		aks5lema.14	$$⊢\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\}$$
8		aks5lema.15	$$⊢S={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
9		aks5lem4a.7	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
10		aks5lem4a.12	$$⊢\phi \to A\in \mathbb{Z}$$
11		aks5lem4a.13	$$⊢\phi \to \left[\left(N{\cdot }_{{\mathrm{mulGrp}}_S}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_S\mathrm{algSc}\left(S\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right]\left(S{~}_{\mathit{QG}}L\right)=\left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_S}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_S\mathrm{algSc}\left(S\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right]\left(S{~}_{\mathit{QG}}L\right)$$
12		eqid	$$⊢\left(b\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)\circ b\right)=\left(b\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)\circ b\right)$$
13		eqid	$$⊢\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)=\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)$$
14		eqid	$$⊢\left(c\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(c\right)\left(M\right)\right)=\left(c\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(c\right)\left(M\right)\right)$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}d\bigcup \left(\left(c\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(c\right)\left(M\right)\right)\circ \left(b\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)\circ b\right)\right)\left[e\right]$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}e\bigcup \left(\left(c\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(c\right)\left(M\right)\right)\circ \left(b\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)\circ b\right)\right)\left[d\right]$$
17		imaeq2	$$⊢e=d\to \left(\left(c\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(c\right)\left(M\right)\right)\circ \left(b\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)\circ b\right)\right)\left[e\right]=\left(\left(c\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(c\right)\left(M\right)\right)\circ \left(b\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)\circ b\right)\right)\left[d\right]$$
18	17	unieqd	$$⊢e=d\to \bigcup \left(\left(c\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(c\right)\left(M\right)\right)\circ \left(b\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)\circ b\right)\right)\left[e\right]=\bigcup \left(\left(c\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(c\right)\left(M\right)\right)\circ \left(b\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)\circ b\right)\right)\left[d\right]$$
19	15 16 18	cbvmpt	$$⊢\left(e\in {\mathrm{Base}}_B⟼\bigcup \left(\left(c\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(c\right)\left(M\right)\right)\circ \left(b\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)\circ b\right)\right)\left[e\right]\right)=\left(d\in {\mathrm{Base}}_B⟼\bigcup \left(\left(c\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(c\right)\left(M\right)\right)\circ \left(b\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼\left(a\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[a\right]\right)\circ b\right)\right)\left[d\right]\right)$$
20	1 2 3 4 5 6 7 8 12 13 14 9 19 10 11	aks5lem3a	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_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(A\right)\right)\right)\left(M\right)={\mathrm{eval}}_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(A\right)\right)\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_K}M\right)$$