Metamath Proof Explorer

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 
|- ( ph -> K e. Field )
aks5lem1.2 
|- P = ( chr ` K )
aks5lem1.3 
|- ( ph -> ( P e. Prime /\ N e. NN /\ P || N ) )
aks5lem1.4 
|- F = ( p e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( G o. p ) )
aks5lem1.5 
|- G = ( q e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " q ) )
aks5lem1.6 
|- H = ( r e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` r ) ` M ) )
aks5lem1.7 
|- ( ph -> M e. ( Base ` K ) )
Assertion aks5lem1 
|- ( ph -> ( H o. F ) e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom K ) )

Proof

Step Hyp Ref Expression
1 aks5lem1.1 
 |-  ( ph -> K e. Field )
2 aks5lem1.2 
 |-  P = ( chr ` K )
3 aks5lem1.3 
 |-  ( ph -> ( P e. Prime /\ N e. NN /\ P || N ) )
4 aks5lem1.4 
 |-  F = ( p e. ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) |-> ( G o. p ) )
5 aks5lem1.5 
 |-  G = ( q e. ( Base ` ( Z/nZ ` N ) ) |-> U. ( ( ZRHom ` K ) " q ) )
6 aks5lem1.6 
 |-  H = ( r e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( eval1 ` K ) ` r ) ` M ) )
7 aks5lem1.7 
 |-  ( ph -> M e. ( Base ` K ) )
8 eqid 
 |-  ( eval1 ` K ) = ( eval1 ` K )
9 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
10 eqid 
 |-  ( Base ` K ) = ( Base ` K )
11 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
12 1 fldcrngd 
 |-  ( ph -> K e. CRing )
13 8 9 10 11 12 7 6 evl1maprhm 
 |-  ( ph -> H e. ( ( Poly1 ` K ) RingHom K ) )
14 eqid 
 |-  ( Poly1 ` ( Z/nZ ` N ) ) = ( Poly1 ` ( Z/nZ ` N ) )
15 eqid 
 |-  ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) ) = ( Base ` ( Poly1 ` ( Z/nZ ` N ) ) )
16 crngring 
 |-  ( K e. CRing -> K e. Ring )
17 12 16 syl 
 |-  ( ph -> K e. Ring )
18 3 simp2d 
 |-  ( ph -> N e. NN )
19 2 eqcomi 
 |-  ( chr ` K ) = P
20 3 simp1d 
 |-  ( ph -> P e. Prime )
21 prmnn 
 |-  ( P e. Prime -> P e. NN )
22 20 21 syl 
 |-  ( ph -> P e. NN )
23 22 nnzd 
 |-  ( ph -> P e. ZZ )
24 19 23 eqeltrid 
 |-  ( ph -> ( chr ` K ) e. ZZ )
25 3 simp3d 
 |-  ( ph -> P || N )
26 19 25 eqbrtrid 
 |-  ( ph -> ( chr ` K ) || N )
27 eqid 
 |-  ( Z/nZ ` N ) = ( Z/nZ ` N )
28 17 18 24 26 27 5 zndvdchrrhm 
 |-  ( ph -> G e. ( ( Z/nZ ` N ) RingHom K ) )
29 14 9 15 4 28 rhmply1 
 |-  ( ph -> F e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom ( Poly1 ` K ) ) )
30 rhmco 
 |-  ( ( H e. ( ( Poly1 ` K ) RingHom K ) /\ F e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom ( Poly1 ` K ) ) ) -> ( H o. F ) e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom K ) )
31 13 29 30 syl2anc 
 |-  ( ph -> ( H o. F ) e. ( ( Poly1 ` ( Z/nZ ` N ) ) RingHom K ) )