Theorem aks5lem3a

Description: Lemma for AKS section 5. (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)$$
	aks5lem3a.4	$$⊢F=\left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼G\circ p\right)$$
	aks5lem3a.5	$$⊢G=\left(q\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[q\right]\right)$$
	aks5lem3a.6	$$⊢H=\left(r\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(r\right)\left(M\right)\right)$$
	aks5lem3a.7	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
	aks5lem3a.8	$$⊢I=\left(s\in {\mathrm{Base}}_B⟼\bigcup \left(H\circ F\right)\left[s\right]\right)$$
	aks5lem3a.12	$$⊢\phi \to A\in \mathbb{Z}$$
	aks5lem3a.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	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)$$

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		aks5lem3a.4	$$⊢F=\left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼G\circ p\right)$$
10		aks5lem3a.5	$$⊢G=\left(q\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[q\right]\right)$$
11		aks5lem3a.6	$$⊢H=\left(r\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(r\right)\left(M\right)\right)$$
12		aks5lem3a.7	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
13		aks5lem3a.8	$$⊢I=\left(s\in {\mathrm{Base}}_B⟼\bigcup \left(H\circ F\right)\left[s\right]\right)$$
14		aks5lem3a.12	$$⊢\phi \to A\in \mathbb{Z}$$
15		aks5lem3a.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)$$
16	1	fldcrngd	$$⊢\phi \to K\in \mathrm{CRing}$$
17		eqid	$$⊢{\mathrm{mulGrp}}_K={\mathrm{mulGrp}}_K$$
18	17	crngmgp	$$⊢K\in \mathrm{CRing}\to {\mathrm{mulGrp}}_K\in \mathrm{CMnd}$$
19	16 18	syl	$$⊢\phi \to {\mathrm{mulGrp}}_K\in \mathrm{CMnd}$$
20	6	nnnn0d	$$⊢\phi \to R\in {\mathbb{N}}_0$$
21		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_K}={\cdot }_{{\mathrm{mulGrp}}_K}$$
22	19 20 21	isprimroot	$$⊢\phi \to \left(M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)\leftrightarrow \left(M\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_K}\wedge R{\cdot }_{{\mathrm{mulGrp}}_K}M=0_{{\mathrm{mulGrp}}_K}\wedge \forall d\in {\mathbb{N}}_0\left(d{\cdot }_{{\mathrm{mulGrp}}_K}M=0_{{\mathrm{mulGrp}}_K}\to R\parallel d\right)\right)\right)$$
23	12 22	mpbid	$$⊢\phi \to \left(M\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_K}\wedge R{\cdot }_{{\mathrm{mulGrp}}_K}M=0_{{\mathrm{mulGrp}}_K}\wedge \forall d\in {\mathbb{N}}_0\left(d{\cdot }_{{\mathrm{mulGrp}}_K}M=0_{{\mathrm{mulGrp}}_K}\to R\parallel d\right)\right)$$
24	23	simp1d	$$⊢\phi \to M\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
25		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
26	17 25	mgpbas	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
27	26	eqcomi	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_K}={\mathrm{Base}}_K$$
28	24 27	eleqtrdi	$$⊢\phi \to M\in {\mathrm{Base}}_K$$
29	1 2 3 9 10 11 28	aks5lem1	$$⊢\phi \to H\circ F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}K\right)$$
30		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
31	30 17	rhmmhm	$$⊢H\circ F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}K\right)\to H\circ F\in \left({\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{MndHom}{\mathrm{mulGrp}}_K\right)$$
32	29 31	syl	$$⊢\phi \to H\circ F\in \left({\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{MndHom}{\mathrm{mulGrp}}_K\right)$$
33	3	simp2d	$$⊢\phi \to N\in \mathbb{N}$$
34	33	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
35		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
36		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}={+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
37		eqid	$$⊢\mathbb{Z}/N\mathbb{Z}=\mathbb{Z}/N\mathbb{Z}$$
38	37	zncrng	$$⊢N\in {\mathbb{N}}_0\to \mathbb{Z}/N\mathbb{Z}\in \mathrm{CRing}$$
39	34 38	syl	$$⊢\phi \to \mathbb{Z}/N\mathbb{Z}\in \mathrm{CRing}$$
40		eqid	$$⊢{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
41	40	ply1crng	$$⊢\mathbb{Z}/N\mathbb{Z}\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{CRing}$$
42	39 41	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{CRing}$$
43	42	crngringd	$$⊢\phi \to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{Ring}$$
44		ringgrp	$$⊢{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{Ring}\to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{Grp}$$
45	43 44	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{Grp}$$
46	39	crngringd	$$⊢\phi \to \mathbb{Z}/N\mathbb{Z}\in \mathrm{Ring}$$
47		eqid	$$⊢{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)={\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
48	47 40 35	vr1cl	$$⊢\mathbb{Z}/N\mathbb{Z}\in \mathrm{Ring}\to {\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
49	46 48	syl	$$⊢\phi \to {\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
50		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)$$
51		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)=\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)$$
52		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)=\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)$$
53	40 50 51 52 39 14	ply1asclzrhval	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)=\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(A\right)$$
54	51	zrhrhm	$$⊢{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)$$
55		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
56	55 35	rhmf	$$⊢\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\to \mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right):\mathbb{Z}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
57	54 56	syl	$$⊢{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right):\mathbb{Z}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
58	43 57	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right):\mathbb{Z}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
59	58 14	ffvelcdmd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
60	53 59	eqeltrd	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
61	35 36 45 49 60	grpcld	$$⊢\phi \to {\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
62	30 35	mgpbas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}$$
63		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}$$
64	62 63 21	mhmmulg	$$⊢\left(H\circ F\in \left({\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{MndHom}{\mathrm{mulGrp}}_K\right)\wedge N\in {\mathbb{N}}_0\wedge {\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\to \left(H\circ F\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)=N{\cdot }_{{\mathrm{mulGrp}}_K}\left(H\circ F\right)\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)$$
65	32 34 61 64	syl3anc	$$⊢\phi \to \left(H\circ F\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)=N{\cdot }_{{\mathrm{mulGrp}}_K}\left(H\circ F\right)\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)$$
66		eqid	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(K\right)$$
67	16	crngringd	$$⊢\phi \to K\in \mathrm{Ring}$$
68	2	eqcomi	$$⊢\mathrm{chr}\left(K\right)=P$$
69	3	simp1d	$$⊢\phi \to P\in \mathbb{P}$$
70		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
71	69 70	syl	$$⊢\phi \to P\in \mathbb{N}$$
72	71	nnzd	$$⊢\phi \to P\in \mathbb{Z}$$
73	68 72	eqeltrid	$$⊢\phi \to \mathrm{chr}\left(K\right)\in \mathbb{Z}$$
74	68	a1i	$$⊢\phi \to \mathrm{chr}\left(K\right)=P$$
75	3	simp3d	$$⊢\phi \to P\parallel N$$
76	74 75	eqbrtrd	$$⊢\phi \to \mathrm{chr}\left(K\right)\parallel N$$
77	67 33 73 76 37 10	zndvdchrrhm	$$⊢\phi \to G\in \left(\mathbb{Z}/N\mathbb{Z}\mathrm{RingHom}K\right)$$
78	40 66 35 9 77	rhmply1	$$⊢\phi \to F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}{\mathrm{Poly}}_1\left(K\right)\right)$$
79		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
80	35 79	rhmf	$$⊢F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}{\mathrm{Poly}}_1\left(K\right)\right)\to F:{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
81	78 80	syl	$$⊢\phi \to F:{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
82	81 61	fvco3d	$$⊢\phi \to \left(H\circ F\right)\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=H\left(F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)$$
83	11	a1i	$$⊢\phi \to H=\left(r\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼{\mathrm{eval}}_1\left(K\right)\left(r\right)\left(M\right)\right)$$
84		simpr	$$⊢\left(\phi \wedge r=F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\to r=F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)$$
85	84	fveq2d	$$⊢\left(\phi \wedge r=F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\to {\mathrm{eval}}_1\left(K\right)\left(r\right)={\mathrm{eval}}_1\left(K\right)\left(F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)$$
86	85	fveq1d	$$⊢\left(\phi \wedge r=F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\to {\mathrm{eval}}_1\left(K\right)\left(r\right)\left(M\right)={\mathrm{eval}}_1\left(K\right)\left(F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\left(M\right)$$
87	81 61	ffvelcdmd	$$⊢\phi \to F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
88		fvexd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\left(M\right)\in \mathrm{V}$$
89	83 86 87 88	fvmptd	$$⊢\phi \to H\left(F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)={\mathrm{eval}}_1\left(K\right)\left(F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\left(M\right)$$
90		rhmghm	$$⊢F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}{\mathrm{Poly}}_1\left(K\right)\right)\to F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{GrpHom}{\mathrm{Poly}}_1\left(K\right)\right)$$
91	78 90	syl	$$⊢\phi \to F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{GrpHom}{\mathrm{Poly}}_1\left(K\right)\right)$$
92		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left(K\right)}={+}_{{\mathrm{Poly}}_1\left(K\right)}$$
93	35 36 92	ghmlin	$$⊢\left(F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{GrpHom}{\mathrm{Poly}}_1\left(K\right)\right)\wedge {\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\wedge \mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\to F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)$$
94	91 49 60 93	syl3anc	$$⊢\phi \to F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)$$
95		eqid	$$⊢{\mathrm{var}}_1\left(K\right)={\mathrm{var}}_1\left(K\right)$$
96	40 66 35 9 47 95 77	rhmply1vr1	$$⊢\phi \to F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)={\mathrm{var}}_1\left(K\right)$$
97	53	fveq2d	$$⊢\phi \to F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=F\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(A\right)\right)$$
98		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)=\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
99	78 14 51 98	rhmzrhval	$$⊢\phi \to F\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(A\right)\right)=\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)$$
100	97 99	eqtrd	$$⊢\phi \to F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)$$
101		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
102		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(K\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)$$
103	66 101 98 102 16 14	ply1asclzrhval	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)\right)=\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)$$
104	100 103	eqtr4d	$$⊢\phi \to F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)\right)$$
105	96 104	oveq12d	$$⊢\phi \to F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\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(A\right)\right)$$
106	94 105	eqtrd	$$⊢\phi \to F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\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(A\right)\right)$$
107	106	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\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)$$
108	107	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\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(M\right)$$
109	89 108	eqtrd	$$⊢\phi \to H\left(F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\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(M\right)$$
110	82 109	eqtrd	$$⊢\phi \to \left(H\circ F\right)\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\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(M\right)$$
111	110	oveq2d	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_K}\left(H\circ F\right)\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=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)$$
112	65 111	eqtr2d	$$⊢\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)=\left(H\circ F\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)$$
113		eceq1	$$⊢u=N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\to \left[u\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)=\left[\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)$$
114	113	fveq2d	$$⊢u=N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\to I\left(\left[u\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=I\left(\left[\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)$$
115		fveq2	$$⊢u=N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\to \left(H\circ F\right)\left(u\right)=\left(H\circ F\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)$$
116	114 115	eqeq12d	$$⊢u=N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\to \left(I\left(\left[u\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=\left(H\circ F\right)\left(u\right)\leftrightarrow I\left(\left[\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=\left(H\circ F\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right)$$
117	8	oveq1i	$$⊢S{~}_{\mathit{QG}}L={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L$$
118	8 117	oveq12i	$$⊢S{/}_{𝑠}\left(S{~}_{\mathit{QG}}L\right)={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){/}_{𝑠}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)$$
119	4 118	eqtri	$$⊢B={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){/}_{𝑠}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)$$
120	8	fveq2i	$$⊢\mathrm{RSpan}\left(S\right)=\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)$$
121	8	fveq2i	$$⊢{\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
122	121	fveq2i	$$⊢{\cdot }_{{\mathrm{mulGrp}}_S}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}$$
123	122	oveqi	$$⊢R{\cdot }_{{\mathrm{mulGrp}}_S}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)=R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
124	8	fveq2i	$$⊢1_S=1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
125	8	fveq2i	$$⊢{-}_S={-}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
126	123 124 125	oveq123i	$$⊢\left(R{\cdot }_{{\mathrm{mulGrp}}_S}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){-}_S{1}_S=\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){-}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}{1}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
127	126	sneqi	$$⊢\left\{\left(R{\cdot }_{{\mathrm{mulGrp}}_S}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){-}_S{1}_S\right\}=\left\{\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){-}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}{1}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right\}$$
128	120 127	fveq12i	$$⊢\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)=\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\left\{\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){-}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}{1}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right\}\right)$$
129	5 128	eqtri	$$⊢L=\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\left\{\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){-}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}{1}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right\}\right)$$
130	1 2 3 9 10 11 12 13 119 129 6	aks5lem2	$$⊢\phi \to \left(I\in \left(B\mathrm{RingHom}K\right)\wedge \forall u\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}I\left(\left[u\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=\left(H\circ F\right)\left(u\right)\right)$$
131	130	simprd	$$⊢\phi \to \forall u\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}I\left(\left[u\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=\left(H\circ F\right)\left(u\right)$$
132	30	ringmgp	$$⊢{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\in \mathrm{Mnd}$$
133	43 132	syl	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\in \mathrm{Mnd}$$
134	62 63 133 34 61	mulgnn0cld	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
135	116 131 134	rspcdva	$$⊢\phi \to I\left(\left[\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=\left(H\circ F\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)$$
136	135	eqcomd	$$⊢\phi \to \left(H\circ F\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)=I\left(\left[\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)$$
137	8	eqcomi	$$⊢{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)=S$$
138	137	a1i	$$⊢\phi \to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)=S$$
139	138	fveq2d	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}={\mathrm{mulGrp}}_S$$
140	139	fveq2d	$$⊢\phi \to {\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}={\cdot }_{{\mathrm{mulGrp}}_S}$$
141		eqidd	$$⊢\phi \to N=N$$
142	138	fveq2d	$$⊢\phi \to {+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}={+}_S$$
143		eqidd	$$⊢\phi \to {\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)={\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
144	138	fveq2d	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)=\mathrm{algSc}\left(S\right)$$
145	144	fveq1d	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)=\mathrm{algSc}\left(S\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)$$
146	142 143 145	oveq123d	$$⊢\phi \to {\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)={\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)$$
147	140 141 146	oveq123d	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=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)$$
148	147	eceq1d	$$⊢\phi \to \left[\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)=\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({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)$$
149	138	oveq1d	$$⊢\phi \to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L=S{~}_{\mathit{QG}}L$$
150	149	eceq2d	$$⊢\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({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)=\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)$$
151	148 150	eqtrd	$$⊢\phi \to \left[\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)=\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)$$
152		eqcom	$$⊢{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)=S\leftrightarrow S={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
153	152	imbi2i	$$⊢\left(\phi \to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)=S\right)\leftrightarrow \left(\phi \to S={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)$$
154	138 153	mpbi	$$⊢\phi \to S={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
155	154	fveq2d	$$⊢\phi \to {+}_S={+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
156	154	fveq2d	$$⊢\phi \to {\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
157	156	fveq2d	$$⊢\phi \to {\cdot }_{{\mathrm{mulGrp}}_S}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}$$
158	157	oveqd	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_S}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)=N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
159	154	fveq2d	$$⊢\phi \to \mathrm{algSc}\left(S\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)$$
160	159	fveq1d	$$⊢\phi \to \mathrm{algSc}\left(S\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)$$
161	155 158 160	oveq123d	$$⊢\phi \to \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)=\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)$$
162	161	eceq1d	$$⊢\phi \to \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)=\left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\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)$$
163	149	eqcomd	$$⊢\phi \to S{~}_{\mathit{QG}}L={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L$$
164	163	eceq2d	$$⊢\phi \to \left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\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)=\left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)$$
165	162 164	eqtrd	$$⊢\phi \to \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)=\left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)$$
166	151 15 165	3eqtrd	$$⊢\phi \to \left[\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)=\left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)$$
167	166	fveq2d	$$⊢\phi \to I\left(\left[\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=I\left(\left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)$$
168		eceq1	$$⊢u=\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\to \left[u\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)=\left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)$$
169	168	fveq2d	$$⊢u=\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\to I\left(\left[u\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=I\left(\left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)$$
170		fveq2	$$⊢u=\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\to \left(H\circ F\right)\left(u\right)=\left(H\circ F\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)$$
171	169 170	eqeq12d	$$⊢u=\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\to \left(I\left(\left[u\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=\left(H\circ F\right)\left(u\right)\leftrightarrow I\left(\left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=\left(H\circ F\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)$$
172	62 63 133 34 49	mulgnn0cld	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
173	35 36 45 172 60	grpcld	$$⊢\phi \to \left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
174	171 131 173	rspcdva	$$⊢\phi \to I\left(\left[\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=\left(H\circ F\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)$$
175	136 167 174	3eqtrd	$$⊢\phi \to \left(H\circ F\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)=\left(H\circ F\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)$$
176	81 173	fvco3d	$$⊢\phi \to \left(H\circ F\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=H\left(F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)$$
177		simpr	$$⊢\left(\phi \wedge r=F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\to r=F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)$$
178	177	fveq2d	$$⊢\left(\phi \wedge r=F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\to {\mathrm{eval}}_1\left(K\right)\left(r\right)={\mathrm{eval}}_1\left(K\right)\left(F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)$$
179	178	fveq1d	$$⊢\left(\phi \wedge r=F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\to {\mathrm{eval}}_1\left(K\right)\left(r\right)\left(M\right)={\mathrm{eval}}_1\left(K\right)\left(F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\left(M\right)$$
180	81 173	ffvelcdmd	$$⊢\phi \to F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
181		fvexd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\left(M\right)\in \mathrm{V}$$
182	83 179 180 181	fvmptd	$$⊢\phi \to H\left(F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)={\mathrm{eval}}_1\left(K\right)\left(F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\left(M\right)$$
183	35 36 92	ghmlin	$$⊢\left(F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{GrpHom}{\mathrm{Poly}}_1\left(K\right)\right)\wedge N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\wedge \mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\to F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=F\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)$$
184	91 172 60 183	syl3anc	$$⊢\phi \to F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=F\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)$$
185	184	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)={\mathrm{eval}}_1\left(K\right)\left(F\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)$$
186	185	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\left(M\right)={\mathrm{eval}}_1\left(K\right)\left(F\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\left(M\right)$$
187		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}$$
188	30 187	rhmmhm	$$⊢F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}{\mathrm{Poly}}_1\left(K\right)\right)\to F\in \left({\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{MndHom}{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\right)$$
189	78 188	syl	$$⊢\phi \to F\in \left({\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{MndHom}{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\right)$$
190		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
191	62 63 190	mhmmulg	$$⊢\left(F\in \left({\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{MndHom}{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\right)\wedge N\in {\mathbb{N}}_0\wedge {\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\to F\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)=N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)$$
192	189 34 49 191	syl3anc	$$⊢\phi \to F\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)=N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)$$
193	192 97	oveq12d	$$⊢\phi \to F\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)=\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(A\right)\right)$$
194	193	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(F\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)={\mathrm{eval}}_1\left(K\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(A\right)\right)\right)$$
195	194	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(F\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\right)\left(M\right)={\mathrm{eval}}_1\left(K\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(A\right)\right)\right)\left(M\right)$$
196	96	oveq2d	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)=N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)$$
197	196 99	oveq12d	$$⊢\phi \to \left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(A\right)\right)=\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)$$
198	197	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(A\right)\right)\right)={\mathrm{eval}}_1\left(K\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)$$
199	198	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(A\right)\right)\right)\left(M\right)={\mathrm{eval}}_1\left(K\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)$$
200		eqid	$$⊢{\mathrm{eval}}_1\left(K\right)={\mathrm{eval}}_1\left(K\right)$$
201	200 95 25 66 79 16 28	evl1vard	$$⊢\phi \to \left({\mathrm{var}}_1\left(K\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right)\right)\left(M\right)=M\right)$$
202	200 66 25 79 16 28 201 190 21 34	evl1expd	$$⊢\phi \to \left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\left(M\right)=N{\cdot }_{{\mathrm{mulGrp}}_K}M\right)$$
203	66	ply1crng	$$⊢K\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}$$
204	16 203	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}$$
205	204	crngringd	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}$$
206	98	zrhrhm	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}{\mathrm{Poly}}_1\left(K\right)\right)$$
207	55 79	rhmf	$$⊢\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}{\mathrm{Poly}}_1\left(K\right)\right)\to \mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right):\mathbb{Z}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
208	206 207	syl	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right):\mathbb{Z}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
209	205 208	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right):\mathbb{Z}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
210	209 14	ffvelcdmd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
211		eqidd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)={\mathrm{eval}}_1\left(K\right)\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)$$
212	210 211	jca	$$⊢\phi \to \left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)={\mathrm{eval}}_1\left(K\right)\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)\right)$$
213		eqid	$$⊢{+}_K={+}_K$$
214	200 66 25 79 16 28 202 212 92 213	evl1addd	$$⊢\phi \to \left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)=\left(N{\cdot }_{{\mathrm{mulGrp}}_K}M\right){+}_K{\mathrm{eval}}_1\left(K\right)\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)\right)$$
215	214	simprd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)=\left(N{\cdot }_{{\mathrm{mulGrp}}_K}M\right){+}_K{\mathrm{eval}}_1\left(K\right)\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)$$
216	102	zrhrhm	$$⊢K\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)$$
217	55 25	rhmf	$$⊢\mathrm{\mathbb{Z}RHom}\left(K\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)\to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
218	216 217	syl	$$⊢K\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
219	67 218	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right):\mathbb{Z}⟶{\mathrm{Base}}_K$$
220	219 14	ffvelcdmd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)\in {\mathrm{Base}}_K$$
221	200 66 25 101 79 16 220 28	evl1scad	$$⊢\phi \to \left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\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{\mathbb{Z}RHom}\left(K\right)\left(A\right)\right)$$
222	221	simprd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\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{\mathbb{Z}RHom}\left(K\right)\left(A\right)$$
223	222	eqcomd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)={\mathrm{eval}}_1\left(K\right)\left(\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)$$
224	103	fveq2d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)\right)\right)={\mathrm{eval}}_1\left(K\right)\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)$$
225	224	fveq1d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\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{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)$$
226	223 225	eqtr2d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)$$
227	226	oveq2d	$$⊢\phi \to \left(N{\cdot }_{{\mathrm{mulGrp}}_K}M\right){+}_K{\mathrm{eval}}_1\left(K\right)\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)=\left(N{\cdot }_{{\mathrm{mulGrp}}_K}M\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)$$
228	215 227	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(A\right)\right)\left(M\right)=\left(N{\cdot }_{{\mathrm{mulGrp}}_K}M\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)$$
229	199 228	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(A\right)\right)\right)\left(M\right)=\left(N{\cdot }_{{\mathrm{mulGrp}}_K}M\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)$$
230	19	cmnmndd	$$⊢\phi \to {\mathrm{mulGrp}}_K\in \mathrm{Mnd}$$
231	26 21 230 34 28	mulgnn0cld	$$⊢\phi \to N{\cdot }_{{\mathrm{mulGrp}}_K}M\in {\mathrm{Base}}_K$$
232	200 95 25 66 79 16 231	evl1vard	$$⊢\phi \to \left({\mathrm{var}}_1\left(K\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left({\mathrm{var}}_1\left(K\right)\right)\left(N{\cdot }_{{\mathrm{mulGrp}}_K}M\right)=N{\cdot }_{{\mathrm{mulGrp}}_K}M\right)$$
233	200 66 25 101 79 16 220 231	evl1scad	$$⊢\phi \to \left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\mathrm{eval}}_1\left(K\right)\left(\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)=\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)\right)$$
234	200 66 25 79 16 231 232 233 92 213	evl1addd	$$⊢\phi \to \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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge {\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)=\left(N{\cdot }_{{\mathrm{mulGrp}}_K}M\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)\right)$$
235	234	simprd	$$⊢\phi \to {\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)=\left(N{\cdot }_{{\mathrm{mulGrp}}_K}M\right){+}_K\mathrm{\mathbb{Z}RHom}\left(K\right)\left(A\right)$$
236	229 235	eqtr4d	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}F\left({\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{\mathbb{Z}RHom}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\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)$$
237	195 236	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(F\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(K\right)}F\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\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)$$
238	186 237	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\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)$$
239	182 238	eqtrd	$$⊢\phi \to H\left(F\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\right)\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)$$
240	176 239	eqtrd	$$⊢\phi \to \left(H\circ F\right)\left(\left(N{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right){+}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/N\mathbb{Z}\right)\left(A\right)\right)\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)$$
241	112 175 240	3eqtrd	$$⊢\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)$$