Metamath Proof Explorer

Theorem aks6d1c6isolem1

Description: Lemma to construct the map out of the quotient for AKS. (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 aks6d1c6isolem1 
|- ( ph -> ( ( R |`s U ) |`s ran F ) e. Grp )

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 eqidd 
 |-  ( ph -> ( ( R |`s U ) |`s ran F ) = ( ( R |`s U ) |`s ran F ) )
7 eqidd 
 |-  ( ph -> ( 0g ` ( R |`s U ) ) = ( 0g ` ( R |`s U ) ) )
8 eqidd 
 |-  ( ph -> ( +g ` ( R |`s U ) ) = ( +g ` ( R |`s U ) ) )
9 eqid 
 |-  ( Base ` ( R |`s U ) ) = ( Base ` ( R |`s U ) )
10 eqid 
 |-  ( .g ` ( R |`s U ) ) = ( .g ` ( R |`s U ) )
11 1 2 3 primrootsunit 
 |-  ( ph -> ( ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) /\ ( R |`s U ) e. Abel ) )
12 11 simprd 
 |-  ( ph -> ( R |`s U ) e. Abel )
13 12 ablgrpd 
 |-  ( ph -> ( R |`s U ) e. Grp )
14 13 adantr 
 |-  ( ( ph /\ x e. ZZ ) -> ( R |`s U ) e. Grp )
15 simpr 
 |-  ( ( ph /\ x e. ZZ ) -> x e. ZZ )
16 11 simpld 
 |-  ( ph -> ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) )
17 5 16 eleqtrd 
 |-  ( ph -> M e. ( ( R |`s U ) PrimRoots K ) )
18 12 ablcmnd 
 |-  ( ph -> ( R |`s U ) e. CMnd )
19 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
20 18 19 10 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 ) ) ) )
21 20 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 ) ) ) )
22 17 21 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 ) ) )
23 22 simp1d 
 |-  ( ph -> M e. ( Base ` ( R |`s U ) ) )
24 23 adantr 
 |-  ( ( ph /\ x e. ZZ ) -> M e. ( Base ` ( R |`s U ) ) )
25 9 10 14 15 24 mulgcld 
 |-  ( ( ph /\ x e. ZZ ) -> ( x ( .g ` ( R |`s U ) ) M ) e. ( Base ` ( R |`s U ) ) )
26 25 4 fmptd 
 |-  ( ph -> F : ZZ --> ( Base ` ( R |`s U ) ) )
27 frn 
 |-  ( F : ZZ --> ( Base ` ( R |`s U ) ) -> ran F C_ ( Base ` ( R |`s U ) ) )
28 26 27 syl 
 |-  ( ph -> ran F C_ ( Base ` ( R |`s U ) ) )
29 0zd 
 |-  ( ph -> 0 e. ZZ )
30 simpr 
 |-  ( ( ph /\ c = 0 ) -> c = 0 )
31 30 fveqeq2d 
 |-  ( ( ph /\ c = 0 ) -> ( ( F ` c ) = ( 0g ` ( R |`s U ) ) <-> ( F ` 0 ) = ( 0g ` ( R |`s U ) ) ) )
32 4 a1i 
 |-  ( ph -> F = ( x e. ZZ |-> ( x ( .g ` ( R |`s U ) ) M ) ) )
33 simpr 
 |-  ( ( ph /\ x = 0 ) -> x = 0 )
34 33 oveq1d 
 |-  ( ( ph /\ x = 0 ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( 0 ( .g ` ( R |`s U ) ) M ) )
35 eqid 
 |-  ( 0g ` ( R |`s U ) ) = ( 0g ` ( R |`s U ) )
