Metamath Proof Explorer

Theorem aks6d1c6lem5

Description: Eliminate the size hypothesis. Claim 6. (Contributed by metakunt, 15-May-2025)

Ref Expression
Hypotheses aks6d1c6lem5.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
aks6d1c6lem5.2 
|- P = ( chr ` K )
aks6d1c6lem5.3 
|- ( ph -> K e. Field )
aks6d1c6lem5.4 
|- ( ph -> P e. Prime )
aks6d1c6lem5.5 
|- ( ph -> R e. NN )
aks6d1c6lem5.6 
|- ( ph -> N e. NN )
aks6d1c6lem5.7 
|- ( ph -> P || N )
aks6d1c6lem5.8 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c6lem5.9 
|- ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
aks6d1c6lem5.10 
|- G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
aks6d1c6lem5.11 
|- A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
aksaks6dlem5.12 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
aks6d1c6lem5.13 
|- L = ( ZRHom ` ( Z/nZ ` R ) )
aks6d1c6lem5.14 
|- ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
aks6d1c6lem5.15 
|- ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
aks6d1c6lem5.16 
|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
aks6d1c6lem5.17 
|- H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
aks6d1c6lem5.18 
|- D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) )
aks6d1c6lem5.19 
|- S = { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) }
aks6d1c6lem5.20 
|- J = ( j e. ZZ |-> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
aks6d1c6lem5.22 
|- U = { m e. ( Base ` ( mulGrp ` K ) ) | E. n e. ( Base ` ( mulGrp ` K ) ) ( n ( +g ` ( mulGrp ` K ) ) m ) = ( 0g ` ( mulGrp ` K ) ) }
aks6d1c6lem5.23 
|- X = ( b e. ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) |-> U. ( J " b ) )
Assertion aks6d1c6lem5 
|- ( ph -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c6lem5.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
2 aks6d1c6lem5.2 
 |-  P = ( chr ` K )
3 aks6d1c6lem5.3 
 |-  ( ph -> K e. Field )
4 aks6d1c6lem5.4 
 |-  ( ph -> P e. Prime )
5 aks6d1c6lem5.5 
 |-  ( ph -> R e. NN )
6 aks6d1c6lem5.6 
 |-  ( ph -> N e. NN )
7 aks6d1c6lem5.7 
 |-  ( ph -> P || N )
8 aks6d1c6lem5.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks6d1c6lem5.9 
 |-  ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
10 aks6d1c6lem5.10 
 |-  G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
11 aks6d1c6lem5.11 
 |-  A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
12 aksaks6dlem5.12 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
13 aks6d1c6lem5.13 
 |-  L = ( ZRHom ` ( Z/nZ ` R ) )
14 aks6d1c6lem5.14 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
15 aks6d1c6lem5.15 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
16 aks6d1c6lem5.16 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
17 aks6d1c6lem5.17 
 |-  H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
18 aks6d1c6lem5.18 
 |-  D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) )
19 aks6d1c6lem5.19 
 |-  S = { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) }
20 aks6d1c6lem5.20 
 |-  J = ( j e. ZZ |-> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
21 aks6d1c6lem5.22 
 |-  U = { m e. ( Base ` ( mulGrp ` K ) ) | E. n e. ( Base ` ( mulGrp ` K ) ) ( n ( +g ` ( mulGrp ` K ) ) m ) = ( 0g ` ( mulGrp ` K ) ) }
22 aks6d1c6lem5.23 
 |-  X = ( b e. ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) |-> U. ( J " b ) )
23 eqid 
 |-  ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) = ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) )
24 3 fldcrngd 
 |-  ( ph -> K e. CRing )
25 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
26 25 crngmgp 
 |-  ( K e. CRing -> ( mulGrp ` K ) e. CMnd )
27 24 26 syl 
 |-  ( ph -> ( mulGrp ` K ) e. CMnd )
28 27 5 21 20 16 aks6d1c6isolem2 
 |-  ( ph -> J e. ( ZZring GrpHom ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) )
29 eqid 
 |-  ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) = ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } )
30 eqid 
 |-  ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) = ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) )
