Theorem aks5lem1

Description: Section 5 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf. Construction of a ring homomorphism out of Zn X to K. (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)$$
	aks5lem1.7	$$⊢\phi \to M\in {\mathrm{Base}}_K$$
Assertion	aks5lem1	$$⊢\phi \to H\circ F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}K\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		aks5lem1.7	$$⊢\phi \to M\in {\mathrm{Base}}_K$$
8		eqid	$$⊢{\mathrm{eval}}_1\left(K\right)={\mathrm{eval}}_1\left(K\right)$$
9		eqid	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(K\right)$$
10		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
11		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
12	1	fldcrngd	$$⊢\phi \to K\in \mathrm{CRing}$$
13	8 9 10 11 12 7 6	evl1maprhm	$$⊢\phi \to H\in \left({\mathrm{Poly}}_1\left(K\right)\mathrm{RingHom}K\right)$$
14		eqid	$$⊢{\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)={\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)$$
15		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)}$$
16		crngring	$$⊢K\in \mathrm{CRing}\to K\in \mathrm{Ring}$$
17	12 16	syl	$$⊢\phi \to K\in \mathrm{Ring}$$
18	3	simp2d	$$⊢\phi \to N\in \mathbb{N}$$
19	2	eqcomi	$$⊢\mathrm{chr}\left(K\right)=P$$
20	3	simp1d	$$⊢\phi \to P\in \mathbb{P}$$
21		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
22	20 21	syl	$$⊢\phi \to P\in \mathbb{N}$$
23	22	nnzd	$$⊢\phi \to P\in \mathbb{Z}$$
24	19 23	eqeltrid	$$⊢\phi \to \mathrm{chr}\left(K\right)\in \mathbb{Z}$$
25	3	simp3d	$$⊢\phi \to P\parallel N$$
26	19 25	eqbrtrid	$$⊢\phi \to \mathrm{chr}\left(K\right)\parallel N$$
27		eqid	$$⊢\mathbb{Z}/N\mathbb{Z}=\mathbb{Z}/N\mathbb{Z}$$
28	17 18 24 26 27 5	zndvdchrrhm	$$⊢\phi \to G\in \left(\mathbb{Z}/N\mathbb{Z}\mathrm{RingHom}K\right)$$
29	14 9 15 4 28	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)$$
30		rhmco	$$⊢\left(H\in \left({\mathrm{Poly}}_1\left(K\right)\mathrm{RingHom}K\right)\wedge F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}{\mathrm{Poly}}_1\left(K\right)\right)\right)\to H\circ F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}K\right)$$
31	13 29 30	syl2anc	$$⊢\phi \to H\circ F\in \left({\mathrm{Poly}}_1\left(\mathbb{Z}/N\mathbb{Z}\right)\mathrm{RingHom}K\right)$$