36 9 35 10 mulg0 
 |-  ( M e. ( Base ` ( R |`s U ) ) -> ( 0 ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
37 23 36 syl 
 |-  ( ph -> ( 0 ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
38 37 adantr 
 |-  ( ( ph /\ x = 0 ) -> ( 0 ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
39 34 38 eqtrd 
 |-  ( ( ph /\ x = 0 ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
40 fvexd 
 |-  ( ph -> ( 0g ` ( R |`s U ) ) e. _V )
41 32 39 29 40 fvmptd 
 |-  ( ph -> ( F ` 0 ) = ( 0g ` ( R |`s U ) ) )
42 29 31 41 rspcedvd 
 |-  ( ph -> E. c e. ZZ ( F ` c ) = ( 0g ` ( R |`s U ) ) )
43 26 ffnd 
 |-  ( ph -> F Fn ZZ )
44 fvelrnb 
 |-  ( F Fn ZZ -> ( ( 0g ` ( R |`s U ) ) e. ran F <-> E. c e. ZZ ( F ` c ) = ( 0g ` ( R |`s U ) ) ) )
45 43 44 syl 
 |-  ( ph -> ( ( 0g ` ( R |`s U ) ) e. ran F <-> E. c e. ZZ ( F ` c ) = ( 0g ` ( R |`s U ) ) ) )
46 42 45 mpbird 
 |-  ( ph -> ( 0g ` ( R |`s U ) ) e. ran F )
47 fvelrnb 
 |-  ( F Fn ZZ -> ( y e. ran F <-> E. d e. ZZ ( F ` d ) = y ) )
48 43 47 syl 
 |-  ( ph -> ( y e. ran F <-> E. d e. ZZ ( F ` d ) = y ) )
49 48 biimpd 
 |-  ( ph -> ( y e. ran F -> E. d e. ZZ ( F ` d ) = y ) )
50 49 imp 
 |-  ( ( ph /\ y e. ran F ) -> E. d e. ZZ ( F ` d ) = y )
51 50 3adant3 
 |-  ( ( ph /\ y e. ran F /\ z e. ran F ) -> E. d e. ZZ ( F ` d ) = y )
52 simpl1 
 |-  ( ( ( ph /\ y e. ran F /\ z e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) -> ph )
53 simpl3 
 |-  ( ( ( ph /\ y e. ran F /\ z e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) -> z e. ran F )
54 52 53 jca 
 |-  ( ( ( ph /\ y e. ran F /\ z e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) -> ( ph /\ z e. ran F ) )
55 fvelrnb 
 |-  ( F Fn ZZ -> ( z e. ran F <-> E. e e. ZZ ( F ` e ) = z ) )
56 43 55 syl 
 |-  ( ph -> ( z e. ran F <-> E. e e. ZZ ( F ` e ) = z ) )
57 56 biimpd 
 |-  ( ph -> ( z e. ran F -> E. e e. ZZ ( F ` e ) = z ) )
58 57 imp 
 |-  ( ( ph /\ z e. ran F ) -> E. e e. ZZ ( F ` e ) = z )
59 54 58 syl 
 |-  ( ( ( ph /\ y e. ran F /\ z e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) -> E. e e. ZZ ( F ` e ) = z )
60 simpll1 
 |-  ( ( ( ( ph /\ y e. ran F /\ z e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) /\ E. e e. ZZ ( F ` e ) = z ) -> ph )
61 simplr 
 |-  ( ( ( ( ph /\ y e. ran F /\ z e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) /\ E. e e. ZZ ( F ` e ) = z ) -> E. d e. ZZ ( F ` d ) = y )
62 simpr 
 |-  ( ( ( ( ph /\ y e. ran F /\ z e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) /\ E. e e. ZZ ( F ` e ) = z ) -> E. e e. ZZ ( F ` e ) = z )
63 60 61 62 3jca 
 |-  ( ( ( ( ph /\ y e. ran F /\ z e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) /\ E. e e. ZZ ( F ` e ) = z ) -> ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) )
64 simpr 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ ( F ` g ) = z ) -> ( F ` g ) = z )
65 64 eqcomd 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ ( F ` g ) = z ) -> z = ( F ` g ) )
66 65 oveq2d 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ ( F ` g ) = z ) -> ( y ( +g ` ( R |`s U ) ) z ) = ( y ( +g ` ( R |`s U ) ) ( F ` g ) ) )
67 simpr 
 |-  ( ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ( F ` f ) = y )
68 67 eqcomd 
 |-  ( ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> y = ( F ` f ) )
69 68 oveq1d 
 |-  ( ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ( y ( +g ` ( R |`s U ) ) ( F ` g ) ) = ( ( F ` f ) ( +g ` ( R |`s U ) ) ( F ` g ) ) )
70 simpll1 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ f e. ZZ ) -> ph )
71 70 adantr 
 |-  ( ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ph )
72 simpllr 
 |-  ( ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> g e. ZZ )
73 simplr 
 |-  ( ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> f e. ZZ )
74 71 72 73 3jca 
 |-  ( ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ( ph /\ g e. ZZ /\ f e. ZZ ) )
75 4 a1i 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> F = ( x e. ZZ |-> ( x ( .g ` ( R |`s U ) ) M ) ) )
76 simpr 
 |-  ( ( ( ph /\ g e. ZZ /\ f e. ZZ ) /\ x = f ) -> x = f )
77 76 oveq1d 
 |-  ( ( ( ph /\ g e. ZZ /\ f e. ZZ ) /\ x = f ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( f ( .g ` ( R |`s U ) ) M ) )
78 simp3 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> f e. ZZ )
79 ovexd 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( f ( .g ` ( R |`s U ) ) M ) e. _V )
80 75 77 78 79 fvmptd 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( F ` f ) = ( f ( .g ` ( R |`s U ) ) M ) )
81 simpr 
 |-  ( ( ( ph /\ g e. ZZ /\ f e. ZZ ) /\ x = g ) -> x = g )
82 81 oveq1d 
 |-  ( ( ( ph /\ g e. ZZ /\ f e. ZZ ) /\ x = g ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( g ( .g ` ( R |`s U ) ) M ) )
83 simp2 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> g e. ZZ )
84 ovexd 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( g ( .g ` ( R |`s U ) ) M ) e. _V )
85 75 82 83 84 fvmptd 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( F ` g ) = ( g ( .g ` ( R |`s U ) ) M ) )
86 80 85 oveq12d 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( ( F ` f ) ( +g ` ( R |`s U ) ) ( F ` g ) ) = ( ( f ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( g ( .g ` ( R |`s U ) ) M ) ) )
87 13 3ad2ant1 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( R |`s U ) e. Grp )
88 23 3ad2ant1 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> M e. ( Base ` ( R |`s U ) ) )
89 78 83 88 3jca 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( f e. ZZ /\ g e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) )
90 eqid 
 |-  ( +g ` ( R |`s U ) ) = ( +g ` ( R |`s U ) )
