Theorem aks6d1c6lem5

Description: Eliminate the size hypothesis. Claim 6. (Contributed by metakunt, 15-May-2025)

	Ref	Expression
Hypotheses	aks6d1c6lem5.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \forall y\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(y\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}y\right)\right)\right\}$$
	aks6d1c6lem5.2	$$⊢P=\mathrm{chr}\left(K\right)$$
	aks6d1c6lem5.3	$$⊢\phi \to K\in \mathrm{Field}$$
	aks6d1c6lem5.4	$$⊢\phi \to P\in \mathbb{P}$$
	aks6d1c6lem5.5	$$⊢\phi \to R\in \mathbb{N}$$
	aks6d1c6lem5.6	$$⊢\phi \to N\in \mathbb{N}$$
	aks6d1c6lem5.7	$$⊢\phi \to P\parallel N$$
	aks6d1c6lem5.8	$$⊢\phi \to N\gcd R=1$$
	aks6d1c6lem5.9	$$⊢\phi \to \forall b\in \left(1\dots A\right)b\gcd N=1$$
	aks6d1c6lem5.10	$$⊢G=\left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)$$
	aks6d1c6lem5.11	$$⊢A=⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
	aksaks6dlem5.12	$$⊢E=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
	aks6d1c6lem5.13	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)$$
	aks6d1c6lem5.14	$$⊢\phi \to \forall a\in \left(1\dots A\right)N\underset{\dot{}}{\sim }\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(a\right)\right)\right)$$
	aks6d1c6lem5.15	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K⟼P{\cdot }_{{\mathrm{mulGrp}}_K}x\right)\in \left(K\mathrm{RingIso}K\right)$$
	aks6d1c6lem5.16	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
	aks6d1c6lem5.17	$$⊢H=\left(h\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼{\mathrm{eval}}_1\left(K\right)\left(G\left(h\right)\right)\left(M\right)\right)$$
	aks6d1c6lem5.18	$$⊢D=\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
	aks6d1c6lem5.19	$$⊢S=\left\{s\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)|\sum _{t=0}^{A}s\left(t\right)\le D-1\right\}$$
	aks6d1c6lem5.20	$$⊢J=\left(j\in \mathbb{Z}⟼j{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)$$
	aks6d1c6lem5.22	$$⊢U=\left\{m\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_K}|\exists n\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_K}n{+}_{{\mathrm{mulGrp}}_K}m=0_{{\mathrm{mulGrp}}_K}\right\}$$
	aks6d1c6lem5.23	$$⊢X=\left(b\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}⟼\bigcup J\left[b\right]\right)$$