31 zringbas 
 |-  ZZ = ( Base ` ZZring )
32 nfcv 
 |-  F/_ c [ d ] ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) )
33 nfcv 
 |-  F/_ d [ c ] ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) )
34 eceq1 
 |-  ( d = c -> [ d ] ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) = [ c ] ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) )
35 32 33 34 cbvmpt 
 |-  ( d e. ZZ |-> [ d ] ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) = ( c e. ZZ |-> [ c ] ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) )
36 23 28 29 30 22 31 35 ghmquskerco 
 |-  ( ph -> J = ( X o. ( d e. ZZ |-> [ d ] ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) )
37 eqid 
 |-  ( RSpan ` ZZring ) = ( RSpan ` ZZring )
38 27 5 21 20 16 37 aks6d1c6isolem3 
 |-  ( ph -> ( ( RSpan ` ZZring ) ` { R } ) = ( `' J " { ( 0g ` ( ( mulGrp ` K ) |`s U ) ) } ) )
39 27 5 21 primrootsunit 
 |-  ( ph -> ( ( ( mulGrp ` K ) PrimRoots R ) = ( ( ( mulGrp ` K ) |`s U ) PrimRoots R ) /\ ( ( mulGrp ` K ) |`s U ) e. Abel ) )
40 39 simprd 
 |-  ( ph -> ( ( mulGrp ` K ) |`s U ) e. Abel )
41 40 ablgrpd 
 |-  ( ph -> ( ( mulGrp ` K ) |`s U ) e. Grp )
42 41 grpmndd 
 |-  ( ph -> ( ( mulGrp ` K ) |`s U ) e. Mnd )
43 0zd 
 |-  ( ph -> 0 e. ZZ )
44 simpr 
 |-  ( ( ph /\ w = 0 ) -> w = 0 )
45 44 fveqeq2d 
 |-  ( ( ph /\ w = 0 ) -> ( ( J ` w ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) <-> ( J ` 0 ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) ) )
46 20 a1i 
 |-  ( ph -> J = ( j e. ZZ |-> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
47 simpr 
 |-  ( ( ph /\ j = 0 ) -> j = 0 )
48 47 oveq1d 
 |-  ( ( ph /\ j = 0 ) -> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0 ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
49 39 simpld 
 |-  ( ph -> ( ( mulGrp ` K ) PrimRoots R ) = ( ( ( mulGrp ` K ) |`s U ) PrimRoots R ) )
50 16 49 eleqtrd 
 |-  ( ph -> M e. ( ( ( mulGrp ` K ) |`s U ) PrimRoots R ) )
51 40 ablcmnd 
 |-  ( ph -> ( ( mulGrp ` K ) |`s U ) e. CMnd )
52 5 nnnn0d 
 |-  ( ph -> R e. NN0 )
53 eqid 
 |-  ( .g ` ( ( mulGrp ` K ) |`s U ) ) = ( .g ` ( ( mulGrp ` K ) |`s U ) )
54 51 52 53 isprimroot 
 |-  ( ph -> ( M e. ( ( ( mulGrp ` K ) |`s U ) PrimRoots R ) <-> ( M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) /\ ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) -> R || l ) ) ) )
55 54 biimpd 
 |-  ( ph -> ( M e. ( ( ( mulGrp ` K ) |`s U ) PrimRoots R ) -> ( M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) /\ ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) -> R || l ) ) ) )
56 50 55 mpd 
 |-  ( ph -> ( M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) /\ ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) -> R || l ) ) )
57 56 simp1d 
 |-  ( ph -> M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) )
58 eqid 
 |-  ( Base ` ( ( mulGrp ` K ) |`s U ) ) = ( Base ` ( ( mulGrp ` K ) |`s U ) )
59 eqid 
 |-  ( 0g ` ( ( mulGrp ` K ) |`s U ) ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) )
60 58 59 53 mulg0 
 |-  ( M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) -> ( 0 ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
61 57 60 syl 
 |-  ( ph -> ( 0 ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
62 61 adantr 
 |-  ( ( ph /\ j = 0 ) -> ( 0 ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
63 48 62 eqtrd 
 |-  ( ( ph /\ j = 0 ) -> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
64 fvexd 
 |-  ( ph -> ( 0g ` ( ( mulGrp ` K ) |`s U ) ) e. _V )
