Metamath Proof Explorer

Theorem aks5lem7

Description: Lemma for aks5. We clean up the hypotheses compared to aks5lem6 . (Contributed by metakunt, 9-Aug-2025)

Ref Expression
Hypotheses aks5lem7.1 
|- ( ph -> ( # ` ( Base ` K ) ) e. NN )
aks5lem7.2 
|- P = ( chr ` K )
aks5lem7.3 
|- ( ph -> K e. Field )
aks5lem7.4 
|- ( ph -> P e. Prime )
aks5lem7.5 
|- ( ph -> R e. NN )
aks5lem7.6 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks5lem7.7 
|- ( ph -> P || N )
aks5lem7.8 
|- ( ph -> ( N gcd R ) = 1 )
aks5lem7.9 
|- A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
aks5lem7.10 
|- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
aks5lem7.11 
|- ( ph -> R || ( ( # ` ( Base ` K ) ) - 1 ) )
aks5lem7.12 
|- ( ph -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
aks5lem7.13 
|- ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
aks5lem7.14 
|- S = ( Poly1 ` ( Z/nZ ` N ) )
aks5lem7.15 
|- L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) X ) ( -g ` S ) ( 1r ` S ) ) } )
aks5lem7.16 
|- X = ( var1 ` ( Z/nZ ` N ) )
Assertion aks5lem7 
|- ( ph -> N = ( P ^ ( P pCnt N ) ) )

Proof

Step Hyp Ref Expression
1 aks5lem7.1 
 |-  ( ph -> ( # ` ( Base ` K ) ) e. NN )
2 aks5lem7.2 
 |-  P = ( chr ` K )
3 aks5lem7.3 
 |-  ( ph -> K e. Field )
4 aks5lem7.4 
 |-  ( ph -> P e. Prime )
5 aks5lem7.5 
 |-  ( ph -> R e. NN )
6 aks5lem7.6 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
7 aks5lem7.7 
 |-  ( ph -> P || N )
8 aks5lem7.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks5lem7.9 
 |-  A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
10 aks5lem7.10 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
11 aks5lem7.11 
 |-  ( ph -> R || ( ( # ` ( Base ` K ) ) - 1 ) )
12 aks5lem7.12 
 |-  ( ph -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
13 aks5lem7.13 
 |-  ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
14 aks5lem7.14 
 |-  S = ( Poly1 ` ( Z/nZ ` N ) )
15 aks5lem7.15 
 |-  L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) X ) ( -g ` S ) ( 1r ` S ) ) } )
16 aks5lem7.16 
 |-  X = ( var1 ` ( Z/nZ ` N ) )
17 eqid 
 |-  { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. l e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` l ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) l ) ) ) } = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. l e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` l ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) l ) ) ) }
18 3 adantr 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> K e. Field )
19 4 adantr 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> P e. Prime )
20 5 adantr 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> R e. NN )
21 6 adantr 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> N e. ( ZZ>= ` 3 ) )
22 7 adantr 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> P || N )
23 8 adantr 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> ( N gcd R ) = 1 )
24 10 adantr 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
25 eqid 
 |-  ( Base ` K ) = ( Base ` K )
26 eqid 
 |-  ( .g ` ( mulGrp ` K ) ) = ( .g ` ( mulGrp ` K ) )
27 eqid 
 |-  ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) = ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) )
28 fldidom 
 |-  ( K e. Field -> K e. IDomn )
29 3 28 syl 
 |-  ( ph -> K e. IDomn )
30 29 idomcringd 
 |-  ( ph -> K e. CRing )
31 25 2 26 27 30 4 frobrhm 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingHom K ) )
32 3 3 31 25 25 fldhmf1 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) : ( Base ` K ) -1-1-> ( Base ` K ) )
33 fvexd 
 |-  ( ph -> ( Base ` K ) e. _V )
34 eqeng 
 |-  ( ( Base ` K ) e. _V -> ( ( Base ` K ) = ( Base ` K ) -> ( Base ` K ) ~~ ( Base ` K ) ) )
35 33 25 34 mpisyl 
 |-  ( ph -> ( Base ` K ) ~~ ( Base ` K ) )
36 1 nnnn0d 
 |-  ( ph -> ( # ` ( Base ` K ) ) e. NN0 )
37 hashclb 
 |-  ( ( Base ` K ) e. _V -> ( ( Base ` K ) e. Fin <-> ( # ` ( Base ` K ) ) e. NN0 ) )
38 33 37 syl 
 |-  ( ph -> ( ( Base ` K ) e. Fin <-> ( # ` ( Base ` K ) ) e. NN0 ) )
39 36 38 mpbird 
 |-  ( ph -> ( Base ` K ) e. Fin )
40 f1finf1o 
 |-  ( ( ( Base ` K ) ~~ ( Base ` K ) /\ ( Base ` K ) e. Fin ) -> ( ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) : ( Base ` K ) -1-1-> ( Base ` K ) <-> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) )
41 35 39 40 syl2anc 
 |-  ( ph -> ( ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) : ( Base ` K ) -1-1-> ( Base ` K ) <-> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) )
42 32 41 mpbid 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
43 31 42 jca 
 |-  ( ph -> ( ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingHom K ) /\ ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) )
44 25 25 isrim 
 |-  ( ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) <-> ( ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingHom K ) /\ ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) )