91 9 10 90 mulgdir 
 |-  ( ( ( R |`s U ) e. Grp /\ ( f e. ZZ /\ g e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) ) -> ( ( f + g ) ( .g ` ( R |`s U ) ) M ) = ( ( f ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( g ( .g ` ( R |`s U ) ) M ) ) )
92 87 89 91 syl2anc 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( ( f + g ) ( .g ` ( R |`s U ) ) M ) = ( ( f ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( g ( .g ` ( R |`s U ) ) M ) ) )
93 78 83 zaddcld 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( f + g ) e. ZZ )
94 simpr 
 |-  ( ( ( ph /\ g e. ZZ /\ f e. ZZ ) /\ h = ( f + g ) ) -> h = ( f + g ) )
95 94 fveqeq2d 
 |-  ( ( ( ph /\ g e. ZZ /\ f e. ZZ ) /\ h = ( f + g ) ) -> ( ( F ` h ) = ( ( f + g ) ( .g ` ( R |`s U ) ) M ) <-> ( F ` ( f + g ) ) = ( ( f + g ) ( .g ` ( R |`s U ) ) M ) ) )
96 simpr 
 |-  ( ( ( ph /\ g e. ZZ /\ f e. ZZ ) /\ x = ( f + g ) ) -> x = ( f + g ) )
97 96 oveq1d 
 |-  ( ( ( ph /\ g e. ZZ /\ f e. ZZ ) /\ x = ( f + g ) ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( ( f + g ) ( .g ` ( R |`s U ) ) M ) )
98 ovexd 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( ( f + g ) ( .g ` ( R |`s U ) ) M ) e. _V )
99 75 97 93 98 fvmptd 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( F ` ( f + g ) ) = ( ( f + g ) ( .g ` ( R |`s U ) ) M ) )
100 93 95 99 rspcedvd 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> E. h e. ZZ ( F ` h ) = ( ( f + g ) ( .g ` ( R |`s U ) ) M ) )
101 fvelrnb 
 |-  ( F Fn ZZ -> ( ( ( f + g ) ( .g ` ( R |`s U ) ) M ) e. ran F <-> E. h e. ZZ ( F ` h ) = ( ( f + g ) ( .g ` ( R |`s U ) ) M ) ) )
102 43 101 syl 
 |-  ( ph -> ( ( ( f + g ) ( .g ` ( R |`s U ) ) M ) e. ran F <-> E. h e. ZZ ( F ` h ) = ( ( f + g ) ( .g ` ( R |`s U ) ) M ) ) )
103 102 3ad2ant1 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( ( ( f + g ) ( .g ` ( R |`s U ) ) M ) e. ran F <-> E. h e. ZZ ( F ` h ) = ( ( f + g ) ( .g ` ( R |`s U ) ) M ) ) )
104 100 103 mpbird 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( ( f + g ) ( .g ` ( R |`s U ) ) M ) e. ran F )
105 92 104 eqeltrrd 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( ( f ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( g ( .g ` ( R |`s U ) ) M ) ) e. ran F )
106 86 105 eqeltrd 
 |-  ( ( ph /\ g e. ZZ /\ f e. ZZ ) -> ( ( F ` f ) ( +g ` ( R |`s U ) ) ( F ` g ) ) e. ran F )
107 74 106 syl 
 |-  ( ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ( ( F ` f ) ( +g ` ( R |`s U ) ) ( F ` g ) ) e. ran F )
108 69 107 eqeltrd 
 |-  ( ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ( y ( +g ` ( R |`s U ) ) ( F ` g ) ) e. ran F )
109 simpl2 
 |-  ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) -> E. d e. ZZ ( F ` d ) = y )
110 nfv 
 |-  F/ f ( F ` d ) = y
111 nfv 
 |-  F/ d ( F ` f ) = y
112 fveqeq2 
 |-  ( d = f -> ( ( F ` d ) = y <-> ( F ` f ) = y ) )
113 110 111 112 cbvrexw 
 |-  ( E. d e. ZZ ( F ` d ) = y <-> E. f e. ZZ ( F ` f ) = y )
114 113 biimpi 
 |-  ( E. d e. ZZ ( F ` d ) = y -> E. f e. ZZ ( F ` f ) = y )
115 109 114 syl 
 |-  ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) -> E. f e. ZZ ( F ` f ) = y )
116 108 115 r19.29a 
 |-  ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) -> ( y ( +g ` ( R |`s U ) ) ( F ` g ) ) e. ran F )
117 116 adantr 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ ( F ` g ) = z ) -> ( y ( +g ` ( R |`s U ) ) ( F ` g ) ) e. ran F )
118 66 117 eqeltrd 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) /\ g e. ZZ ) /\ ( F ` g ) = z ) -> ( y ( +g ` ( R |`s U ) ) z ) e. ran F )
119 simp3 
 |-  ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) -> E. e e. ZZ ( F ` e ) = z )