65 46 63 43 64 fvmptd 
 |-  ( ph -> ( J ` 0 ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
66 43 45 65 rspcedvd 
 |-  ( ph -> E. w e. ZZ ( J ` w ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
67 41 adantr 
 |-  ( ( ph /\ j e. ZZ ) -> ( ( mulGrp ` K ) |`s U ) e. Grp )
68 simpr 
 |-  ( ( ph /\ j e. ZZ ) -> j e. ZZ )
69 57 adantr 
 |-  ( ( ph /\ j e. ZZ ) -> M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) )
70 58 53 67 68 69 mulgcld 
 |-  ( ( ph /\ j e. ZZ ) -> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) )
71 70 20 fmptd 
 |-  ( ph -> J : ZZ --> ( Base ` ( ( mulGrp ` K ) |`s U ) ) )
72 71 ffnd 
 |-  ( ph -> J Fn ZZ )
73 fvelrnb 
 |-  ( J Fn ZZ -> ( ( 0g ` ( ( mulGrp ` K ) |`s U ) ) e. ran J <-> E. w e. ZZ ( J ` w ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) ) )
74 72 73 syl 
 |-  ( ph -> ( ( 0g ` ( ( mulGrp ` K ) |`s U ) ) e. ran J <-> E. w e. ZZ ( J ` w ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) ) )
75 66 74 mpbird 
 |-  ( ph -> ( 0g ` ( ( mulGrp ` K ) |`s U ) ) e. ran J )
76 71 frnd 
 |-  ( ph -> ran J C_ ( Base ` ( ( mulGrp ` K ) |`s U ) ) )
77 eqid 
 |-  ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) = ( ( ( mulGrp ` K ) |`s U ) |`s ran J )
78 77 58 59 ress0g 
 |-  ( ( ( ( mulGrp ` K ) |`s U ) e. Mnd /\ ( 0g ` ( ( mulGrp ` K ) |`s U ) ) e. ran J /\ ran J C_ ( Base ` ( ( mulGrp ` K ) |`s U ) ) ) -> ( 0g ` ( ( mulGrp ` K ) |`s U ) ) = ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) )
79 42 75 76 78 syl3anc 
 |-  ( ph -> ( 0g ` ( ( mulGrp ` K ) |`s U ) ) = ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) )
80 79 sneqd 
 |-  ( ph -> { ( 0g ` ( ( mulGrp ` K ) |`s U ) ) } = { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } )
81 80 imaeq2d 
 |-  ( ph -> ( `' J " { ( 0g ` ( ( mulGrp ` K ) |`s U ) ) } ) = ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) )
82 38 81 eqtr2d 
 |-  ( ph -> ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) = ( ( RSpan ` ZZring ) ` { R } ) )
83 82 oveq2d 
 |-  ( ph -> ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) = ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) )
84 83 eceq2d 
 |-  ( ph -> [ d ] ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) = [ d ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) )
85 84 mpteq2dv 
 |-  ( ph -> ( d e. ZZ |-> [ d ] ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) = ( d e. ZZ |-> [ d ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) )
86 eqid 
 |-  ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) = ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) )
87 eqid 
 |-  ( Z/nZ ` R ) = ( Z/nZ ` R )