Assertion	aks6d1c6lem5	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{D+A}{D-1}\right)\le \left|H\left[{{\mathbb{N}}_0}^{\left(0\dots A\right)}\right]\right|$$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c6lem5.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \forall y\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(y\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}y\right)\right)\right\}$$
2		aks6d1c6lem5.2	$$⊢P=\mathrm{chr}\left(K\right)$$
3		aks6d1c6lem5.3	$$⊢\phi \to K\in \mathrm{Field}$$
4		aks6d1c6lem5.4	$$⊢\phi \to P\in \mathbb{P}$$
5		aks6d1c6lem5.5	$$⊢\phi \to R\in \mathbb{N}$$
6		aks6d1c6lem5.6	$$⊢\phi \to N\in \mathbb{N}$$
7		aks6d1c6lem5.7	$$⊢\phi \to P\parallel N$$
8		aks6d1c6lem5.8	$$⊢\phi \to N\gcd R=1$$
9		aks6d1c6lem5.9	$$⊢\phi \to \forall b\in \left(1\dots A\right)b\gcd N=1$$
10		aks6d1c6lem5.10	$$⊢G=\left(g\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼\underset{i=0}{\overset{A}{{\sum }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}}}\left(g\left(i\right){\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(K\right)}}\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(i\right)\right)\right)\right)\right)$$
11		aks6d1c6lem5.11	$$⊢A=⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
12		aksaks6dlem5.12	$$⊢E=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
13		aks6d1c6lem5.13	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(\mathbb{Z}/R\mathbb{Z}\right)$$
14		aks6d1c6lem5.14	$$⊢\phi \to \forall a\in \left(1\dots A\right)N\underset{\dot{}}{\sim }\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(a\right)\right)\right)$$
15		aks6d1c6lem5.15	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K⟼P{\cdot }_{{\mathrm{mulGrp}}_K}x\right)\in \left(K\mathrm{RingIso}K\right)$$
16		aks6d1c6lem5.16	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
17		aks6d1c6lem5.17	$$⊢H=\left(h\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)⟼{\mathrm{eval}}_1\left(K\right)\left(G\left(h\right)\right)\left(M\right)\right)$$
18		aks6d1c6lem5.18	$$⊢D=\left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
19		aks6d1c6lem5.19	$$⊢S=\left\{s\in \left({{\mathbb{N}}_0}^{\left(0\dots A\right)}\right)|\sum _{t=0}^{A}s\left(t\right)\le D-1\right\}$$
20		aks6d1c6lem5.20	$$⊢J=\left(j\in \mathbb{Z}⟼j{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)$$
21		aks6d1c6lem5.22	$$⊢U=\left\{m\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_K}|\exists n\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_K}n{+}_{{\mathrm{mulGrp}}_K}m=0_{{\mathrm{mulGrp}}_K}\right\}$$
22		aks6d1c6lem5.23	$$⊢X=\left(b\in {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}⟼\bigcup J\left[b\right]\right)$$
23		eqid	$$⊢0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}=0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}$$
24	3	fldcrngd	$$⊢\phi \to K\in \mathrm{CRing}$$
25		eqid	$$⊢{\mathrm{mulGrp}}_K={\mathrm{mulGrp}}_K$$
26	25	crngmgp	$$⊢K\in \mathrm{CRing}\to {\mathrm{mulGrp}}_K\in \mathrm{CMnd}$$
27	24 26	syl	$$⊢\phi \to {\mathrm{mulGrp}}_K\in \mathrm{CMnd}$$
28	27 5 21 20 16	aks6d1c6isolem2	$$⊢\phi \to J\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)\right)$$
29		eqid	$$⊢J^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]=J^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]$$
30		eqid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)$$
31		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
32		nfcv	$$⊢\underset{\_}{Ⅎ}c\left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)$$
33		nfcv	$$⊢\underset{\_}{Ⅎ}d\left[c\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)$$
34		eceq1	$$⊢d=c\to \left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)=\left[c\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)$$
35	32 33 34	cbvmpt	$$⊢\left(d\in \mathbb{Z}⟼\left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)=\left(c\in \mathbb{Z}⟼\left[c\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)$$
36	23 28 29 30 22 31 35	ghmquskerco	$$⊢\phi \to J=X\circ \left(d\in \mathbb{Z}⟼\left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)$$
37		eqid	$$⊢\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
38	27 5 21 20 16 37	aks6d1c6isolem3	$$⊢\phi \to \mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)=J^{-1}\left[\left\{0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\right\}\right]$$
39	27 5 21	primrootsunit	$$⊢\phi \to \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R=\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)\mathrm{PrimRoots}R\wedge {\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\in \mathrm{Abel}\right)$$
40	39	simprd	$$⊢\phi \to {\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\in \mathrm{Abel}$$
41	40	ablgrpd	$$⊢\phi \to {\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\in \mathrm{Grp}$$
42	41	grpmndd	$$⊢\phi \to {\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\in \mathrm{Mnd}$$
43		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
44		simpr	$$⊢\left(\phi \wedge w=0\right)\to w=0$$
45	44	fveqeq2d	$$⊢\left(\phi \wedge w=0\right)\to \left(J\left(w\right)=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\leftrightarrow J\left(0\right)=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\right)$$
46	20	a1i	$$⊢\phi \to J=\left(j\in \mathbb{Z}⟼j{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)$$
47		simpr	$$⊢\left(\phi \wedge j=0\right)\to j=0$$
48	47	oveq1d	$$⊢\left(\phi \wedge j=0\right)\to j{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M$$
49	39	simpld	$$⊢\phi \to {\mathrm{mulGrp}}_K\mathrm{PrimRoots}R=\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)\mathrm{PrimRoots}R$$
50	16 49	eleqtrd	$$⊢\phi \to M\in \left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)\mathrm{PrimRoots}R\right)$$
51	40	ablcmnd	$$⊢\phi \to {\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\in \mathrm{CMnd}$$
52	5	nnnn0d	$$⊢\phi \to R\in {\mathbb{N}}_0$$
53		eqid	$$⊢{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}={\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
54	51 52 53	isprimroot	$$⊢\phi \to \left(M\in \left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)\mathrm{PrimRoots}R\right)\leftrightarrow \left(M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\wedge R{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\wedge \forall l\in {\mathbb{N}}_0\left(l{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\to R\parallel l\right)\right)\right)$$
55	54	biimpd	$$⊢\phi \to \left(M\in \left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)\mathrm{PrimRoots}R\right)\to \left(M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\wedge R{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\wedge \forall l\in {\mathbb{N}}_0\left(l{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\to R\parallel l\right)\right)\right)$$
56	50 55	mpd	$$⊢\phi \to \left(M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\wedge R{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\wedge \forall l\in {\mathbb{N}}_0\left(l{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\to R\parallel l\right)\right)$$
57	56	simp1d	$$⊢\phi \to M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
58		eqid	$$⊢{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
59		eqid	$$⊢0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
60	58 59 53	mulg0	$$⊢M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\to 0{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
61	57 60	syl	$$⊢\phi \to 0{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
62	61	adantr	$$⊢\left(\phi \wedge j=0\right)\to 0{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
63	48 62	eqtrd	$$⊢\left(\phi \wedge j=0\right)\to j{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
64		fvexd	$$⊢\phi \to 0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\in \mathrm{V}$$
65	46 63 43 64	fvmptd	$$⊢\phi \to J\left(0\right)=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
66	43 45 65	rspcedvd	$$⊢\phi \to \exists w\in \mathbb{Z}J\left(w\right)=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
67	41	adantr	$$⊢\left(\phi \wedge j\in \mathbb{Z}\right)\to {\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\in \mathrm{Grp}$$
68		simpr	$$⊢\left(\phi \wedge j\in \mathbb{Z}\right)\to j\in \mathbb{Z}$$
69	57	adantr	$$⊢\left(\phi \wedge j\in \mathbb{Z}\right)\to M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
70	58 53 67 68 69	mulgcld	$$⊢\left(\phi \wedge j\in \mathbb{Z}\right)\to j{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
71	70 20	fmptd	$$⊢\phi \to J:\mathbb{Z}⟶{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
72	71	ffnd	$$⊢\phi \to JFn\mathbb{Z}$$
73		fvelrnb	$$⊢JFn\mathbb{Z}\to \left(0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\in \mathrm{ran}J\leftrightarrow \exists w\in \mathbb{Z}J\left(w\right)=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\right)$$
74	72 73	syl	$$⊢\phi \to \left(0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\in \mathrm{ran}J\leftrightarrow \exists w\in \mathbb{Z}J\left(w\right)=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\right)$$
75	66 74	mpbird	$$⊢\phi \to 0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\in \mathrm{ran}J$$
76	71	frnd	$$⊢\phi \to \mathrm{ran}J\subseteq {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
77		eqid	$$⊢\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J=\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J$$
78	77 58 59	ress0g	$$⊢\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\in \mathrm{Mnd}\wedge 0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\in \mathrm{ran}J\wedge \mathrm{ran}J\subseteq {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\right)\to 0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}=0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}$$
79	42 75 76 78	syl3anc	$$⊢\phi \to 0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}=0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}$$
80	79	sneqd	$$⊢\phi \to \left\{0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\right\}=\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}$$
81	80	imaeq2d	$$⊢\phi \to J^{-1}\left[\left\{0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\right\}\right]=J^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]$$
82	38 81	eqtr2d	$$⊢\phi \to J^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)$$
83	82	oveq2d	$$⊢\phi \to {\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]={\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)$$
84	83	eceq2d	$$⊢\phi \to \left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)=\left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)$$
85	84	mpteq2dv	$$⊢\phi \to \left(d\in \mathbb{Z}⟼\left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)=\left(d\in \mathbb{Z}⟼\left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)\right)$$
86		eqid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)={\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)$$
87		eqid	$$⊢\mathbb{Z}/R\mathbb{Z}=\mathbb{Z}/R\mathbb{Z}$$
88	37 86 87 13	znzrh2	$$⊢R\in {\mathbb{N}}_0\to L=\left(d\in \mathbb{Z}⟼\left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)\right)$$
89	52 88	syl	$$⊢\phi \to L=\left(d\in \mathbb{Z}⟼\left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)\right)$$
90	89	eqcomd	$$⊢\phi \to \left(d\in \mathbb{Z}⟼\left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)\right)=L$$
91	85 90	eqtrd	$$⊢\phi \to \left(d\in \mathbb{Z}⟼\left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)=L$$
92	91	coeq2d	$$⊢\phi \to X\circ \left(d\in \mathbb{Z}⟼\left[d\right]\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)=X\circ L$$
93	36 92	eqtrd	$$⊢\phi \to J=X\circ L$$
94	93	coeq2d	$$⊢\phi \to X^{-1}\circ J=X^{-1}\circ \left(X\circ L\right)$$
95		coass	$$⊢\left(X^{-1}\circ X\right)\circ L=X^{-1}\circ \left(X\circ L\right)$$
96	95	eqcomi	$$⊢X^{-1}\circ \left(X\circ L\right)=\left(X^{-1}\circ X\right)\circ L$$
97	94 96	eqtrdi	$$⊢\phi \to X^{-1}\circ J=\left(X^{-1}\circ X\right)\circ L$$
98	77 58	ressbas2	$$⊢\mathrm{ran}J\subseteq {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\to \mathrm{ran}J={\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}$$
99	76 98	syl	$$⊢\phi \to \mathrm{ran}J={\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}$$
100	23 28 29 30 22 99	ghmqusker	$$⊢\phi \to X\in \left(\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)\mathrm{GrpIso}\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)\right)$$
101		eqid	$$⊢{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}={\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}$$
102		eqid	$$⊢{\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}={\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}$$
103	101 102	gimf1o	$$⊢X\in \left(\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)\mathrm{GrpIso}\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)\right)\to X:{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}\underset{1-1\; onto}{⟶}{\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}$$
104	100 103	syl	$$⊢\phi \to X:{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}\underset{1-1\; onto}{⟶}{\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}$$
105		f1ococnv1	$$⊢X:{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}\underset{1-1\; onto}{⟶}{\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\to X^{-1}\circ X={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}}$$
106	104 105	syl	$$⊢\phi \to X^{-1}\circ X={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}}$$
107	106	coeq1d	$$⊢\phi \to \left(X^{-1}\circ X\right)\circ L=\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}}\right)\circ L$$
108	87	zncrng	$$⊢R\in {\mathbb{N}}_0\to \mathbb{Z}/R\mathbb{Z}\in \mathrm{CRing}$$
109	52 108	syl	$$⊢\phi \to \mathbb{Z}/R\mathbb{Z}\in \mathrm{CRing}$$
110		crngring	$$⊢\mathbb{Z}/R\mathbb{Z}\in \mathrm{CRing}\to \mathbb{Z}/R\mathbb{Z}\in \mathrm{Ring}$$
111	13	zrhrhm	$$⊢\mathbb{Z}/R\mathbb{Z}\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}\mathbb{Z}/R\mathbb{Z}\right)$$
112		eqid	$$⊢{\mathrm{Base}}_{\mathbb{Z}/R\mathbb{Z}}={\mathrm{Base}}_{\mathbb{Z}/R\mathbb{Z}}$$
113	31 112	rhmf	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}\mathbb{Z}/R\mathbb{Z}\right)\to L:\mathbb{Z}⟶{\mathrm{Base}}_{\mathbb{Z}/R\mathbb{Z}}$$
114	109 110 111 113	4syl	$$⊢\phi \to L:\mathbb{Z}⟶{\mathrm{Base}}_{\mathbb{Z}/R\mathbb{Z}}$$
115		eqid	$$⊢{\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)$$
116	37 115 87	znbas2	$$⊢R\in {\mathbb{N}}_0\to {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)\right)}={\mathrm{Base}}_{\mathbb{Z}/R\mathbb{Z}}$$
117	52 116	syl	$$⊢\phi \to {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)\right)}={\mathrm{Base}}_{\mathbb{Z}/R\mathbb{Z}}$$
118	117	feq3d	$$⊢\phi \to \left(L:\mathbb{Z}⟶{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)\right)}\leftrightarrow L:\mathbb{Z}⟶{\mathrm{Base}}_{\mathbb{Z}/R\mathbb{Z}}\right)$$
119	114 118	mpbird	$$⊢\phi \to L:\mathbb{Z}⟶{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)\right)}$$
120	82	eqcomd	$$⊢\phi \to \mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)=J^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]$$
121	120	oveq2d	$$⊢\phi \to {\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)={\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]$$
122	121	oveq2d	$$⊢\phi \to {\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)$$
123	122	fveq2d	$$⊢\phi \to {\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)\right)}={\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}$$
124	123	feq3d	$$⊢\phi \to \left(L:\mathbb{Z}⟶{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(\left\{R\right\}\right)\right)\right)}\leftrightarrow L:\mathbb{Z}⟶{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}\right)$$
125	119 124	mpbid	$$⊢\phi \to L:\mathbb{Z}⟶{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}$$
126		fcoi2	$$⊢L:\mathbb{Z}⟶{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}\to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}}\right)\circ L=L$$
127	125 126	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}}\right)\circ L=L$$
128	107 127	eqtrd	$$⊢\phi \to \left(X^{-1}\circ X\right)\circ L=L$$
129	97 128	eqtr2d	$$⊢\phi \to L=X^{-1}\circ J$$
130	129	imaeq1d	$$⊢\phi \to L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]=\left(X^{-1}\circ J\right)\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]$$
131		imaco	$$⊢\left(X^{-1}\circ J\right)\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]=X^{-1}\left[J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right]$$
132	131	a1i	$$⊢\phi \to \left(X^{-1}\circ J\right)\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]=X^{-1}\left[J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right]$$
133	130 132	eqtrd	$$⊢\phi \to L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]=X^{-1}\left[J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right]$$
134	133	fveq2d	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|=\left|X^{-1}\left[J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right]\right|$$
135		simplll	$$⊢\left(\left(\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\wedge u\in \mathbb{Z}\right)\wedge J\left(u\right)=w\right)\to \phi$$
136		simplr	$$⊢\left(\left(\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\wedge u\in \mathbb{Z}\right)\wedge J\left(u\right)=w\right)\to u\in \mathbb{Z}$$
137	135 136	jca	$$⊢\left(\left(\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\wedge u\in \mathbb{Z}\right)\wedge J\left(u\right)=w\right)\to \left(\phi \wedge u\in \mathbb{Z}\right)$$
138		simplr	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to z\in \left(0\dots R-1\right)$$
139		simpr	$$⊢\left(\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\wedge v=z\right)\to v=z$$
140	139	fveqeq2d	$$⊢\left(\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\wedge v=z\right)\to \left(J\left(v\right)=J\left(u\right)\leftrightarrow J\left(z\right)=J\left(u\right)\right)$$
141	20	a1i	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to J=\left(j\in \mathbb{Z}⟼j{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)$$
142		simpr	$$⊢\left(\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\wedge j=z\right)\to j=z$$
143	142	oveq1d	$$⊢\left(\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\wedge j=z\right)\to j{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M$$
144		fzssz	$$⊢\left(0\dots R-1\right)\subseteq \mathbb{Z}$$
145	144 138	sselid	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to z\in \mathbb{Z}$$
146		ovexd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\in \mathrm{V}$$
147	141 143 145 146	fvmptd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to J\left(z\right)=z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M$$
148		simpr	$$⊢\left(\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\wedge j=u\right)\to j=u$$
149	148	oveq1d	$$⊢\left(\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\wedge j=u\right)\to j{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=u{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M$$
150		simpr	$$⊢\left(\phi \wedge u\in \mathbb{Z}\right)\to u\in \mathbb{Z}$$
151	150	ad3antrrr	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to u\in \mathbb{Z}$$
152		ovexd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to u{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\in \mathrm{V}$$
153	141 149 151 152	fvmptd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to J\left(u\right)=u{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M$$
154		simpr	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to u=yR+z$$
155	154	oveq1d	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to u{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=\left(yR+z\right){\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M$$
156	41	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to {\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\in \mathrm{Grp}$$
157		simplr	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to y\in \mathbb{Z}$$
158	5	adantr	$$⊢\left(\phi \wedge u\in \mathbb{Z}\right)\to R\in \mathbb{N}$$
159	158	ad2antrr	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to R\in \mathbb{N}$$
160	159	nnzd	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to R\in \mathbb{Z}$$
161	157 160	zmulcld	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to yR\in \mathbb{Z}$$
162	144	sseli	$$⊢z\in \left(0\dots R-1\right)\to z\in \mathbb{Z}$$
163	162	adantl	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to z\in \mathbb{Z}$$
164	57	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
165	161 163 164	3jca	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to \left(yR\in \mathbb{Z}\wedge z\in \mathbb{Z}\wedge M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\right)$$
166		eqid	$$⊢{+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}={+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
167	58 53 166	mulgdir	$$⊢\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\in \mathrm{Grp}\wedge \left(yR\in \mathbb{Z}\wedge z\in \mathbb{Z}\wedge M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\right)\right)\to \left(yR+z\right){\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=\left(yR{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right){+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\left(z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)$$
168	156 165 167	syl2anc	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to \left(yR+z\right){\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=\left(yR{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right){+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\left(z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)$$
169	157 160 164	3jca	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to \left(y\in \mathbb{Z}\wedge R\in \mathbb{Z}\wedge M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\right)$$
170	58 53	mulgass	$$⊢\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\in \mathrm{Grp}\wedge \left(y\in \mathbb{Z}\wedge R\in \mathbb{Z}\wedge M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\right)\right)\to yR{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=y{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\left(R{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)$$
171	156 169 170	syl2anc	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to yR{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=y{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\left(R{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)$$
172	56	simp2d	$$⊢\phi \to R{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
173	172	adantr	$$⊢\left(\phi \wedge u\in \mathbb{Z}\right)\to R{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
174	173	adantr	$$⊢\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\to R{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
175	174	adantr	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to R{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
176	175	oveq2d	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to y{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\left(R{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)=y{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}{0}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
177	58 53 59	mulgz	$$⊢\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\in \mathrm{Grp}\wedge y\in \mathbb{Z}\right)\to y{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}{0}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
178	156 157 177	syl2anc	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to y{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}{0}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
179	176 178	eqtrd	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to y{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\left(R{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
180	171 179	eqtrd	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to yR{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
181	180	oveq1d	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to \left(yR{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right){+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\left(z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)=0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}{+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\left(z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)$$
182	58 53 156 163 164	mulgcld	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\in {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}$$
183	58 166 59 156 182	grplidd	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to 0_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}{+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\left(z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)=z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M$$
184	181 183	eqtrd	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to \left(yR{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right){+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}\left(z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M\right)=z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M$$
185	168 184	eqtrd	$$⊢\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\to \left(yR+z\right){\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M$$
186	185	adantr	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to \left(yR+z\right){\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M$$
187	155 186	eqtrd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to u{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M$$
188	153 187	eqtr2d	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to z{\cdot }_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right)}M=J\left(u\right)$$
189	147 188	eqtrd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to J\left(z\right)=J\left(u\right)$$
190	138 140 189	rspcedvd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \mathbb{Z}\right)\wedge y\in \mathbb{Z}\right)\wedge z\in \left(0\dots R-1\right)\right)\wedge u=yR+z\right)\to \exists v\in \left(0\dots R-1\right)J\left(v\right)=J\left(u\right)$$
191	150 158	remexz	$$⊢\left(\phi \wedge u\in \mathbb{Z}\right)\to \exists y\in \mathbb{Z}\exists z\in \left(0\dots R-1\right)u=yR+z$$
192	190 191	r19.29vva	$$⊢\left(\phi \wedge u\in \mathbb{Z}\right)\to \exists v\in \left(0\dots R-1\right)J\left(v\right)=J\left(u\right)$$
193	137 192	syl	$$⊢\left(\left(\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\wedge u\in \mathbb{Z}\right)\wedge J\left(u\right)=w\right)\to \exists v\in \left(0\dots R-1\right)J\left(v\right)=J\left(u\right)$$
194		simpr	$$⊢\left(\left(\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\wedge u\in \mathbb{Z}\right)\wedge J\left(u\right)=w\right)\to J\left(u\right)=w$$
195	194	eqcomd	$$⊢\left(\left(\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\wedge u\in \mathbb{Z}\right)\wedge J\left(u\right)=w\right)\to w=J\left(u\right)$$
196	195	eqeq2d	$$⊢\left(\left(\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\wedge u\in \mathbb{Z}\right)\wedge J\left(u\right)=w\right)\to \left(J\left(v\right)=w\leftrightarrow J\left(v\right)=J\left(u\right)\right)$$
197	196	rexbidv	$$⊢\left(\left(\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\wedge u\in \mathbb{Z}\right)\wedge J\left(u\right)=w\right)\to \left(\exists v\in \left(0\dots R-1\right)J\left(v\right)=w\leftrightarrow \exists v\in \left(0\dots R-1\right)J\left(v\right)=J\left(u\right)\right)$$
198	193 197	mpbird	$$⊢\left(\left(\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\wedge u\in \mathbb{Z}\right)\wedge J\left(u\right)=w\right)\to \exists v\in \left(0\dots R-1\right)J\left(v\right)=w$$
199		ssidd	$$⊢\phi \to \mathbb{Z}\subseteq \mathbb{Z}$$
200		fvelimab	$$⊢\left(JFn\mathbb{Z}\wedge \mathbb{Z}\subseteq \mathbb{Z}\right)\to \left(w\in J\left[\mathbb{Z}\right]\leftrightarrow \exists u\in \mathbb{Z}J\left(u\right)=w\right)$$
201	72 199 200	syl2anc	$$⊢\phi \to \left(w\in J\left[\mathbb{Z}\right]\leftrightarrow \exists u\in \mathbb{Z}J\left(u\right)=w\right)$$
202	201	biimpd	$$⊢\phi \to \left(w\in J\left[\mathbb{Z}\right]\to \exists u\in \mathbb{Z}J\left(u\right)=w\right)$$
203	202	imp	$$⊢\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\to \exists u\in \mathbb{Z}J\left(u\right)=w$$
204	198 203	r19.29a	$$⊢\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\to \exists v\in \left(0\dots R-1\right)J\left(v\right)=w$$
205	144	a1i	$$⊢\phi \to \left(0\dots R-1\right)\subseteq \mathbb{Z}$$
206		fvelimab	$$⊢\left(JFn\mathbb{Z}\wedge \left(0\dots R-1\right)\subseteq \mathbb{Z}\right)\to \left(w\in J\left[\left(0\dots R-1\right)\right]\leftrightarrow \exists v\in \left(0\dots R-1\right)J\left(v\right)=w\right)$$
207	72 205 206	syl2anc	$$⊢\phi \to \left(w\in J\left[\left(0\dots R-1\right)\right]\leftrightarrow \exists v\in \left(0\dots R-1\right)J\left(v\right)=w\right)$$
208	207	adantr	$$⊢\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\to \left(w\in J\left[\left(0\dots R-1\right)\right]\leftrightarrow \exists v\in \left(0\dots R-1\right)J\left(v\right)=w\right)$$
209	204 208	mpbird	$$⊢\left(\phi \wedge w\in J\left[\mathbb{Z}\right]\right)\to w\in J\left[\left(0\dots R-1\right)\right]$$
210	209	ex	$$⊢\phi \to \left(w\in J\left[\mathbb{Z}\right]\to w\in J\left[\left(0\dots R-1\right)\right]\right)$$
211	210	ssrdv	$$⊢\phi \to J\left[\mathbb{Z}\right]\subseteq J\left[\left(0\dots R-1\right)\right]$$
212	207	biimpd	$$⊢\phi \to \left(w\in J\left[\left(0\dots R-1\right)\right]\to \exists v\in \left(0\dots R-1\right)J\left(v\right)=w\right)$$
213	212	imp	$$⊢\left(\phi \wedge w\in J\left[\left(0\dots R-1\right)\right]\right)\to \exists v\in \left(0\dots R-1\right)J\left(v\right)=w$$
214	144	sseli	$$⊢v\in \left(0\dots R-1\right)\to v\in \mathbb{Z}$$
215	214	adantr	$$⊢\left(v\in \left(0\dots R-1\right)\wedge J\left(v\right)=w\right)\to v\in \mathbb{Z}$$
216	215	adantl	$$⊢\left(\left(\phi \wedge w\in J\left[\left(0\dots R-1\right)\right]\right)\wedge \left(v\in \left(0\dots R-1\right)\wedge J\left(v\right)=w\right)\right)\to v\in \mathbb{Z}$$
217		simprr	$$⊢\left(\left(\phi \wedge w\in J\left[\left(0\dots R-1\right)\right]\right)\wedge \left(v\in \left(0\dots R-1\right)\wedge J\left(v\right)=w\right)\right)\to J\left(v\right)=w$$
218	213 216 217	reximssdv	$$⊢\left(\phi \wedge w\in J\left[\left(0\dots R-1\right)\right]\right)\to \exists v\in \mathbb{Z}J\left(v\right)=w$$
219	72	adantr	$$⊢\left(\phi \wedge w\in J\left[\left(0\dots R-1\right)\right]\right)\to JFn\mathbb{Z}$$
220		ssidd	$$⊢\left(\phi \wedge w\in J\left[\left(0\dots R-1\right)\right]\right)\to \mathbb{Z}\subseteq \mathbb{Z}$$
221		fvelimab	$$⊢\left(JFn\mathbb{Z}\wedge \mathbb{Z}\subseteq \mathbb{Z}\right)\to \left(w\in J\left[\mathbb{Z}\right]\leftrightarrow \exists v\in \mathbb{Z}J\left(v\right)=w\right)$$
222	219 220 221	syl2anc	$$⊢\left(\phi \wedge w\in J\left[\left(0\dots R-1\right)\right]\right)\to \left(w\in J\left[\mathbb{Z}\right]\leftrightarrow \exists v\in \mathbb{Z}J\left(v\right)=w\right)$$
223	218 222	mpbird	$$⊢\left(\phi \wedge w\in J\left[\left(0\dots R-1\right)\right]\right)\to w\in J\left[\mathbb{Z}\right]$$
224	223	ex	$$⊢\phi \to \left(w\in J\left[\left(0\dots R-1\right)\right]\to w\in J\left[\mathbb{Z}\right]\right)$$
225	224	ssrdv	$$⊢\phi \to J\left[\left(0\dots R-1\right)\right]\subseteq J\left[\mathbb{Z}\right]$$
226	211 225	eqssd	$$⊢\phi \to J\left[\mathbb{Z}\right]=J\left[\left(0\dots R-1\right)\right]$$
227	72	fnfund	$$⊢\phi \to \mathrm{Fun}J$$
228		fzfid	$$⊢\phi \to \left(0\dots R-1\right)\in \mathrm{Fin}$$
229		imafi	$$⊢\left(\mathrm{Fun}J\wedge \left(0\dots R-1\right)\in \mathrm{Fin}\right)\to J\left[\left(0\dots R-1\right)\right]\in \mathrm{Fin}$$
230	227 228 229	syl2anc	$$⊢\phi \to J\left[\left(0\dots R-1\right)\right]\in \mathrm{Fin}$$
231	226 230	eqeltrd	$$⊢\phi \to J\left[\mathbb{Z}\right]\in \mathrm{Fin}$$
232	6 4 7 12	aks6d1c2p1	$$⊢\phi \to E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶\mathbb{N}$$
233		nnssz	$$⊢\mathbb{N}\subseteq \mathbb{Z}$$
234	233	a1i	$$⊢\phi \to \mathbb{N}\subseteq \mathbb{Z}$$
235	232 234	jca	$$⊢\phi \to \left(E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶\mathbb{N}\wedge \mathbb{N}\subseteq \mathbb{Z}\right)$$
236		fss	$$⊢\left(E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶\mathbb{N}\wedge \mathbb{N}\subseteq \mathbb{Z}\right)\to E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶\mathbb{Z}$$
237	235 236	syl	$$⊢\phi \to E:{\mathbb{N}}_0\times {\mathbb{N}}_0⟶\mathbb{Z}$$
238	237	frnd	$$⊢\phi \to \mathrm{ran}E\subseteq \mathbb{Z}$$
239	232	ffnd	$$⊢\phi \to EFn\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)$$
240		fnima	$$⊢EFn\left({\mathbb{N}}_0\times {\mathbb{N}}_0\right)\to E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]=\mathrm{ran}E$$
241	239 240	syl	$$⊢\phi \to E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]=\mathrm{ran}E$$
242	241	sseq1d	$$⊢\phi \to \left(E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\subseteq \mathbb{Z}\leftrightarrow \mathrm{ran}E\subseteq \mathbb{Z}\right)$$
243	238 242	mpbird	$$⊢\phi \to E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\subseteq \mathbb{Z}$$
244		imass2	$$⊢E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\subseteq \mathbb{Z}\to J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\subseteq J\left[\mathbb{Z}\right]$$
245	243 244	syl	$$⊢\phi \to J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\subseteq J\left[\mathbb{Z}\right]$$
246	231 245	ssfid	$$⊢\phi \to J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\in \mathrm{Fin}$$
247		dff1o2	$$⊢X:{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}\underset{1-1\; onto}{⟶}{\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\leftrightarrow \left(XFn{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}\wedge \mathrm{Fun}{X}^{-1}\wedge \mathrm{ran}X={\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right)$$
248	247	biimpi	$$⊢X:{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}\underset{1-1\; onto}{⟶}{\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\to \left(XFn{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}\wedge \mathrm{Fun}{X}^{-1}\wedge \mathrm{ran}X={\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right)$$
249	248	simp2d	$$⊢X:{\mathrm{Base}}_{\left({\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}{J}^{-1}\left[\left\{0_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\right\}\right]\right)\right)}\underset{1-1\; onto}{⟶}{\mathrm{Base}}_{\left(\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}U\right){\upharpoonright }_{𝑠}\mathrm{ran}J\right)}\to \mathrm{Fun}{X}^{-1}$$
250	104 249	syl	$$⊢\phi \to \mathrm{Fun}{X}^{-1}$$
251		imadomfi	$$⊢\left(J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\in \mathrm{Fin}\wedge \mathrm{Fun}{X}^{-1}\right)\to X^{-1}\left[J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right]\preccurlyeq J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]$$
252	246 250 251	syl2anc	$$⊢\phi \to X^{-1}\left[J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right]\preccurlyeq J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]$$
253		hashdomi	$$⊢X^{-1}\left[J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right]\preccurlyeq J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\to \left|X^{-1}\left[J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right]\right|\le \left|J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
254	252 253	syl	$$⊢\phi \to \left|X^{-1}\left[J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right]\right|\le \left|J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
255	134 254	eqbrtrd	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\le \left|J\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|$$
256	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 255 21	aks6d1c6lem4	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{D+A}{D-1}\right)\le \left|H\left[{{\mathbb{N}}_0}^{\left(0\dots A\right)}\right]\right|$$