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	⊢ ( 𝜑 → 𝐾 ∈ Field )
	aks5lem1.2	⊢ 𝑃 = ( chr ‘ 𝐾 )
	aks5lem1.3	⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁 ) )
	aks5lem1.4	⊢ 𝐹 = ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( 𝐺 ∘ 𝑝 ) )
	aks5lem1.5	⊢ 𝐺 = ( 𝑞 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑞 ) )
	aks5lem1.6	⊢ 𝐻 = ( 𝑟 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑟 ) ‘ 𝑀 ) )
	aks5lem1.7	⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ 𝐾 ) )
Assertion	aks5lem1	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) RingHom 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		aks5lem1.1	⊢ ( 𝜑 → 𝐾 ∈ Field )
2		aks5lem1.2	⊢ 𝑃 = ( chr ‘ 𝐾 )
3		aks5lem1.3	⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁 ) )
4		aks5lem1.4	⊢ 𝐹 = ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( 𝐺 ∘ 𝑝 ) )
5		aks5lem1.5	⊢ 𝐺 = ( 𝑞 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑞 ) )
6		aks5lem1.6	⊢ 𝐻 = ( 𝑟 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑟 ) ‘ 𝑀 ) )
7		aks5lem1.7	⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ 𝐾 ) )
8		eqid	⊢ ( eval1 ‘ 𝐾 ) = ( eval1 ‘ 𝐾 )
9		eqid	⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ 𝐾 )
10		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
12	1	fldcrngd	⊢ ( 𝜑 → 𝐾 ∈ CRing )
13	8 9 10 11 12 7 6	evl1maprhm	⊢ ( 𝜑 → 𝐻 ∈ ( ( Poly1 ‘ 𝐾 ) RingHom 𝐾 ) )
14		eqid	⊢ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
15		eqid	⊢ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
16		crngring	⊢ ( 𝐾 ∈ CRing → 𝐾 ∈ Ring )
17	12 16	syl	⊢ ( 𝜑 → 𝐾 ∈ Ring )
18	3	simp2d	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
19	2	eqcomi	⊢ ( chr ‘ 𝐾 ) = 𝑃
20	3	simp1d	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
21		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
22	20 21	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
23	22	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
24	19 23	eqeltrid	⊢ ( 𝜑 → ( chr ‘ 𝐾 ) ∈ ℤ )
25	3	simp3d	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
26	19 25	eqbrtrid	⊢ ( 𝜑 → ( chr ‘ 𝐾 ) ∥ 𝑁 )
27		eqid	⊢ ( ℤ/nℤ ‘ 𝑁 ) = ( ℤ/nℤ ‘ 𝑁 )
28	17 18 24 26 27 5	zndvdchrrhm	⊢ ( 𝜑 → 𝐺 ∈ ( ( ℤ/nℤ ‘ 𝑁 ) RingHom 𝐾 ) )
29	14 9 15 4 28	rhmply1	⊢ ( 𝜑 → 𝐹 ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) RingHom ( Poly1 ‘ 𝐾 ) ) )
30		rhmco	⊢ ( ( 𝐻 ∈ ( ( Poly1 ‘ 𝐾 ) RingHom 𝐾 ) ∧ 𝐹 ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) RingHom ( Poly1 ‘ 𝐾 ) ) ) → ( 𝐻 ∘ 𝐹 ) ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) RingHom 𝐾 ) )
31	13 29 30	syl2anc	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) RingHom 𝐾 ) )