88 37 86 87 13 znzrh2 
 |-  ( R e. NN0 -> L = ( d e. ZZ |-> [ d ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) )
89 52 88 syl 
 |-  ( ph -> L = ( d e. ZZ |-> [ d ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) )
90 89 eqcomd 
 |-  ( ph -> ( d e. ZZ |-> [ d ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) = L )
91 85 90 eqtrd 
 |-  ( ph -> ( d e. ZZ |-> [ d ] ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) = L )
92 91 coeq2d 
 |-  ( ph -> ( X o. ( d e. ZZ |-> [ d ] ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) = ( X o. L ) )
93 36 92 eqtrd 
 |-  ( ph -> J = ( X o. L ) )
94 93 coeq2d 
 |-  ( ph -> ( `' X o. J ) = ( `' X o. ( X o. L ) ) )
95 coass 
 |-  ( ( `' X o. X ) o. L ) = ( `' X o. ( X o. L ) )
96 95 eqcomi 
 |-  ( `' X o. ( X o. L ) ) = ( ( `' X o. X ) o. L )
97 94 96 eqtrdi 
 |-  ( ph -> ( `' X o. J ) = ( ( `' X o. X ) o. L ) )
98 77 58 ressbas2 
 |-  ( ran J C_ ( Base ` ( ( mulGrp ` K ) |`s U ) ) -> ran J = ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) )
99 76 98 syl 
 |-  ( ph -> ran J = ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) )
100 23 28 29 30 22 99 ghmqusker 
 |-  ( ph -> X e. ( ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) GrpIso ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) )
101 eqid 
 |-  ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) = ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) )
102 eqid 
 |-  ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) = ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) )
103 101 102 gimf1o 
 |-  ( X e. ( ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) GrpIso ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) -> X : ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) -1-1-onto-> ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) )
104 100 103 syl 
 |-  ( ph -> X : ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) -1-1-onto-> ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) )
105 f1ococnv1 
 |-  ( X : ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) -1-1-onto-> ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) -> ( `' X o. X ) = ( _I |` ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) ) )
106 104 105 syl 
 |-  ( ph -> ( `' X o. X ) = ( _I |` ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) ) )
107 106 coeq1d 
 |-  ( ph -> ( ( `' X o. X ) o. L ) = ( ( _I |` ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) ) o. L ) )
108 87 zncrng 
 |-  ( R e. NN0 -> ( Z/nZ ` R ) e. CRing )
109 52 108 syl 
 |-  ( ph -> ( Z/nZ ` R ) e. CRing )
110 crngring 
 |-  ( ( Z/nZ ` R ) e. CRing -> ( Z/nZ ` R ) e. Ring )
111 13 zrhrhm 
 |-  ( ( Z/nZ ` R ) e. Ring -> L e. ( ZZring RingHom ( Z/nZ ` R ) ) )
112 eqid 
 |-  ( Base ` ( Z/nZ ` R ) ) = ( Base ` ( Z/nZ ` R ) )
113 31 112 rhmf 
 |-  ( L e. ( ZZring RingHom ( Z/nZ ` R ) ) -> L : ZZ --> ( Base ` ( Z/nZ ` R ) ) )
114 109 110 111 113 4syl 
 |-  ( ph -> L : ZZ --> ( Base ` ( Z/nZ ` R ) ) )
115 eqid 
 |-  ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) = ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) )
116 37 115 87 znbas2 
 |-  ( R e. NN0 -> ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) ) = ( Base ` ( Z/nZ ` R ) ) )
117 52 116 syl 
 |-  ( ph -> ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) ) = ( Base ` ( Z/nZ ` R ) ) )
118 117 feq3d 
 |-  ( ph -> ( L : ZZ --> ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) ) <-> L : ZZ --> ( Base ` ( Z/nZ ` R ) ) ) )
119 114 118 mpbird 
 |-  ( ph -> L : ZZ --> ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) ) )
120 82 eqcomd 
 |-  ( ph -> ( ( RSpan ` ZZring ) ` { R } ) = ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) )
121 120 oveq2d 
 |-  ( ph -> ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) = ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) )
122 121 oveq2d 
 |-  ( ph -> ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) = ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) )
123 122 fveq2d 
 |-  ( ph -> ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) ) = ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) )
124 123 feq3d 
 |-  ( ph -> ( L : ZZ --> ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { R } ) ) ) ) <-> L : ZZ --> ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) ) )
125 119 124 mpbid 
 |-  ( ph -> L : ZZ --> ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) )
126 fcoi2 
 |-  ( L : ZZ --> ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) -> ( ( _I |` ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) ) o. L ) = L )
127 125 126 syl 
 |-  ( ph -> ( ( _I |` ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) ) o. L ) = L )
128 107 127 eqtrd 
 |-  ( ph -> ( ( `' X o. X ) o. L ) = L )
129 97 128 eqtr2d 
 |-  ( ph -> L = ( `' X o. J ) )
130 129 imaeq1d 
 |-  ( ph -> ( L " ( E " ( NN0 X. NN0 ) ) ) = ( ( `' X o. J ) " ( E " ( NN0 X. NN0 ) ) ) )
131 imaco 
 |-  ( ( `' X o. J ) " ( E " ( NN0 X. NN0 ) ) ) = ( `' X " ( J " ( E " ( NN0 X. NN0 ) ) ) )
132 131 a1i 
 |-  ( ph -> ( ( `' X o. J ) " ( E " ( NN0 X. NN0 ) ) ) = ( `' X " ( J " ( E " ( NN0 X. NN0 ) ) ) ) )
133 130 132 eqtrd 
 |-  ( ph -> ( L " ( E " ( NN0 X. NN0 ) ) ) = ( `' X " ( J " ( E " ( NN0 X. NN0 ) ) ) ) )
134 133 fveq2d 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) = ( # ` ( `' X " ( J " ( E " ( NN0 X. NN0 ) ) ) ) ) )
135 simplll 
 |-  ( ( ( ( ph /\ w e. ( J " ZZ ) ) /\ u e. ZZ ) /\ ( J ` u ) = w ) -> ph )
136 simplr 
 |-  ( ( ( ( ph /\ w e. ( J " ZZ ) ) /\ u e. ZZ ) /\ ( J ` u ) = w ) -> u e. ZZ )
137 135 136 jca 
 |-  ( ( ( ( ph /\ w e. ( J " ZZ ) ) /\ u e. ZZ ) /\ ( J ` u ) = w ) -> ( ph /\ u e. ZZ ) )
138 simplr 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> z e. ( 0 ... ( R - 1 ) ) )
139 simpr 
 |-  ( ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) /\ v = z ) -> v = z )
140 139 fveqeq2d 
 |-  ( ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) /\ v = z ) -> ( ( J ` v ) = ( J ` u ) <-> ( J ` z ) = ( J ` u ) ) )
141 20 a1i 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> J = ( j e. ZZ |-> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
142 simpr 
 |-  ( ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) /\ j = z ) -> j = z )
143 142 oveq1d 
 |-  ( ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) /\ j = z ) -> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
144 fzssz 
 |-  ( 0 ... ( R - 1 ) ) C_ ZZ
145 144 138 sselid 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> z e. ZZ )
146 ovexd 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) e. _V )
147 141 143 145 146 fvmptd 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> ( J ` z ) = ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
148 simpr 
 |-  ( ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) /\ j = u ) -> j = u )
149 148 oveq1d 
 |-  ( ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) /\ j = u ) -> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( u ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
150 simpr 
 |-  ( ( ph /\ u e. ZZ ) -> u e. ZZ )
151 150 ad3antrrr 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> u e. ZZ )
152 ovexd 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> ( u ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) e. _V )
153 141 149 151 152 fvmptd 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> ( J ` u ) = ( u ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
154 simpr 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> u = ( ( y x. R ) + z ) )
155 154 oveq1d 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> ( u ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( ( ( y x. R ) + z ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
156 41 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( ( mulGrp ` K ) |`s U ) e. Grp )
157 simplr 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> y e. ZZ )
158 5 adantr 
 |-  ( ( ph /\ u e. ZZ ) -> R e. NN )
159 158 ad2antrr 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> R e. NN )
160 159 nnzd 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> R e. ZZ )
161 157 160 zmulcld 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( y x. R ) e. ZZ )
162 144 sseli 
 |-  ( z e. ( 0 ... ( R - 1 ) ) -> z e. ZZ )
163 162 adantl 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> z e. ZZ )
164 57 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) )
165 161 163 164 3jca 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( ( y x. R ) e. ZZ /\ z e. ZZ /\ M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) ) )
166 eqid 
 |-  ( +g ` ( ( mulGrp ` K ) |`s U ) ) = ( +g ` ( ( mulGrp ` K ) |`s U ) )
167 58 53 166 mulgdir 
 |-  ( ( ( ( mulGrp ` K ) |`s U ) e. Grp /\ ( ( y x. R ) e. ZZ /\ z e. ZZ /\ M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) ) ) -> ( ( ( y x. R ) + z ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( ( ( y x. R ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ( +g ` ( ( mulGrp ` K ) |`s U ) ) ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
168 156 165 167 syl2anc 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( ( ( y x. R ) + z ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( ( ( y x. R ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ( +g ` ( ( mulGrp ` K ) |`s U ) ) ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
169 157 160 164 3jca 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( y e. ZZ /\ R e. ZZ /\ M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) ) )
170 58 53 mulgass 
 |-  ( ( ( ( mulGrp ` K ) |`s U ) e. Grp /\ ( y e. ZZ /\ R e. ZZ /\ M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) ) ) -> ( ( y x. R ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( y ( .g ` ( ( mulGrp ` K ) |`s U ) ) ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
171 156 169 170 syl2anc 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( ( y x. R ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( y ( .g ` ( ( mulGrp ` K ) |`s U ) ) ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
172 56 simp2d 
 |-  ( ph -> ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
173 172 adantr 
 |-  ( ( ph /\ u e. ZZ ) -> ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
174 173 adantr 
 |-  ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) -> ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
175 174 adantr 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
176 175 oveq2d 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( y ( .g ` ( ( mulGrp ` K ) |`s U ) ) ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) = ( y ( .g ` ( ( mulGrp ` K ) |`s U ) ) ( 0g ` ( ( mulGrp ` K ) |`s U ) ) ) )
177 58 53 59 mulgz 
 |-  ( ( ( ( mulGrp ` K ) |`s U ) e. Grp /\ y e. ZZ ) -> ( y ( .g ` ( ( mulGrp ` K ) |`s U ) ) ( 0g ` ( ( mulGrp ` K ) |`s U ) ) ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
178 156 157 177 syl2anc 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( y ( .g ` ( ( mulGrp ` K ) |`s U ) ) ( 0g ` ( ( mulGrp ` K ) |`s U ) ) ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
179 176 178 eqtrd 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( y ( .g ` ( ( mulGrp ` K ) |`s U ) ) ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
180 171 179 eqtrd 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( ( y x. R ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) )
181 180 oveq1d 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( ( ( y x. R ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ( +g ` ( ( mulGrp ` K ) |`s U ) ) ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) = ( ( 0g ` ( ( mulGrp ` K ) |`s U ) ) ( +g ` ( ( mulGrp ` K ) |`s U ) ) ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
182 58 53 156 163 164 mulgcld 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) )
183 58 166 59 156 182 grplidd 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( ( 0g ` ( ( mulGrp ` K ) |`s U ) ) ( +g ` ( ( mulGrp ` K ) |`s U ) ) ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) = ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
184 181 183 eqtrd 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( ( ( y x. R ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ( +g ` ( ( mulGrp ` K ) |`s U ) ) ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) = ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
185 168 184 eqtrd 
 |-  ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) -> ( ( ( y x. R ) + z ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
186 185 adantr 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> ( ( ( y x. R ) + z ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
187 155 186 eqtrd 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> ( u ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
188 153 187 eqtr2d 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> ( z ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( J ` u ) )
189 147 188 eqtrd 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> ( J ` z ) = ( J ` u ) )
190 138 140 189 rspcedvd 
 |-  ( ( ( ( ( ph /\ u e. ZZ ) /\ y e. ZZ ) /\ z e. ( 0 ... ( R - 1 ) ) ) /\ u = ( ( y x. R ) + z ) ) -> E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = ( J ` u ) )
191 150 158 remexz 
 |-  ( ( ph /\ u e. ZZ ) -> E. y e. ZZ E. z e. ( 0 ... ( R - 1 ) ) u = ( ( y x. R ) + z ) )
192 190 191 r19.29vva 
 |-  ( ( ph /\ u e. ZZ ) -> E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = ( J ` u ) )
193 137 192 syl 
 |-  ( ( ( ( ph /\ w e. ( J " ZZ ) ) /\ u e. ZZ ) /\ ( J ` u ) = w ) -> E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = ( J ` u ) )
194 simpr 
 |-  ( ( ( ( ph /\ w e. ( J " ZZ ) ) /\ u e. ZZ ) /\ ( J ` u ) = w ) -> ( J ` u ) = w )
195 194 eqcomd 
 |-  ( ( ( ( ph /\ w e. ( J " ZZ ) ) /\ u e. ZZ ) /\ ( J ` u ) = w ) -> w = ( J ` u ) )
196 195 eqeq2d 
 |-  ( ( ( ( ph /\ w e. ( J " ZZ ) ) /\ u e. ZZ ) /\ ( J ` u ) = w ) -> ( ( J ` v ) = w <-> ( J ` v ) = ( J ` u ) ) )
197 196 rexbidv 
 |-  ( ( ( ( ph /\ w e. ( J " ZZ ) ) /\ u e. ZZ ) /\ ( J ` u ) = w ) -> ( E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = w <-> E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = ( J ` u ) ) )
198 193 197 mpbird 
 |-  ( ( ( ( ph /\ w e. ( J " ZZ ) ) /\ u e. ZZ ) /\ ( J ` u ) = w ) -> E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = w )
199 ssidd 
 |-  ( ph -> ZZ C_ ZZ )
200 fvelimab 
 |-  ( ( J Fn ZZ /\ ZZ C_ ZZ ) -> ( w e. ( J " ZZ ) <-> E. u e. ZZ ( J ` u ) = w ) )
201 72 199 200 syl2anc 
 |-  ( ph -> ( w e. ( J " ZZ ) <-> E. u e. ZZ ( J ` u ) = w ) )
202 201 biimpd 
 |-  ( ph -> ( w e. ( J " ZZ ) -> E. u e. ZZ ( J ` u ) = w ) )
203 202 imp 
 |-  ( ( ph /\ w e. ( J " ZZ ) ) -> E. u e. ZZ ( J ` u ) = w )
204 198 203 r19.29a 
 |-  ( ( ph /\ w e. ( J " ZZ ) ) -> E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = w )
205 144 a1i 
 |-  ( ph -> ( 0 ... ( R - 1 ) ) C_ ZZ )
206 fvelimab 
 |-  ( ( J Fn ZZ /\ ( 0 ... ( R - 1 ) ) C_ ZZ ) -> ( w e. ( J " ( 0 ... ( R - 1 ) ) ) <-> E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = w ) )
207 72 205 206 syl2anc 
 |-  ( ph -> ( w e. ( J " ( 0 ... ( R - 1 ) ) ) <-> E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = w ) )
208 207 adantr 
 |-  ( ( ph /\ w e. ( J " ZZ ) ) -> ( w e. ( J " ( 0 ... ( R - 1 ) ) ) <-> E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = w ) )
209 204 208 mpbird 
 |-  ( ( ph /\ w e. ( J " ZZ ) ) -> w e. ( J " ( 0 ... ( R - 1 ) ) ) )
210 209 ex 
 |-  ( ph -> ( w e. ( J " ZZ ) -> w e. ( J " ( 0 ... ( R - 1 ) ) ) ) )
211 210 ssrdv 
 |-  ( ph -> ( J " ZZ ) C_ ( J " ( 0 ... ( R - 1 ) ) ) )
212 207 biimpd 
 |-  ( ph -> ( w e. ( J " ( 0 ... ( R - 1 ) ) ) -> E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = w ) )
213 212 imp 
 |-  ( ( ph /\ w e. ( J " ( 0 ... ( R - 1 ) ) ) ) -> E. v e. ( 0 ... ( R - 1 ) ) ( J ` v ) = w )
214 144 sseli 
 |-  ( v e. ( 0 ... ( R - 1 ) ) -> v e. ZZ )
215 214 adantr 
 |-  ( ( v e. ( 0 ... ( R - 1 ) ) /\ ( J ` v ) = w ) -> v e. ZZ )
216 215 adantl 
 |-  ( ( ( ph /\ w e. ( J " ( 0 ... ( R - 1 ) ) ) ) /\ ( v e. ( 0 ... ( R - 1 ) ) /\ ( J ` v ) = w ) ) -> v e. ZZ )
217 simprr 
 |-  ( ( ( ph /\ w e. ( J " ( 0 ... ( R - 1 ) ) ) ) /\ ( v e. ( 0 ... ( R - 1 ) ) /\ ( J ` v ) = w ) ) -> ( J ` v ) = w )
218 213 216 217 reximssdv 
 |-  ( ( ph /\ w e. ( J " ( 0 ... ( R - 1 ) ) ) ) -> E. v e. ZZ ( J ` v ) = w )
219 72 adantr 
 |-  ( ( ph /\ w e. ( J " ( 0 ... ( R - 1 ) ) ) ) -> J Fn ZZ )
220 ssidd 
 |-  ( ( ph /\ w e. ( J " ( 0 ... ( R - 1 ) ) ) ) -> ZZ C_ ZZ )
221 fvelimab 
 |-  ( ( J Fn ZZ /\ ZZ C_ ZZ ) -> ( w e. ( J " ZZ ) <-> E. v e. ZZ ( J ` v ) = w ) )
222 219 220 221 syl2anc 
 |-  ( ( ph /\ w e. ( J " ( 0 ... ( R - 1 ) ) ) ) -> ( w e. ( J " ZZ ) <-> E. v e. ZZ ( J ` v ) = w ) )
223 218 222 mpbird 
 |-  ( ( ph /\ w e. ( J " ( 0 ... ( R - 1 ) ) ) ) -> w e. ( J " ZZ ) )
224 223 ex 
 |-  ( ph -> ( w e. ( J " ( 0 ... ( R - 1 ) ) ) -> w e. ( J " ZZ ) ) )
225 224 ssrdv 
 |-  ( ph -> ( J " ( 0 ... ( R - 1 ) ) ) C_ ( J " ZZ ) )
226 211 225 eqssd 
 |-  ( ph -> ( J " ZZ ) = ( J " ( 0 ... ( R - 1 ) ) ) )
227 72 fnfund 
 |-  ( ph -> Fun J )
228 fzfid 
 |-  ( ph -> ( 0 ... ( R - 1 ) ) e. Fin )
229 imafi 
 |-  ( ( Fun J /\ ( 0 ... ( R - 1 ) ) e. Fin ) -> ( J " ( 0 ... ( R - 1 ) ) ) e. Fin )
230 227 228 229 syl2anc 
 |-  ( ph -> ( J " ( 0 ... ( R - 1 ) ) ) e. Fin )
231 226 230 eqeltrd 
 |-  ( ph -> ( J " ZZ ) e. Fin )
232 6 4 7 12 aks6d1c2p1 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> NN )
233 nnssz 
 |-  NN C_ ZZ
234 233 a1i 
 |-  ( ph -> NN C_ ZZ )
235 232 234 jca 
 |-  ( ph -> ( E : ( NN0 X. NN0 ) --> NN /\ NN C_ ZZ ) )
236 fss 
 |-  ( ( E : ( NN0 X. NN0 ) --> NN /\ NN C_ ZZ ) -> E : ( NN0 X. NN0 ) --> ZZ )
237 235 236 syl 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> ZZ )
238 237 frnd 
 |-  ( ph -> ran E C_ ZZ )
239 232 ffnd 
 |-  ( ph -> E Fn ( NN0 X. NN0 ) )
240 fnima 
 |-  ( E Fn ( NN0 X. NN0 ) -> ( E " ( NN0 X. NN0 ) ) = ran E )
241 239 240 syl 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) = ran E )
242 241 sseq1d 
 |-  ( ph -> ( ( E " ( NN0 X. NN0 ) ) C_ ZZ <-> ran E C_ ZZ ) )
243 238 242 mpbird 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) C_ ZZ )
244 imass2 
 |-  ( ( E " ( NN0 X. NN0 ) ) C_ ZZ -> ( J " ( E " ( NN0 X. NN0 ) ) ) C_ ( J " ZZ ) )
245 243 244 syl 
 |-  ( ph -> ( J " ( E " ( NN0 X. NN0 ) ) ) C_ ( J " ZZ ) )
246 231 245 ssfid 
 |-  ( ph -> ( J " ( E " ( NN0 X. NN0 ) ) ) e. Fin )
247 dff1o2 
 |-  ( X : ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) -1-1-onto-> ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) <-> ( X Fn ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) /\ Fun `' X /\ ran X = ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) ) )
248 247 biimpi 
 |-  ( X : ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) -1-1-onto-> ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) -> ( X Fn ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) /\ Fun `' X /\ ran X = ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) ) )
249 248 simp2d 
 |-  ( X : ( Base ` ( ZZring /s ( ZZring ~QG ( `' J " { ( 0g ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) } ) ) ) ) -1-1-onto-> ( Base ` ( ( ( mulGrp ` K ) |`s U ) |`s ran J ) ) -> Fun `' X )
250 104 249 syl 
 |-  ( ph -> Fun `' X )
251 imadomfi 
 |-  ( ( ( J " ( E " ( NN0 X. NN0 ) ) ) e. Fin /\ Fun `' X ) -> ( `' X " ( J " ( E " ( NN0 X. NN0 ) ) ) ) ~<_ ( J " ( E " ( NN0 X. NN0 ) ) ) )
252 246 250 251 syl2anc 
 |-  ( ph -> ( `' X " ( J " ( E " ( NN0 X. NN0 ) ) ) ) ~<_ ( J " ( E " ( NN0 X. NN0 ) ) ) )
253 hashdomi 
 |-  ( ( `' X " ( J " ( E " ( NN0 X. NN0 ) ) ) ) ~<_ ( J " ( E " ( NN0 X. NN0 ) ) ) -> ( # ` ( `' X " ( J " ( E " ( NN0 X. NN0 ) ) ) ) ) <_ ( # ` ( J " ( E " ( NN0 X. NN0 ) ) ) ) )
254 252 253 syl 
 |-  ( ph -> ( # ` ( `' X " ( J " ( E " ( NN0 X. NN0 ) ) ) ) ) <_ ( # ` ( J " ( E " ( NN0 X. NN0 ) ) ) ) )
255 134 254 eqbrtrd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( # ` ( J " ( E " ( NN0 X. NN0 ) ) ) ) )
256 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 255 21 aks6d1c6lem4 
 |-  ( ph -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) )