45 43 44 sylibr 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
46 45 adantr 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
47 simpr 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> m e. ( ( mulGrp ` K ) PrimRoots R ) )
48 13 adantr 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
49 16 oveq2i 
 |-  ( R ( .g ` ( mulGrp ` S ) ) X ) = ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) )
50 49 oveq1i 
 |-  ( ( R ( .g ` ( mulGrp ` S ) ) X ) ( -g ` S ) ( 1r ` S ) ) = ( ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` S ) ( 1r ` S ) )
51 50 sneqi 
 |-  { ( ( R ( .g ` ( mulGrp ` S ) ) X ) ( -g ` S ) ( 1r ` S ) ) } = { ( ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` S ) ( 1r ` S ) ) }
52 51 fveq2i 
 |-  ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) X ) ( -g ` S ) ( 1r ` S ) ) } ) = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` S ) ( 1r ` S ) ) } )
53 15 52 eqtri 
 |-  L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` S ) ( 1r ` S ) ) } )
54 12 adantr 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
55 17 2 18 19 20 21 22 23 9 24 46 47 48 14 53 16 54 aks5lem6 
 |-  ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> N = ( P ^ ( P pCnt N ) ) )
56 55 adantr 
 |-  ( ( ( ph /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) /\ m e. ( ( mulGrp ` K ) PrimRoots R ) ) -> N = ( P ^ ( P pCnt N ) ) )
57 eqid 
 |-  ( ( mulGrp ` K ) |`s ( Unit ` K ) ) = ( ( mulGrp ` K ) |`s ( Unit ` K ) )
58 3 flddrngd 
 |-  ( ph -> K e. DivRing )
59 eqid 
 |-  ( Unit ` K ) = ( Unit ` K )
60 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
61 25 59 60 isdrng 
 |-  ( K e. DivRing <-> ( K e. Ring /\ ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) ) )
62 61 biimpi 
 |-  ( K e. DivRing -> ( K e. Ring /\ ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) ) )
63 58 62 syl 
 |-  ( ph -> ( K e. Ring /\ ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) ) )
64 63 simprd 
 |-  ( ph -> ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) )
65 64 fveq2d 
 |-  ( ph -> ( # ` ( Unit ` K ) ) = ( # ` ( ( Base ` K ) \ { ( 0g ` K ) } ) ) )
66 63 simpld 
 |-  ( ph -> K e. Ring )
67 ringgrp 
 |-  ( K e. Ring -> K e. Grp )
68 66 67 syl 
 |-  ( ph -> K e. Grp )
69 25 60 grpidcl 
 |-  ( K e. Grp -> ( 0g ` K ) e. ( Base ` K ) )
70 68 69 syl 
 |-  ( ph -> ( 0g ` K ) e. ( Base ` K ) )
71 hashdifsn 
 |-  ( ( ( Base ` K ) e. Fin /\ ( 0g ` K ) e. ( Base ` K ) ) -> ( # ` ( ( Base ` K ) \ { ( 0g ` K ) } ) ) = ( ( # ` ( Base ` K ) ) - 1 ) )
72 39 70 71 syl2anc 
 |-  ( ph -> ( # ` ( ( Base ` K ) \ { ( 0g ` K ) } ) ) = ( ( # ` ( Base ` K ) ) - 1 ) )
73 65 72 eqtr2d 
 |-  ( ph -> ( ( # ` ( Base ` K ) ) - 1 ) = ( # ` ( Unit ` K ) ) )
74 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
75 74 25 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
76 75 eqcomi 
 |-  ( Base ` ( mulGrp ` K ) ) = ( Base ` K )
77 76 59 unitss 
 |-  ( Unit ` K ) C_ ( Base ` ( mulGrp ` K ) )
78 77 a1i 
 |-  ( ph -> ( Unit ` K ) C_ ( Base ` ( mulGrp ` K ) ) )
79 eqid 
 |-  ( Base ` ( mulGrp ` K ) ) = ( Base ` ( mulGrp ` K ) )
80 57 79 ressbas2 
 |-  ( ( Unit ` K ) C_ ( Base ` ( mulGrp ` K ) ) -> ( Unit ` K ) = ( Base ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) ) )
81 78 80 syl 
 |-  ( ph -> ( Unit ` K ) = ( Base ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) ) )
82 81 fveq2d 
 |-  ( ph -> ( # ` ( Unit ` K ) ) = ( # ` ( Base ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) ) ) )
83 73 82 eqtrd 
 |-  ( ph -> ( ( # ` ( Base ` K ) ) - 1 ) = ( # ` ( Base ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) ) ) )
84 11 83 breqtrd 
 |-  ( ph -> R || ( # ` ( Base ` ( ( mulGrp ` K ) |`s ( Unit ` K ) ) ) ) )
85 57 29 39 5 84 unitscyglem5 
 |-  ( ph -> ( ( mulGrp ` K ) PrimRoots R ) =/= (/) )
86 n0rex 
 |-  ( ( ( mulGrp ` K ) PrimRoots R ) =/= (/) -> E. m e. ( ( mulGrp ` K ) PrimRoots R ) m e. ( ( mulGrp ` K ) PrimRoots R ) )
87 85 86 syl 
 |-  ( ph -> E. m e. ( ( mulGrp ` K ) PrimRoots R ) m e. ( ( mulGrp ` K ) PrimRoots R ) )
88 56 87 r19.29a 
 |-  ( ph -> N = ( P ^ ( P pCnt N ) ) )