Theorem aks5lem2

Description: Lemma for section 5 https://www3.nd.edu/%7eandyp/notes/AKS.pdf. Construct the quotient for the AKS reduction. (Contributed by metakunt, 7-Jun-2025)

	Ref	Expression
Hypotheses	aks5lem1.1	$$⊢\phi \to K\in \mathrm{Field}$$
	aks5lem1.2	$$⊢P=\mathrm{chr}\left(K\right)$$
	aks5lem1.3	$$⊢\phi \to \left(P\in \mathbb{P}\wedge N\in \mathbb{N}\wedge P\parallel N\right)$$
	aks5lem1.4	$$⊢F=\left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼G\circ p\right)$$
	aks5lem1.5	$$⊢G=\left(q\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[q\right]\right)$$
	aks5lem1.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)$$
	aks5lem2.1	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
	aks5lem2.2	$$⊢I=\left(s\in {\mathrm{Base}}_A⟼\bigcup \left(H\circ F\right)\left[s\right]\right)$$
	aks5lem2.3	$$⊢A={\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)$$
	aks5lem2.4	$$⊢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)$$
	aks5lem2.5	$$⊢\phi \to R\in \mathbb{N}$$
Assertion	aks5lem2	$$⊢\phi \to \left(I\in \left(A\mathrm{RingHom}K\right)\wedge \forall g\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}I\left(\left[g\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=\left(H\circ F\right)\left(g\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		aks5lem1.1	$$⊢\phi \to K\in \mathrm{Field}$$
2		aks5lem1.2	$$⊢P=\mathrm{chr}\left(K\right)$$
3		aks5lem1.3	$$⊢\phi \to \left(P\in \mathbb{P}\wedge N\in \mathbb{N}\wedge P\parallel N\right)$$
4		aks5lem1.4	$$⊢F=\left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟼G\circ p\right)$$
5		aks5lem1.5	$$⊢G=\left(q\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[q\right]\right)$$
6		aks5lem1.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)$$
7		aks5lem2.1	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
8		aks5lem2.2	$$⊢I=\left(s\in {\mathrm{Base}}_A⟼\bigcup \left(H\circ F\right)\left[s\right]\right)$$
9		aks5lem2.3	$$⊢A={\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)$$
10		aks5lem2.4	$$⊢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)$$
11		aks5lem2.5	$$⊢\phi \to R\in \mathbb{N}$$
12		eqid	$$⊢0_K=0_K$$
13	1	fldcrngd	$$⊢\phi \to K\in \mathrm{CRing}$$
14		eqid	$$⊢{\mathrm{mulGrp}}_K={\mathrm{mulGrp}}_K$$
15	14	crngmgp	$$⊢K\in \mathrm{CRing}\to {\mathrm{mulGrp}}_K\in \mathrm{CMnd}$$
16	13 15	syl	$$⊢\phi \to {\mathrm{mulGrp}}_K\in \mathrm{CMnd}$$
17	11	nnnn0d	$$⊢\phi \to R\in {\mathbb{N}}_0$$
18		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_K}={\cdot }_{{\mathrm{mulGrp}}_K}$$
19	16 17 18	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 l\in {\mathbb{N}}_0\left(l{\cdot }_{{\mathrm{mulGrp}}_K}M=0_{{\mathrm{mulGrp}}_K}\to R\parallel l\right)\right)\right)$$
20	7 19	mpbid	$$⊢\phi \to \left(M\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_K}\wedge R{\cdot }_{{\mathrm{mulGrp}}_K}M=0_{{\mathrm{mulGrp}}_K}\wedge \forall l\in {\mathbb{N}}_0\left(l{\cdot }_{{\mathrm{mulGrp}}_K}M=0_{{\mathrm{mulGrp}}_K}\to R\parallel l\right)\right)$$
21	20	simp1d	$$⊢\phi \to M\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
22		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
23	14 22	mgpbas	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
24	23	eqcomi	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_K}={\mathrm{Base}}_K$$
25	21 24	eleqtrdi	$$⊢\phi \to M\in {\mathrm{Base}}_K$$
26	1 2 3 4 5 6 25	aks5lem1	$$⊢\phi \to H\circ F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}K\right)$$
27		eqid	$$⊢{\left(H\circ F\right)}^{-1}\left[\left\{0_K\right\}\right]={\left(H\circ F\right)}^{-1}\left[\left\{0_K\right\}\right]$$
28	3	simp2d	$$⊢\phi \to N\in \mathbb{N}$$
29	28	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
30		eqid	$$⊢\mathbb{Z}/N\mathbb{Z}=\mathbb{Z}/N\mathbb{Z}$$
31	30	zncrng	$$⊢N\in {\mathbb{N}}_0\to \mathbb{Z}/N\mathbb{Z}\in \mathrm{CRing}$$
32	29 31	syl	$$⊢\phi \to \mathbb{Z}/N\mathbb{Z}\in \mathrm{CRing}$$
33		eqid	$$⊢{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
34	33	ply1crng	$$⊢\mathbb{Z}/N\mathbb{Z}\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{CRing}$$
35	32 34	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{CRing}$$
36	35	crnggrpd	$$⊢\phi \to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{Grp}$$
37		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)}$$
38		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)}$$
39	37 38	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)}}$$
40		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)}}$$
41	35	crngringd	$$⊢\phi \to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{Ring}$$
42	37	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}$$
43	41 42	syl	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\in \mathrm{Mnd}$$
44	32	crngringd	$$⊢\phi \to \mathbb{Z}/N\mathbb{Z}\in \mathrm{Ring}$$
45		eqid	$$⊢{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)={\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
46	45 33 38	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)}$$
47	44 46	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)}$$
48	39 40 43 17 47	mulgnn0cld	$$⊢\phi \to R{\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)}$$
49		eqid	$$⊢1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}=1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
50	38 49	ringidcl	$$⊢{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{Ring}\to 1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
51	41 50	syl	$$⊢\phi \to 1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
52		eqid	$$⊢{-}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}={-}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
53	38 52	grpsubcl	$$⊢\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{Grp}\wedge R{\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 1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\to \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)}\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
54	36 48 51 53	syl3anc	$$⊢\phi \to \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)}\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
55		fvexd	$$⊢\phi \to {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}\in \mathrm{V}$$
56	55	mptexd	$$⊢\phi \to \left(q\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}⟼\bigcup \mathrm{\mathbb{Z}RHom}\left(K\right)\left[q\right]\right)\in \mathrm{V}$$
57	5 56	eqeltrid	$$⊢\phi \to G\in \mathrm{V}$$
58	57	adantr	$$⊢\left(\phi \wedge p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\to G\in \mathrm{V}$$
59		vex	$$⊢p\in \mathrm{V}$$
60	59	a1i	$$⊢\left(\phi \wedge p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\to p\in \mathrm{V}$$
61	58 60	coexd	$$⊢\left(\phi \wedge p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\to G\circ p\in \mathrm{V}$$
62	61 4	fmptd	$$⊢\phi \to F:{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟶\mathrm{V}$$
63	62	ffund	$$⊢\phi \to \mathrm{Fun}F$$
64	62	fdmd	$$⊢\phi \to \mathrm{dom}F={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
65	54 64	eleqtrrd	$$⊢\phi \to \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)}\in \mathrm{dom}F$$
66		fvco	$$⊢\left(\mathrm{Fun}F\wedge \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)}\in \mathrm{dom}F\right)\to \left(H\circ F\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)=H\left(F\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)$$
67	63 65 66	syl2anc	$$⊢\phi \to \left(H\circ F\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)=H\left(F\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)$$
68		eqid	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(K\right)$$
69	13	crngringd	$$⊢\phi \to K\in \mathrm{Ring}$$
70	3	simp1d	$$⊢\phi \to P\in \mathbb{P}$$
71		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
72	70 71	syl	$$⊢\phi \to P\in \mathbb{N}$$
73	2 72	eqeltrrid	$$⊢\phi \to \mathrm{chr}\left(K\right)\in \mathbb{N}$$
74	73	nnzd	$$⊢\phi \to \mathrm{chr}\left(K\right)\in \mathbb{Z}$$
75	3	simp3d	$$⊢\phi \to P\parallel N$$
76	2 75	eqbrtrrid	$$⊢\phi \to \mathrm{chr}\left(K\right)\parallel N$$
77	69 28 74 76 30 5	zndvdchrrhm	$$⊢\phi \to G\in \left(\mathbb{Z}/N\mathbb{Z}\mathrm{RingHom}K\right)$$
78	33 68 38 4 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		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)$$
80	78 79	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)$$
81		eqid	$$⊢{-}_{{\mathrm{Poly}}_1\left(K\right)}={-}_{{\mathrm{Poly}}_1\left(K\right)}$$
82	38 52 81	ghmsub	$$⊢\left(F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{GrpHom}{\mathrm{Poly}}_1\left(K\right)\right)\wedge R{\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 1_{{\mathrm{Poly}}_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(\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)=F\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(K\right)}F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)$$
83	80 48 51 82	syl3anc	$$⊢\phi \to F\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)=F\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(K\right)}F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)$$
84	83	fveq2d	$$⊢\phi \to H\left(F\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)=H\left(F\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(K\right)}F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\right)$$
85		eqid	$$⊢{\mathrm{eval}}_1\left(K\right)={\mathrm{eval}}_1\left(K\right)$$
86		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
87	85 68 22 86 13 25 6	evl1maprhm	$$⊢\phi \to H\in \left({\mathrm{Poly}}_1\left(K\right)\mathrm{RingHom}K\right)$$
88		rhmghm	$$⊢H\in \left({\mathrm{Poly}}_1\left(K\right)\mathrm{RingHom}K\right)\to H\in \left({\mathrm{Poly}}_1\left(K\right)\mathrm{GrpHom}K\right)$$
89	87 88	syl	$$⊢\phi \to H\in \left({\mathrm{Poly}}_1\left(K\right)\mathrm{GrpHom}K\right)$$
90	38 86	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)}$$
91	78 90	syl	$$⊢\phi \to F:{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}⟶{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
92	91 48	ffvelcdmd	$$⊢\phi \to F\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
93	91 51	ffvelcdmd	$$⊢\phi \to F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
94		eqid	$$⊢{-}_K={-}_K$$
95	86 81 94	ghmsub	$$⊢\left(H\in \left({\mathrm{Poly}}_1\left(K\right)\mathrm{GrpHom}K\right)\wedge F\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)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\right)\to H\left(F\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(K\right)}F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\right)=H\left(F\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)\right){-}_{K}H\left(F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\right)$$
96	89 92 93 95	syl3anc	$$⊢\phi \to H\left(F\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(K\right)}F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\right)=H\left(F\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)\right){-}_{K}H\left(F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\right)$$
97		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}={\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
98	38 97 49 41 48	ringlidmd	$$⊢\phi \to 1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}{\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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)=R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
99	98	eqcomd	$$⊢\phi \to R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)=1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}{\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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)$$
100	32	elexd	$$⊢\phi \to \mathbb{Z}/N\mathbb{Z}\in \mathrm{V}$$
101	33	ply1sca	$$⊢\mathbb{Z}/N\mathbb{Z}\in \mathrm{V}\to \mathbb{Z}/N\mathbb{Z}=\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)$$
102	100 101	syl	$$⊢\phi \to \mathbb{Z}/N\mathbb{Z}=\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)$$
103	102	fveq2d	$$⊢\phi \to 1_{\mathbb{Z}/N\mathbb{Z}}=1_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)}$$
104	103	fveq2d	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(1_{\mathbb{Z}/N\mathbb{Z}}\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(1_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)}\right)$$
105		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)$$
106		eqid	$$⊢\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)=\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)$$
107	33	ply1lmod	$$⊢\mathbb{Z}/N\mathbb{Z}\in \mathrm{Ring}\to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{LMod}$$
108	44 107	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{LMod}$$
109	105 106 108 41	ascl1	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(1_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)}\right)=1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
110	104 109	eqtrd	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(1_{\mathbb{Z}/N\mathbb{Z}}\right)=1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
111	110	eqcomd	$$⊢\phi \to 1_{{\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(1_{\mathbb{Z}/N\mathbb{Z}}\right)$$
112	111	oveq1d	$$⊢\phi \to 1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}{\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(1_{\mathbb{Z}/N\mathbb{Z}}\right){\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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)$$
113	99 112	eqtrd	$$⊢\phi \to R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(1_{\mathbb{Z}/N\mathbb{Z}}\right){\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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)$$
114	33	ply1assa	$$⊢\mathbb{Z}/N\mathbb{Z}\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{AssAlg}$$
115	32 114	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{AssAlg}$$
116		eqid	$$⊢{\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}={\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}$$
117		eqid	$$⊢1_{\mathbb{Z}/N\mathbb{Z}}=1_{\mathbb{Z}/N\mathbb{Z}}$$
118	116 117	ringidcl	$$⊢\mathbb{Z}/N\mathbb{Z}\in \mathrm{Ring}\to 1_{\mathbb{Z}/N\mathbb{Z}}\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}$$
119	44 118	syl	$$⊢\phi \to 1_{\mathbb{Z}/N\mathbb{Z}}\in {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}$$
120	102	fveq2d	$$⊢\phi \to {\mathrm{Base}}_{\mathbb{Z}/N\mathbb{Z}}={\mathrm{Base}}_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)}$$
121	119 120	eleqtrd	$$⊢\phi \to 1_{\mathbb{Z}/N\mathbb{Z}}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)}$$
122		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)}$$
123		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}={\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}$$
124	105 106 122 38 97 123	asclmul1	$$⊢\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\in \mathrm{AssAlg}\wedge 1_{\mathbb{Z}/N\mathbb{Z}}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)}\wedge R{\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)}\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(1_{\mathbb{Z}/N\mathbb{Z}}\right){\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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)=1_{\mathbb{Z}/N\mathbb{Z}}{\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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)$$
125	115 121 48 124	syl3anc	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\right)\left(1_{\mathbb{Z}/N\mathbb{Z}}\right){\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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)=1_{\mathbb{Z}/N\mathbb{Z}}{\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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)$$
126	113 125	eqtrd	$$⊢\phi \to R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}}{\mathrm{var}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)=1_{\mathbb{Z}/N\mathbb{Z}}{\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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)$$
127	126	fveq2d	$$⊢\phi \to F\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)=F\left(1_{\mathbb{Z}/N\mathbb{Z}}{\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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)\right)$$
128		eqid	$$⊢{\mathrm{var}}_1\left(K\right)={\mathrm{var}}_1\left(K\right)$$
129		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}={\cdot }_{{\mathrm{Poly}}_1\left(K\right)}$$
130		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}$$
131		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
132	33 68 38 116 4 45 128 123 129 37 130 40 131 77 119 17	rhmply1mon	$$⊢\phi \to F\left(1_{\mathbb{Z}/N\mathbb{Z}}{\cdot }_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\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)\right)=G\left(1_{\mathbb{Z}/N\mathbb{Z}}\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)$$
133	127 132	eqtrd	$$⊢\phi \to F\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)=G\left(1_{\mathbb{Z}/N\mathbb{Z}}\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)$$
134	133	fveq2d	$$⊢\phi \to H\left(F\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)\right)=H\left(G\left(1_{\mathbb{Z}/N\mathbb{Z}}\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)$$
135		eqid	$$⊢1_K=1_K$$
136	117 135	rhm1	$$⊢G\in \left(\mathbb{Z}/N\mathbb{Z}\mathrm{RingHom}K\right)\to G\left(1_{\mathbb{Z}/N\mathbb{Z}}\right)=1_K$$
137	77 136	syl	$$⊢\phi \to G\left(1_{\mathbb{Z}/N\mathbb{Z}}\right)=1_K$$
138	137	oveq1d	$$⊢\phi \to G\left(1_{\mathbb{Z}/N\mathbb{Z}}\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)=1_K{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)$$
139	138	fveq2d	$$⊢\phi \to H\left(G\left(1_{\mathbb{Z}/N\mathbb{Z}}\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)=H\left(1_K{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)$$
140	68	ply1assa	$$⊢K\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{AssAlg}$$
141	13 140	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{AssAlg}$$
142	22 135	ringidcl	$$⊢K\in \mathrm{Ring}\to 1_K\in {\mathrm{Base}}_K$$
143	69 142	syl	$$⊢\phi \to 1_K\in {\mathrm{Base}}_K$$
144	68	ply1sca	$$⊢K\in \mathrm{Field}\to K=\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
145	1 144	syl	$$⊢\phi \to K=\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
146	145	fveq2d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(K\right)\right)}$$
147	143 146	eleqtrd	$$⊢\phi \to 1_K\in {\mathrm{Base}}_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(K\right)\right)}$$
148	130 86	mgpbas	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}$$
149	68	ply1crng	$$⊢K\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}$$
150	13 149	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}$$
151		crngring	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}$$
152	150 151	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}$$
153	130	ringmgp	$$⊢{\mathrm{Poly}}_1\left(K\right)\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}$$
154	152 153	syl	$$⊢\phi \to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}\in \mathrm{Mnd}$$
155	128 68 86	vr1cl	$$⊢K\in \mathrm{Ring}\to {\mathrm{var}}_1\left(K\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
156	69 155	syl	$$⊢\phi \to {\mathrm{var}}_1\left(K\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
157	148 131 154 17 156	mulgnn0cld	$$⊢\phi \to R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
158		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
159		eqid	$$⊢\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(K\right)\right)=\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(K\right)\right)$$
160		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(K\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(K\right)\right)}$$
161		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}={\cdot }_{{\mathrm{Poly}}_1\left(K\right)}$$
162	158 159 160 86 161 129	asclmul1	$$⊢\left({\mathrm{Poly}}_1\left(K\right)\in \mathrm{AssAlg}\wedge 1_K\in {\mathrm{Base}}_{\mathrm{Scalar}\left({\mathrm{Poly}}_1\left(K\right)\right)}\wedge R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(1_K\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)=1_K{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)$$
163	141 147 157 162	syl3anc	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(1_K\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)=1_K{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)$$
164	163	eqcomd	$$⊢\phi \to 1_K{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(1_K\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)$$
165	164	fveq2d	$$⊢\phi \to H\left(1_K{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)=H\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(1_K\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)$$
166		eqid	$$⊢1_{{\mathrm{Poly}}_1\left(K\right)}=1_{{\mathrm{Poly}}_1\left(K\right)}$$
167	68 158 135 166 69	ply1ascl1	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(1_K\right)=1_{{\mathrm{Poly}}_1\left(K\right)}$$
168	167	oveq1d	$$⊢\phi \to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(1_K\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)=1_{{\mathrm{Poly}}_1\left(K\right)}{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)$$
169	168	fveq2d	$$⊢\phi \to H\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(1_K\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)=H\left(1_{{\mathrm{Poly}}_1\left(K\right)}{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)$$
170	86 161 166 152 157	ringlidmd	$$⊢\phi \to 1_{{\mathrm{Poly}}_1\left(K\right)}{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)=R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)$$
171	170	fveq2d	$$⊢\phi \to H\left(1_{{\mathrm{Poly}}_1\left(K\right)}{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)=H\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)$$
172	6	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)$$
173		simpr	$$⊢\left(\phi \wedge r=R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\to r=R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)$$
174	173	fveq2d	$$⊢\left(\phi \wedge r=R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\to {\mathrm{eval}}_1\left(K\right)\left(r\right)={\mathrm{eval}}_1\left(K\right)\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)$$
175	174	fveq1d	$$⊢\left(\phi \wedge r=R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\to {\mathrm{eval}}_1\left(K\right)\left(r\right)\left(M\right)={\mathrm{eval}}_1\left(K\right)\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\left(M\right)$$
176		fvexd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\left(M\right)\in \mathrm{V}$$
177	172 175 157 176	fvmptd	$$⊢\phi \to H\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)={\mathrm{eval}}_1\left(K\right)\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\left(M\right)$$
178	85 128 22 68 86 13 25	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)$$
179	85 68 22 86 13 25 178 131 18 17	evl1expd	$$⊢\phi \to \left(R{\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(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\left(M\right)=R{\cdot }_{{\mathrm{mulGrp}}_K}M\right)$$
180	179	simprd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\left(M\right)=R{\cdot }_{{\mathrm{mulGrp}}_K}M$$
181	20	simp2d	$$⊢\phi \to R{\cdot }_{{\mathrm{mulGrp}}_K}M=0_{{\mathrm{mulGrp}}_K}$$
182	14 135	ringidval	$$⊢1_K=0_{{\mathrm{mulGrp}}_K}$$
183	182	eqcomi	$$⊢0_{{\mathrm{mulGrp}}_K}=1_K$$
184	183	a1i	$$⊢\phi \to 0_{{\mathrm{mulGrp}}_K}=1_K$$
185	181 184	eqtrd	$$⊢\phi \to R{\cdot }_{{\mathrm{mulGrp}}_K}M=1_K$$
186	180 185	eqtrd	$$⊢\phi \to {\mathrm{eval}}_1\left(K\right)\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\left(M\right)=1_K$$
187	177 186	eqtrd	$$⊢\phi \to H\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)=1_K$$
188	171 187	eqtrd	$$⊢\phi \to H\left(1_{{\mathrm{Poly}}_1\left(K\right)}{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)=1_K$$
189	169 188	eqtrd	$$⊢\phi \to H\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(1_K\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)=1_K$$
190	165 189	eqtrd	$$⊢\phi \to H\left(1_K{\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)=1_K$$
191	139 190	eqtrd	$$⊢\phi \to H\left(G\left(1_{\mathbb{Z}/N\mathbb{Z}}\right){\cdot }_{{\mathrm{Poly}}_1\left(K\right)}\left(R{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}{\mathrm{var}}_1\left(K\right)\right)\right)=1_K$$
192	134 191	eqtrd	$$⊢\phi \to H\left(F\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)\right)=1_K$$
193	166 135	rhm1	$$⊢H\in \left({\mathrm{Poly}}_1\left(K\right)\mathrm{RingHom}K\right)\to H\left(1_{{\mathrm{Poly}}_1\left(K\right)}\right)=1_K$$
194	87 193	syl	$$⊢\phi \to H\left(1_{{\mathrm{Poly}}_1\left(K\right)}\right)=1_K$$
195	194	eqcomd	$$⊢\phi \to 1_K=H\left(1_{{\mathrm{Poly}}_1\left(K\right)}\right)$$
196	192 195	eqtrd	$$⊢\phi \to H\left(F\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)\right)=H\left(1_{{\mathrm{Poly}}_1\left(K\right)}\right)$$
197	196 194	eqtrd	$$⊢\phi \to H\left(F\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)\right)=1_K$$
198	49 166	rhm1	$$⊢F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}{\mathrm{Poly}}_1\left(K\right)\right)\to F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)=1_{{\mathrm{Poly}}_1\left(K\right)}$$
199	78 198	syl	$$⊢\phi \to F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)=1_{{\mathrm{Poly}}_1\left(K\right)}$$
200	199	fveq2d	$$⊢\phi \to H\left(F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\right)=H\left(1_{{\mathrm{Poly}}_1\left(K\right)}\right)$$
201	200 194	eqtrd	$$⊢\phi \to H\left(F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\right)=1_K$$
202	197 201	oveq12d	$$⊢\phi \to H\left(F\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)\right){-}_{K}H\left(F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\right)=1_K{-}_K{1}_K$$
203	69	ringgrpd	$$⊢\phi \to K\in \mathrm{Grp}$$
204	22 12 94	grpsubid	$$⊢\left(K\in \mathrm{Grp}\wedge 1_K\in {\mathrm{Base}}_K\right)\to 1_K{-}_K{1}_K=0_K$$
205	203 143 204	syl2anc	$$⊢\phi \to 1_K{-}_K{1}_K=0_K$$
206	202 205	eqtrd	$$⊢\phi \to H\left(F\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)\right){-}_{K}H\left(F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\right)=0_K$$
207	96 206	eqtrd	$$⊢\phi \to H\left(F\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(K\right)}F\left(1_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}\right)\right)=0_K$$
208	84 207	eqtrd	$$⊢\phi \to H\left(F\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)=0_K$$
209	67 208	eqtrd	$$⊢\phi \to \left(H\circ F\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)=0_K$$
210	12 26 27 9 8 35 10 54 209	rhmqusspan	$$⊢\phi \to \left(I\in \left(A\mathrm{RingHom}K\right)\wedge \forall g\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)}I\left(\left[g\right]\left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right){~}_{\mathit{QG}}L\right)\right)=\left(H\circ F\right)\left(g\right)\right)$$