120 nfv 
 |-  F/ g ( F ` e ) = z
121 nfv 
 |-  F/ e ( F ` g ) = z
122 fveqeq2 
 |-  ( e = g -> ( ( F ` e ) = z <-> ( F ` g ) = z ) )
123 120 121 122 cbvrexw 
 |-  ( E. e e. ZZ ( F ` e ) = z <-> E. g e. ZZ ( F ` g ) = z )
124 123 biimpi 
 |-  ( E. e e. ZZ ( F ` e ) = z -> E. g e. ZZ ( F ` g ) = z )
125 119 124 syl 
 |-  ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) -> E. g e. ZZ ( F ` g ) = z )
126 118 125 r19.29a 
 |-  ( ( ph /\ E. d e. ZZ ( F ` d ) = y /\ E. e e. ZZ ( F ` e ) = z ) -> ( y ( +g ` ( R |`s U ) ) z ) e. ran F )
127 63 126 syl 
 |-  ( ( ( ( ph /\ y e. ran F /\ z e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) /\ E. e e. ZZ ( F ` e ) = z ) -> ( y ( +g ` ( R |`s U ) ) z ) e. ran F )
128 127 ex 
 |-  ( ( ( ph /\ y e. ran F /\ z e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) -> ( E. e e. ZZ ( F ` e ) = z -> ( y ( +g ` ( R |`s U ) ) z ) e. ran F ) )
129 59 128 mpd 
 |-  ( ( ( ph /\ y e. ran F /\ z e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) -> ( y ( +g ` ( R |`s U ) ) z ) e. ran F )
130 51 129 mpdan 
 |-  ( ( ph /\ y e. ran F /\ z e. ran F ) -> ( y ( +g ` ( R |`s U ) ) z ) e. ran F )
131 simpr 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ( F ` f ) = y )
132 131 eqcomd 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> y = ( F ` f ) )
133 132 fveq2d 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ( ( invg ` ( R |`s U ) ) ` y ) = ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) )
134 simplll 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ph )
135 simplr 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> f e. ZZ )
136 134 135 jca 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ( ph /\ f e. ZZ ) )
137 simpr 
 |-  ( ( ph /\ f e. ZZ ) -> f e. ZZ )
138 137 znegcld 
 |-  ( ( ph /\ f e. ZZ ) -> -u f e. ZZ )
139 simpr 
 |-  ( ( ( ph /\ f e. ZZ ) /\ h = -u f ) -> h = -u f )
140 139 fveqeq2d 
 |-  ( ( ( ph /\ f e. ZZ ) /\ h = -u f ) -> ( ( F ` h ) = ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) <-> ( F ` -u f ) = ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) ) )
