Metamath Proof Explorer

Theorem aks6d1c6isolem2

Description: Lemma to construct the group homomorphism for the AKS Theorem. (Contributed by metakunt, 14-May-2025)

Ref Expression
Hypotheses aks6d1c6isolem1.1 
|- ( ph -> R e. CMnd )
aks6d1c6isolem1.2 
|- ( ph -> K e. NN )
aks6d1c6isolem1.3 
|- U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
aks6d1c6isolem1.4 
|- F = ( x e. ZZ |-> ( x ( .g ` ( R |`s U ) ) M ) )
aks6d1c6isolem1.5 
|- ( ph -> M e. ( R PrimRoots K ) )
Assertion aks6d1c6isolem2 
|- ( ph -> F e. ( ZZring GrpHom ( ( R |`s U ) |`s ran F ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c6isolem1.1 
 |-  ( ph -> R e. CMnd )
2 aks6d1c6isolem1.2 
 |-  ( ph -> K e. NN )
3 aks6d1c6isolem1.3 
 |-  U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
4 aks6d1c6isolem1.4 
 |-  F = ( x e. ZZ |-> ( x ( .g ` ( R |`s U ) ) M ) )
5 aks6d1c6isolem1.5 
 |-  ( ph -> M e. ( R PrimRoots K ) )
6 zringbas 
 |-  ZZ = ( Base ` ZZring )
7 eqid 
 |-  ( Base ` ( ( R |`s U ) |`s ran F ) ) = ( Base ` ( ( R |`s U ) |`s ran F ) )
8 zringplusg 
 |-  + = ( +g ` ZZring )
9 zex 
 |-  ZZ e. _V
10 9 mptex 
 |-  ( x e. ZZ |-> ( x ( .g ` ( R |`s U ) ) M ) ) e. _V
11 4 10 eqeltri 
 |-  F e. _V
12 11 rnex 
 |-  ran F e. _V
13 eqid 
 |-  ( ( R |`s U ) |`s ran F ) = ( ( R |`s U ) |`s ran F )
14 eqid 
 |-  ( +g ` ( R |`s U ) ) = ( +g ` ( R |`s U ) )
15 13 14 ressplusg 
 |-  ( ran F e. _V -> ( +g ` ( R |`s U ) ) = ( +g ` ( ( R |`s U ) |`s ran F ) ) )
16 12 15 ax-mp 
 |-  ( +g ` ( R |`s U ) ) = ( +g ` ( ( R |`s U ) |`s ran F ) )
17 zringring 
 |-  ZZring e. Ring
18 17 a1i 
 |-  ( ph -> ZZring e. Ring )
19 ringgrp 
 |-  ( ZZring e. Ring -> ZZring e. Grp )
20 18 19 syl 
 |-  ( ph -> ZZring e. Grp )
21 1 2 3 4 5 aks6d1c6isolem1 
 |-  ( ph -> ( ( R |`s U ) |`s ran F ) e. Grp )
22 ovexd 
 |-  ( ( ph /\ x e. ZZ ) -> ( x ( .g ` ( R |`s U ) ) M ) e. _V )
23 22 4 fmptd 
 |-  ( ph -> F : ZZ --> _V )
24 ffn 
 |-  ( F : ZZ --> _V -> F Fn ZZ )
25 23 24 syl 
 |-  ( ph -> F Fn ZZ )
26 dffn3 
 |-  ( F Fn ZZ <-> F : ZZ --> ran F )
27 25 26 sylib 
 |-  ( ph -> F : ZZ --> ran F )
28 fvelrnb 
 |-  ( F Fn ZZ -> ( w e. ran F <-> E. v e. ZZ ( F ` v ) = w ) )
29 25 28 syl 
 |-  ( ph -> ( w e. ran F <-> E. v e. ZZ ( F ` v ) = w ) )
30 29 biimpd 
 |-  ( ph -> ( w e. ran F -> E. v e. ZZ ( F ` v ) = w ) )
31 30 imp 
 |-  ( ( ph /\ w e. ran F ) -> E. v e. ZZ ( F ` v ) = w )
32 simpr 
 |-  ( ( ( ( ph /\ E. v e. ZZ ( F ` v ) = w ) /\ z e. ZZ ) /\ ( F ` z ) = w ) -> ( F ` z ) = w )
33 32 eqcomd 
 |-  ( ( ( ( ph /\ E. v e. ZZ ( F ` v ) = w ) /\ z e. ZZ ) /\ ( F ` z ) = w ) -> w = ( F ` z ) )
34 simplll 
 |-  ( ( ( ( ph /\ E. v e. ZZ ( F ` v ) = w ) /\ z e. ZZ ) /\ ( F ` z ) = w ) -> ph )
35 simplr 
 |-  ( ( ( ( ph /\ E. v e. ZZ ( F ` v ) = w ) /\ z e. ZZ ) /\ ( F ` z ) = w ) -> z e. ZZ )
36 34 35 jca 
 |-  ( ( ( ( ph /\ E. v e. ZZ ( F ` v ) = w ) /\ z e. ZZ ) /\ ( F ` z ) = w ) -> ( ph /\ z e. ZZ ) )
37 4 a1i 
 |-  ( ( ph /\ z e. ZZ ) -> F = ( x e. ZZ |-> ( x ( .g ` ( R |`s U ) ) M ) ) )
38 simpr 
 |-  ( ( ( ph /\ z e. ZZ ) /\ x = z ) -> x = z )
39 38 oveq1d 
 |-  ( ( ( ph /\ z e. ZZ ) /\ x = z ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( z ( .g ` ( R |`s U ) ) M ) )
40 simpr 
 |-  ( ( ph /\ z e. ZZ ) -> z e. ZZ )
41 ovexd 
 |-  ( ( ph /\ z e. ZZ ) -> ( z ( .g ` ( R |`s U ) ) M ) e. _V )
42 37 39 40 41 fvmptd 
 |-  ( ( ph /\ z e. ZZ ) -> ( F ` z ) = ( z ( .g ` ( R |`s U ) ) M ) )
43 eqid 
 |-  ( Base ` ( R |`s U ) ) = ( Base ` ( R |`s U ) )
44 eqid 
 |-  ( .g ` ( R |`s U ) ) = ( .g ` ( R |`s U ) )
45 1 2 3 primrootsunit 
 |-  ( ph -> ( ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) /\ ( R |`s U ) e. Abel ) )
46 45 simprd 
 |-  ( ph -> ( R |`s U ) e. Abel )
47 46 ablgrpd 
 |-  ( ph -> ( R |`s U ) e. Grp )
48 47 adantr 
 |-  ( ( ph /\ z e. ZZ ) -> ( R |`s U ) e. Grp )
49 45 simpld 
 |-  ( ph -> ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) )
50 5 49 eleqtrd 
 |-  ( ph -> M e. ( ( R |`s U ) PrimRoots K ) )
51 46 ablcmnd 
 |-  ( ph -> ( R |`s U ) e. CMnd )
52 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
53 51 52 44 isprimroot 
 |-  ( ph -> ( M e. ( ( R |`s U ) PrimRoots K ) <-> ( M e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
54 53 biimpd 
 |-  ( ph -> ( M e. ( ( R |`s U ) PrimRoots K ) -> ( M e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
55 50 54 mpd 
 |-  ( ph -> ( M e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
56 55 simp1d 
 |-  ( ph -> M e. ( Base ` ( R |`s U ) ) )
57 56 adantr 
 |-  ( ( ph /\ z e. ZZ ) -> M e. ( Base ` ( R |`s U ) ) )
58 43 44 48 40 57 mulgcld 
 |-  ( ( ph /\ z e. ZZ ) -> ( z ( .g ` ( R |`s U ) ) M ) e. ( Base ` ( R |`s U ) ) )
59 42 58 eqeltrd 
 |-  ( ( ph /\ z e. ZZ ) -> ( F ` z ) e. ( Base ` ( R |`s U ) ) )
60 36 59 syl 
 |-  ( ( ( ( ph /\ E. v e. ZZ ( F ` v ) = w ) /\ z e. ZZ ) /\ ( F ` z ) = w ) -> ( F ` z ) e. ( Base ` ( R |`s U ) ) )
61 33 60 eqeltrd 
 |-  ( ( ( ( ph /\ E. v e. ZZ ( F ` v ) = w ) /\ z e. ZZ ) /\ ( F ` z ) = w ) -> w e. ( Base ` ( R |`s U ) ) )
62 nfv 
 |-  F/ z ( F ` v ) = w
63 nfv 
 |-  F/ v ( F ` z ) = w
64 fveqeq2 
 |-  ( v = z -> ( ( F ` v ) = w <-> ( F ` z ) = w ) )
65 62 63 64 cbvrexw 
 |-  ( E. v e. ZZ ( F ` v ) = w <-> E. z e. ZZ ( F ` z ) = w )
66 65 bilani 
 |-  ( ( ph /\ E. v e. ZZ ( F ` v ) = w ) -> E. z e. ZZ ( F ` z ) = w )
67 61 66 r19.29a 
 |-  ( ( ph /\ E. v e. ZZ ( F ` v ) = w ) -> w e. ( Base ` ( R |`s U ) ) )
68 67 ex 
 |-  ( ph -> ( E. v e. ZZ ( F ` v ) = w -> w e. ( Base ` ( R |`s U ) ) ) )
69 68 adantr 
 |-  ( ( ph /\ w e. ran F ) -> ( E. v e. ZZ ( F ` v ) = w -> w e. ( Base ` ( R |`s U ) ) ) )
70 69 imp 
 |-  ( ( ( ph /\ w e. ran F ) /\ E. v e. ZZ ( F ` v ) = w ) -> w e. ( Base ` ( R |`s U ) ) )
71 31 70 mpdan 
 |-  ( ( ph /\ w e. ran F ) -> w e. ( Base ` ( R |`s U ) ) )
72 71 ex 
 |-  ( ph -> ( w e. ran F -> w e. ( Base ` ( R |`s U ) ) ) )
73 72 ssrdv 
 |-  ( ph -> ran F C_ ( Base ` ( R |`s U ) ) )
74 13 43 ressbas2 
 |-  ( ran F C_ ( Base ` ( R |`s U ) ) -> ran F = ( Base ` ( ( R |`s U ) |`s ran F ) ) )
75 73 74 syl 
 |-  ( ph -> ran F = ( Base ` ( ( R |`s U ) |`s ran F ) ) )
76 75 feq3d 
 |-  ( ph -> ( F : ZZ --> ran F <-> F : ZZ --> ( Base ` ( ( R |`s U ) |`s ran F ) ) ) )
77 27 76 mpbid 
 |-  ( ph -> F : ZZ --> ( Base ` ( ( R |`s U ) |`s ran F ) ) )
78 4 a1i 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> F = ( x e. ZZ |-> ( x ( .g ` ( R |`s U ) ) M ) ) )
79 simpr 
 |-  ( ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) /\ x = ( y + z ) ) -> x = ( y + z ) )
80 79 oveq1d 
 |-  ( ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) /\ x = ( y + z ) ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( ( y + z ) ( .g ` ( R |`s U ) ) M ) )
81 simprl 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> y e. ZZ )
82 simprr 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> z e. ZZ )
83 81 82 zaddcld 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( y + z ) e. ZZ )
84 ovexd 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( y + z ) ( .g ` ( R |`s U ) ) M ) e. _V )
85 78 80 83 84 fvmptd 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( F ` ( y + z ) ) = ( ( y + z ) ( .g ` ( R |`s U ) ) M ) )
86 47 adantr 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( R |`s U ) e. Grp )
87 56 adantr 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> M e. ( Base ` ( R |`s U ) ) )
88 81 82 87 3jca 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( y e. ZZ /\ z e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) )
89 43 44 14 mulgdir 
 |-  ( ( ( R |`s U ) e. Grp /\ ( y e. ZZ /\ z e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) ) -> ( ( y + z ) ( .g ` ( R |`s U ) ) M ) = ( ( y ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( z ( .g ` ( R |`s U ) ) M ) ) )
90 86 88 89 syl2anc 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( y + z ) ( .g ` ( R |`s U ) ) M ) = ( ( y ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( z ( .g ` ( R |`s U ) ) M ) ) )
91 simpr 
 |-  ( ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) /\ x = y ) -> x = y )
92 91 oveq1d 
 |-  ( ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) /\ x = y ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( y ( .g ` ( R |`s U ) ) M ) )
93 ovexd 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( y ( .g ` ( R |`s U ) ) M ) e. _V )
94 78 92 81 93 fvmptd 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( F ` y ) = ( y ( .g ` ( R |`s U ) ) M ) )
95 simpr 
 |-  ( ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) /\ x = z ) -> x = z )
96 95 oveq1d 
 |-  ( ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) /\ x = z ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( z ( .g ` ( R |`s U ) ) M ) )
97 ovexd 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( z ( .g ` ( R |`s U ) ) M ) e. _V )
98 78 96 82 97 fvmptd 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( F ` z ) = ( z ( .g ` ( R |`s U ) ) M ) )
99 94 98 oveq12d 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( F ` y ) ( +g ` ( R |`s U ) ) ( F ` z ) ) = ( ( y ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( z ( .g ` ( R |`s U ) ) M ) ) )
100 99 eqcomd 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( y ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( z ( .g ` ( R |`s U ) ) M ) ) = ( ( F ` y ) ( +g ` ( R |`s U ) ) ( F ` z ) ) )
101 90 100 eqtrd 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( ( y + z ) ( .g ` ( R |`s U ) ) M ) = ( ( F ` y ) ( +g ` ( R |`s U ) ) ( F ` z ) ) )
102 85 101 eqtrd 
 |-  ( ( ph /\ ( y e. ZZ /\ z e. ZZ ) ) -> ( F ` ( y + z ) ) = ( ( F ` y ) ( +g ` ( R |`s U ) ) ( F ` z ) ) )
103 6 7 8 16 20 21 77 102 isghmd 
 |-  ( ph -> F e. ( ZZring GrpHom ( ( R |`s U ) |`s ran F ) ) )