Theorem hashscontpowcl

Description: Closure of E for https://www3.nd.edu/%7eandyp/notes/AKS.pdf Theorem 6.1. (Contributed by metakunt, 28-Apr-2025)

	Ref	Expression
Hypotheses	hashscontpowcl.1	$$⊢\phi \to N\in \mathbb{N}$$
	hashscontpowcl.2	$$⊢\phi \to P\in \mathbb{P}$$
	hashscontpowcl.3	$$⊢\phi \to P\parallel N$$
	hashscontpowcl.4	$$⊢\phi \to R\in \mathbb{N}$$
	hashscontpowcl.5	$$⊢\phi \to N\gcd R=1$$
	hashscontpowcl.6	$$⊢E=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
	hashscontpowcl.7	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
	hashscontpowcl.8	$$⊢Y=\mathbb{Z}/R\mathbb{Z}$$
Assertion	hashscontpowcl	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		hashscontpowcl.1	$$⊢\phi \to N\in \mathbb{N}$$
2		hashscontpowcl.2	$$⊢\phi \to P\in \mathbb{P}$$
3		hashscontpowcl.3	$$⊢\phi \to P\parallel N$$
4		hashscontpowcl.4	$$⊢\phi \to R\in \mathbb{N}$$
5		hashscontpowcl.5	$$⊢\phi \to N\gcd R=1$$
6		hashscontpowcl.6	$$⊢E=\left(k\in {\mathbb{N}}_0,l\in {\mathbb{N}}_0⟼P^k{\left(\frac{N}{P}\right)}^l\right)$$
7		hashscontpowcl.7	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
8		hashscontpowcl.8	$$⊢Y=\mathbb{Z}/R\mathbb{Z}$$
9		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
10	8 9	znfi	$$⊢R\in \mathbb{N}\to {\mathrm{Base}}_Y\in \mathrm{Fin}$$
11	4 10	syl	$$⊢\phi \to {\mathrm{Base}}_Y\in \mathrm{Fin}$$
12	4	nnnn0d	$$⊢\phi \to R\in {\mathbb{N}}_0$$
13	8	zncrng	$$⊢R\in {\mathbb{N}}_0\to Y\in \mathrm{CRing}$$
14	12 13	syl	$$⊢\phi \to Y\in \mathrm{CRing}$$
15		crngring	$$⊢Y\in \mathrm{CRing}\to Y\in \mathrm{Ring}$$
16	14 15	syl	$$⊢\phi \to Y\in \mathrm{Ring}$$
17	7	zrhrhm	$$⊢Y\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)$$
18		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
19	18 9	rhmf	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Y\right)\to L:\mathbb{Z}⟶{\mathrm{Base}}_Y$$
20		fimass	$$⊢L:\mathbb{Z}⟶{\mathrm{Base}}_Y\to L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\subseteq {\mathrm{Base}}_Y$$
21	16 17 19 20	4syl	$$⊢\phi \to L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\subseteq {\mathrm{Base}}_Y$$
22	11 21	ssfid	$$⊢\phi \to L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\in \mathrm{Fin}$$
23		hashcl	$$⊢L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\in \mathrm{Fin}\to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in {\mathbb{N}}_0$$
24	22 23	syl	$$⊢\phi \to \left|L\left[E\left[{\mathbb{N}}_0\times {\mathbb{N}}_0\right]\right]\right|\in {\mathbb{N}}_0$$