141 4 a1i 
 |-  ( ( ph /\ f e. ZZ ) -> F = ( x e. ZZ |-> ( x ( .g ` ( R |`s U ) ) M ) ) )
142 simpr 
 |-  ( ( ( ph /\ f e. ZZ ) /\ x = -u f ) -> x = -u f )
143 142 oveq1d 
 |-  ( ( ( ph /\ f e. ZZ ) /\ x = -u f ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( -u f ( .g ` ( R |`s U ) ) M ) )
144 ovexd 
 |-  ( ( ph /\ f e. ZZ ) -> ( -u f ( .g ` ( R |`s U ) ) M ) e. _V )
145 141 143 138 144 fvmptd 
 |-  ( ( ph /\ f e. ZZ ) -> ( F ` -u f ) = ( -u f ( .g ` ( R |`s U ) ) M ) )
146 13 adantr 
 |-  ( ( ph /\ f e. ZZ ) -> ( R |`s U ) e. Grp )
147 23 adantr 
 |-  ( ( ph /\ f e. ZZ ) -> M e. ( Base ` ( R |`s U ) ) )
148 eqid 
 |-  ( invg ` ( R |`s U ) ) = ( invg ` ( R |`s U ) )
149 9 10 148 mulgneg 
 |-  ( ( ( R |`s U ) e. Grp /\ f e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) -> ( -u f ( .g ` ( R |`s U ) ) M ) = ( ( invg ` ( R |`s U ) ) ` ( f ( .g ` ( R |`s U ) ) M ) ) )
150 146 137 147 149 syl3anc 
 |-  ( ( ph /\ f e. ZZ ) -> ( -u f ( .g ` ( R |`s U ) ) M ) = ( ( invg ` ( R |`s U ) ) ` ( f ( .g ` ( R |`s U ) ) M ) ) )
151 simpr 
 |-  ( ( ( ph /\ f e. ZZ ) /\ x = f ) -> x = f )
152 151 oveq1d 
 |-  ( ( ( ph /\ f e. ZZ ) /\ x = f ) -> ( x ( .g ` ( R |`s U ) ) M ) = ( f ( .g ` ( R |`s U ) ) M ) )
153 ovexd 
 |-  ( ( ph /\ f e. ZZ ) -> ( f ( .g ` ( R |`s U ) ) M ) e. _V )
154 141 152 137 153 fvmptd 
 |-  ( ( ph /\ f e. ZZ ) -> ( F ` f ) = ( f ( .g ` ( R |`s U ) ) M ) )
155 154 eqcomd 
 |-  ( ( ph /\ f e. ZZ ) -> ( f ( .g ` ( R |`s U ) ) M ) = ( F ` f ) )
156 155 fveq2d 
 |-  ( ( ph /\ f e. ZZ ) -> ( ( invg ` ( R |`s U ) ) ` ( f ( .g ` ( R |`s U ) ) M ) ) = ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) )
157 150 156 eqtrd 
 |-  ( ( ph /\ f e. ZZ ) -> ( -u f ( .g ` ( R |`s U ) ) M ) = ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) )
158 145 157 eqtrd 
 |-  ( ( ph /\ f e. ZZ ) -> ( F ` -u f ) = ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) )
159 138 140 158 rspcedvd 
 |-  ( ( ph /\ f e. ZZ ) -> E. h e. ZZ ( F ` h ) = ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) )
160 fvelrnb 
 |-  ( F Fn ZZ -> ( ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) e. ran F <-> E. h e. ZZ ( F ` h ) = ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) ) )
161 43 160 syl 
 |-  ( ph -> ( ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) e. ran F <-> E. h e. ZZ ( F ` h ) = ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) ) )
162 161 adantr 
 |-  ( ( ph /\ f e. ZZ ) -> ( ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) e. ran F <-> E. h e. ZZ ( F ` h ) = ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) ) )
163 159 162 mpbird 
 |-  ( ( ph /\ f e. ZZ ) -> ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) e. ran F )
164 163 a1i 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ( ( ph /\ f e. ZZ ) -> ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) e. ran F ) )
165 136 164 mpd 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ( ( invg ` ( R |`s U ) ) ` ( F ` f ) ) e. ran F )
166 133 165 eqeltrd 
 |-  ( ( ( ( ph /\ E. d e. ZZ ( F ` d ) = y ) /\ f e. ZZ ) /\ ( F ` f ) = y ) -> ( ( invg ` ( R |`s U ) ) ` y ) e. ran F )
167 114 adantl 
 |-  ( ( ph /\ E. d e. ZZ ( F ` d ) = y ) -> E. f e. ZZ ( F ` f ) = y )
168 166 167 r19.29a 
 |-  ( ( ph /\ E. d e. ZZ ( F ` d ) = y ) -> ( ( invg ` ( R |`s U ) ) ` y ) e. ran F )
169 168 ex 
 |-  ( ph -> ( E. d e. ZZ ( F ` d ) = y -> ( ( invg ` ( R |`s U ) ) ` y ) e. ran F ) )
170 169 adantr 
 |-  ( ( ph /\ y e. ran F ) -> ( E. d e. ZZ ( F ` d ) = y -> ( ( invg ` ( R |`s U ) ) ` y ) e. ran F ) )
171 170 imp 
 |-  ( ( ( ph /\ y e. ran F ) /\ E. d e. ZZ ( F ` d ) = y ) -> ( ( invg ` ( R |`s U ) ) ` y ) e. ran F )
172 50 171 mpdan 
 |-  ( ( ph /\ y e. ran F ) -> ( ( invg ` ( R |`s U ) ) ` y ) e. ran F )
173 6 7 8 28 46 130 172 13 issubgrpd 
 |-  ( ph -> ( ( R |`s U ) |`s ran F ) e. Grp )