Metamath Proof Explorer

Theorem primrootscoprbij

Description: A bijection between coprime powers of primitive roots and primitive roots. (Contributed by metakunt, 26-Apr-2025)

Ref Expression
Hypotheses primrootscoprbij.1 
|- F = ( m e. ( R PrimRoots K ) |-> ( I ( .g ` R ) m ) )
primrootscoprbij.2 
|- ( ph -> R e. CMnd )
primrootscoprbij.3 
|- ( ph -> K e. NN )
primrootscoprbij.4 
|- ( ph -> I e. NN )
primrootscoprbij.5 
|- ( ph -> J e. NN )
primrootscoprbij.6 
|- ( ph -> Z e. ZZ )
primrootscoprbij.7 
|- ( ph -> 1 = ( ( I x. J ) + ( K x. Z ) ) )
primrootscoprbij.8 
|- U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
Assertion primrootscoprbij 
|- ( ph -> F : ( R PrimRoots K ) -1-1-onto-> ( R PrimRoots K ) )

Proof

Step Hyp Ref Expression
1 primrootscoprbij.1 
 |-  F = ( m e. ( R PrimRoots K ) |-> ( I ( .g ` R ) m ) )
2 primrootscoprbij.2 
 |-  ( ph -> R e. CMnd )
3 primrootscoprbij.3 
 |-  ( ph -> K e. NN )
4 primrootscoprbij.4 
 |-  ( ph -> I e. NN )
5 primrootscoprbij.5 
 |-  ( ph -> J e. NN )
6 primrootscoprbij.6 
 |-  ( ph -> Z e. ZZ )
7 primrootscoprbij.7 
 |-  ( ph -> 1 = ( ( I x. J ) + ( K x. Z ) ) )
8 primrootscoprbij.8 
 |-  U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
9 4 nnzd 
 |-  ( ph -> I e. ZZ )
10 3 nnzd 
 |-  ( ph -> K e. ZZ )
11 5 nnzd 
 |-  ( ph -> J e. ZZ )
12 11 6 jca 
 |-  ( ph -> ( J e. ZZ /\ Z e. ZZ ) )
13 9 10 12 jca31 
 |-  ( ph -> ( ( I e. ZZ /\ K e. ZZ ) /\ ( J e. ZZ /\ Z e. ZZ ) ) )
14 7 eqcomd 
 |-  ( ph -> ( ( I x. J ) + ( K x. Z ) ) = 1 )
15 13 14 jca 
 |-  ( ph -> ( ( ( I e. ZZ /\ K e. ZZ ) /\ ( J e. ZZ /\ Z e. ZZ ) ) /\ ( ( I x. J ) + ( K x. Z ) ) = 1 ) )
16 bezoutr1 
 |-  ( ( ( I e. ZZ /\ K e. ZZ ) /\ ( J e. ZZ /\ Z e. ZZ ) ) -> ( ( ( I x. J ) + ( K x. Z ) ) = 1 -> ( I gcd K ) = 1 ) )
17 16 imp 
 |-  ( ( ( ( I e. ZZ /\ K e. ZZ ) /\ ( J e. ZZ /\ Z e. ZZ ) ) /\ ( ( I x. J ) + ( K x. Z ) ) = 1 ) -> ( I gcd K ) = 1 )
18 15 17 syl 
 |-  ( ph -> ( I gcd K ) = 1 )
19 1 2 3 4 18 primrootscoprf 
 |-  ( ph -> F : ( R PrimRoots K ) --> ( R PrimRoots K ) )
20 eqid 
 |-  ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) = ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) )
21 11 10 jca 
 |-  ( ph -> ( J e. ZZ /\ K e. ZZ ) )
22 9 6 jca 
 |-  ( ph -> ( I e. ZZ /\ Z e. ZZ ) )
23 21 22 jca 
 |-  ( ph -> ( ( J e. ZZ /\ K e. ZZ ) /\ ( I e. ZZ /\ Z e. ZZ ) ) )
24 5 nncnd 
 |-  ( ph -> J e. CC )
25 4 nncnd 
 |-  ( ph -> I e. CC )
26 24 25 mulcomd 
 |-  ( ph -> ( J x. I ) = ( I x. J ) )
27 26 oveq1d 
 |-  ( ph -> ( ( J x. I ) + ( K x. Z ) ) = ( ( I x. J ) + ( K x. Z ) ) )
28 27 14 eqtrd 
 |-  ( ph -> ( ( J x. I ) + ( K x. Z ) ) = 1 )
29 23 28 jca 
 |-  ( ph -> ( ( ( J e. ZZ /\ K e. ZZ ) /\ ( I e. ZZ /\ Z e. ZZ ) ) /\ ( ( J x. I ) + ( K x. Z ) ) = 1 ) )
30 bezoutr1 
 |-  ( ( ( J e. ZZ /\ K e. ZZ ) /\ ( I e. ZZ /\ Z e. ZZ ) ) -> ( ( ( J x. I ) + ( K x. Z ) ) = 1 -> ( J gcd K ) = 1 ) )
31 30 imp 
 |-  ( ( ( ( J e. ZZ /\ K e. ZZ ) /\ ( I e. ZZ /\ Z e. ZZ ) ) /\ ( ( J x. I ) + ( K x. Z ) ) = 1 ) -> ( J gcd K ) = 1 )
32 29 31 syl 
 |-  ( ph -> ( J gcd K ) = 1 )
33 20 2 3 5 32 primrootscoprf 
 |-  ( ph -> ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) : ( R PrimRoots K ) --> ( R PrimRoots K ) )
34 1 a1i 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> F = ( m e. ( R PrimRoots K ) |-> ( I ( .g ` R ) m ) ) )
35 simpr 
 |-  ( ( ( ph /\ x e. ( R PrimRoots K ) ) /\ m = x ) -> m = x )
36 35 oveq2d 
 |-  ( ( ( ph /\ x e. ( R PrimRoots K ) ) /\ m = x ) -> ( I ( .g ` R ) m ) = ( I ( .g ` R ) x ) )
37 simpr 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> x e. ( R PrimRoots K ) )
38 2 cmnmndd 
 |-  ( ph -> R e. Mnd )
39 38 adantr 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> R e. Mnd )
40 4 nnnn0d 
 |-  ( ph -> I e. NN0 )
41 40 adantr 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> I e. NN0 )
42 3 nnnn0d 
 |-  ( ph -> K e. NN0 )
43 eqid 
 |-  ( .g ` R ) = ( .g ` R )
44 2 42 43 isprimroot 
 |-  ( ph -> ( x e. ( R PrimRoots K ) <-> ( x e. ( Base ` R ) /\ ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) ) )
45 44 biimpd 
 |-  ( ph -> ( x e. ( R PrimRoots K ) -> ( x e. ( Base ` R ) /\ ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) ) )
46 45 imp 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( x e. ( Base ` R ) /\ ( K ( .g ` R ) x ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) x ) = ( 0g ` R ) -> K || l ) ) )
47 46 simp1d 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> x e. ( Base ` R ) )
48 eqid 
 |-  ( Base ` R ) = ( Base ` R )
49 48 43 mulgnn0cl 
 |-  ( ( R e. Mnd /\ I e. NN0 /\ x e. ( Base ` R ) ) -> ( I ( .g ` R ) x ) e. ( Base ` R ) )
50 39 41 47 49 syl3anc 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( I ( .g ` R ) x ) e. ( Base ` R ) )
51 34 36 37 50 fvmptd 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( F ` x ) = ( I ( .g ` R ) x ) )
52 51 fveq2d 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) ` ( F ` x ) ) = ( ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) ` ( I ( .g ` R ) x ) ) )
53 eqidd 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) = ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) )
54 simpr 
 |-  ( ( ( ph /\ x e. ( R PrimRoots K ) ) /\ n = ( I ( .g ` R ) x ) ) -> n = ( I ( .g ` R ) x ) )
55 54 oveq2d 
 |-  ( ( ( ph /\ x e. ( R PrimRoots K ) ) /\ n = ( I ( .g ` R ) x ) ) -> ( J ( .g ` R ) n ) = ( J ( .g ` R ) ( I ( .g ` R ) x ) ) )
56 2 adantr 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> R e. CMnd )
57 3 adantr 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> K e. NN )
58 4 adantr 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> I e. NN )
59 18 adantr 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( I gcd K ) = 1 )
60 eqid 
 |-  { s e. ( Base ` R ) | E. t e. ( Base ` R ) ( t ( +g ` R ) s ) = ( 0g ` R ) } = { s e. ( Base ` R ) | E. t e. ( Base ` R ) ( t ( +g ` R ) s ) = ( 0g ` R ) }
61 56 57 58 59 37 60 primrootscoprmpow 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( I ( .g ` R ) x ) e. ( R PrimRoots K ) )
62 5 nnnn0d 
 |-  ( ph -> J e. NN0 )
63 62 adantr 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> J e. NN0 )
64 48 43 mulgnn0cl 
 |-  ( ( R e. Mnd /\ J e. NN0 /\ ( I ( .g ` R ) x ) e. ( Base ` R ) ) -> ( J ( .g ` R ) ( I ( .g ` R ) x ) ) e. ( Base ` R ) )
65 39 63 50 64 syl3anc 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( J ( .g ` R ) ( I ( .g ` R ) x ) ) e. ( Base ` R ) )
66 53 55 61 65 fvmptd 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) ` ( I ( .g ` R ) x ) ) = ( J ( .g ` R ) ( I ( .g ` R ) x ) ) )
67 63 41 47 3jca 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( J e. NN0 /\ I e. NN0 /\ x e. ( Base ` R ) ) )
68 48 43 mulgnn0ass 
 |-  ( ( R e. Mnd /\ ( J e. NN0 /\ I e. NN0 /\ x e. ( Base ` R ) ) ) -> ( ( J x. I ) ( .g ` R ) x ) = ( J ( .g ` R ) ( I ( .g ` R ) x ) ) )
69 39 67 68 syl2anc 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( ( J x. I ) ( .g ` R ) x ) = ( J ( .g ` R ) ( I ( .g ` R ) x ) ) )
70 2 3 8 primrootsunit 
 |-  ( ph -> ( ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) /\ ( R |`s U ) e. Abel ) )
71 70 simpld 
 |-  ( ph -> ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) )
72 71 eleq2d 
 |-  ( ph -> ( x e. ( R PrimRoots K ) <-> x e. ( ( R |`s U ) PrimRoots K ) ) )
73 72 biimpd 
 |-  ( ph -> ( x e. ( R PrimRoots K ) -> x e. ( ( R |`s U ) PrimRoots K ) ) )
74 70 simprd 
 |-  ( ph -> ( R |`s U ) e. Abel )
75 ablgrp 
 |-  ( ( R |`s U ) e. Abel -> ( R |`s U ) e. Grp )
76 74 75 syl 
 |-  ( ph -> ( R |`s U ) e. Grp )
77 grpmnd 
 |-  ( ( R |`s U ) e. Grp -> ( R |`s U ) e. Mnd )
78 76 77 syl 
 |-  ( ph -> ( R |`s U ) e. Mnd )
79 38 78 jca 
 |-  ( ph -> ( R e. Mnd /\ ( R |`s U ) e. Mnd ) )
80 8 a1i 
 |-  ( ph -> U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
81 80 eleq2d 
 |-  ( ph -> ( f e. U <-> f e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
82 81 biimpd 
 |-  ( ph -> ( f e. U -> f e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
83 82 imp 
 |-  ( ( ph /\ f e. U ) -> f e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
84 oveq2 
 |-  ( a = f -> ( i ( +g ` R ) a ) = ( i ( +g ` R ) f ) )
85 84 eqeq1d 
 |-  ( a = f -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( i ( +g ` R ) f ) = ( 0g ` R ) ) )
86 85 rexbidv 
 |-  ( a = f -> ( E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) <-> E. i e. ( Base ` R ) ( i ( +g ` R ) f ) = ( 0g ` R ) ) )
87 86 elrab 
 |-  ( f e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } <-> ( f e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) f ) = ( 0g ` R ) ) )
88 87 biimpi 
 |-  ( f e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } -> ( f e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) f ) = ( 0g ` R ) ) )
89 88 simpld 
 |-  ( f e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } -> f e. ( Base ` R ) )
90 83 89 syl 
 |-  ( ( ph /\ f e. U ) -> f e. ( Base ` R ) )
91 90 ex 
 |-  ( ph -> ( f e. U -> f e. ( Base ` R ) ) )
92 91 ssrdv 
 |-  ( ph -> U C_ ( Base ` R ) )
93 oveq2 
 |-  ( a = ( 0g ` R ) -> ( i ( +g ` R ) a ) = ( i ( +g ` R ) ( 0g ` R ) ) )
94 93 eqeq1d 
 |-  ( a = ( 0g ` R ) -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( i ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
95 94 rexbidv 
 |-  ( a = ( 0g ` R ) -> ( E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) <-> E. i e. ( Base ` R ) ( i ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
96 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
97 48 96 mndidcl 
 |-  ( R e. Mnd -> ( 0g ` R ) e. ( Base ` R ) )
98 38 97 syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
99 simpr 
 |-  ( ( ph /\ i = ( 0g ` R ) ) -> i = ( 0g ` R ) )
100 99 oveq1d 
 |-  ( ( ph /\ i = ( 0g ` R ) ) -> ( i ( +g ` R ) ( 0g ` R ) ) = ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) )
101 100 eqeq1d 
 |-  ( ( ph /\ i = ( 0g ` R ) ) -> ( ( i ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) <-> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
102 eqid 
 |-  ( +g ` R ) = ( +g ` R )
103 48 102 96 mndlid 
 |-  ( ( R e. Mnd /\ ( 0g ` R ) e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
104 38 98 103 syl2anc 
 |-  ( ph -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
105 98 101 104 rspcedvd 
 |-  ( ph -> E. i e. ( Base ` R ) ( i ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
106 95 98 105 elrabd 
 |-  ( ph -> ( 0g ` R ) e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
107 80 eleq2d 
 |-  ( ph -> ( ( 0g ` R ) e. U <-> ( 0g ` R ) e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
108 106 107 mpbird 
 |-  ( ph -> ( 0g ` R ) e. U )
109 92 108 jca 
 |-  ( ph -> ( U C_ ( Base ` R ) /\ ( 0g ` R ) e. U ) )
110 79 109 jca 
 |-  ( ph -> ( ( R e. Mnd /\ ( R |`s U ) e. Mnd ) /\ ( U C_ ( Base ` R ) /\ ( 0g ` R ) e. U ) ) )
111 48 96 issubmndb 
 |-  ( U e. ( SubMnd ` R ) <-> ( ( R e. Mnd /\ ( R |`s U ) e. Mnd ) /\ ( U C_ ( Base ` R ) /\ ( 0g ` R ) e. U ) ) )
112 110 111 sylibr 
 |-  ( ph -> U e. ( SubMnd ` R ) )
113 112 adantr 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> U e. ( SubMnd ` R ) )
114 62 adantr 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> J e. NN0 )
115 40 adantr 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> I e. NN0 )
116 114 115 nn0mulcld 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( J x. I ) e. NN0 )
117 74 ablcmnd 
 |-  ( ph -> ( R |`s U ) e. CMnd )
118 eqid 
 |-  ( .g ` ( R |`s U ) ) = ( .g ` ( R |`s U ) )
119 117 42 118 isprimroot 
 |-  ( ph -> ( x e. ( ( R |`s U ) PrimRoots K ) <-> ( x e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) x ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) x ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
120 119 biimpd 
 |-  ( ph -> ( x e. ( ( R |`s U ) PrimRoots K ) -> ( x e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) x ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) x ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
121 120 imp 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( x e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) x ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) x ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
122 121 simp1d 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> x e. ( Base ` ( R |`s U ) ) )
123 eqid 
 |-  ( R |`s U ) = ( R |`s U )
124 123 48 ressbas2 
 |-  ( U C_ ( Base ` R ) -> U = ( Base ` ( R |`s U ) ) )
125 92 124 syl 
 |-  ( ph -> U = ( Base ` ( R |`s U ) ) )
126 125 adantr 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> U = ( Base ` ( R |`s U ) ) )
127 126 eleq2d 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( x e. U <-> x e. ( Base ` ( R |`s U ) ) ) )
128 122 127 mpbird 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> x e. U )
129 43 123 118 submmulg 
 |-  ( ( U e. ( SubMnd ` R ) /\ ( J x. I ) e. NN0 /\ x e. U ) -> ( ( J x. I ) ( .g ` R ) x ) = ( ( J x. I ) ( .g ` ( R |`s U ) ) x ) )
130 113 116 128 129 syl3anc 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( J x. I ) ( .g ` R ) x ) = ( ( J x. I ) ( .g ` ( R |`s U ) ) x ) )
131 26 adantr 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( J x. I ) = ( I x. J ) )
132 25 24 mulcld 
 |-  ( ph -> ( I x. J ) e. CC )
133 3 nncnd 
 |-  ( ph -> K e. CC )
134 6 zcnd 
 |-  ( ph -> Z e. CC )
135 133 134 mulcld 
 |-  ( ph -> ( K x. Z ) e. CC )
136 1cnd 
 |-  ( ph -> 1 e. CC )
137 132 135 136 addlsub 
 |-  ( ph -> ( ( ( I x. J ) + ( K x. Z ) ) = 1 <-> ( I x. J ) = ( 1 - ( K x. Z ) ) ) )
138 14 137 mpbid 
 |-  ( ph -> ( I x. J ) = ( 1 - ( K x. Z ) ) )
139 133 134 mulcomd 
 |-  ( ph -> ( K x. Z ) = ( Z x. K ) )
140 139 oveq2d 
 |-  ( ph -> ( 1 - ( K x. Z ) ) = ( 1 - ( Z x. K ) ) )
141 138 140 eqtrd 
 |-  ( ph -> ( I x. J ) = ( 1 - ( Z x. K ) ) )
142 139 135 eqeltrrd 
 |-  ( ph -> ( Z x. K ) e. CC )
143 136 142 negsubd 
 |-  ( ph -> ( 1 + -u ( Z x. K ) ) = ( 1 - ( Z x. K ) ) )
144 143 eqcomd 
 |-  ( ph -> ( 1 - ( Z x. K ) ) = ( 1 + -u ( Z x. K ) ) )
145 141 144 eqtrd 
 |-  ( ph -> ( I x. J ) = ( 1 + -u ( Z x. K ) ) )
146 145 adantr 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( I x. J ) = ( 1 + -u ( Z x. K ) ) )
147 131 146 eqtrd 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( J x. I ) = ( 1 + -u ( Z x. K ) ) )
148 147 oveq1d 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( J x. I ) ( .g ` ( R |`s U ) ) x ) = ( ( 1 + -u ( Z x. K ) ) ( .g ` ( R |`s U ) ) x ) )
149 76 adantr 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( R |`s U ) e. Grp )
150 1zzd 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> 1 e. ZZ )
151 6 adantr 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> Z e. ZZ )
152 10 adantr 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> K e. ZZ )
153 151 152 zmulcld 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( Z x. K ) e. ZZ )
154 153 znegcld 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> -u ( Z x. K ) e. ZZ )
155 150 154 122 3jca 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( 1 e. ZZ /\ -u ( Z x. K ) e. ZZ /\ x e. ( Base ` ( R |`s U ) ) ) )
156 eqid 
 |-  ( Base ` ( R |`s U ) ) = ( Base ` ( R |`s U ) )
157 eqid 
 |-  ( +g ` ( R |`s U ) ) = ( +g ` ( R |`s U ) )
158 156 118 157 mulgdir 
 |-  ( ( ( R |`s U ) e. Grp /\ ( 1 e. ZZ /\ -u ( Z x. K ) e. ZZ /\ x e. ( Base ` ( R |`s U ) ) ) ) -> ( ( 1 + -u ( Z x. K ) ) ( .g ` ( R |`s U ) ) x ) = ( ( 1 ( .g ` ( R |`s U ) ) x ) ( +g ` ( R |`s U ) ) ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) x ) ) )
159 149 155 158 syl2anc 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( 1 + -u ( Z x. K ) ) ( .g ` ( R |`s U ) ) x ) = ( ( 1 ( .g ` ( R |`s U ) ) x ) ( +g ` ( R |`s U ) ) ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) x ) ) )
160 156 118 mulg1 
 |-  ( x e. ( Base ` ( R |`s U ) ) -> ( 1 ( .g ` ( R |`s U ) ) x ) = x )
161 122 160 syl 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( 1 ( .g ` ( R |`s U ) ) x ) = x )
162 eqid 
 |-  ( invg ` ( R |`s U ) ) = ( invg ` ( R |`s U ) )
163 156 118 162 mulgneg 
 |-  ( ( ( R |`s U ) e. Grp /\ ( Z x. K ) e. ZZ /\ x e. ( Base ` ( R |`s U ) ) ) -> ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) x ) = ( ( invg ` ( R |`s U ) ) ` ( ( Z x. K ) ( .g ` ( R |`s U ) ) x ) ) )
164 149 153 122 163 syl3anc 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) x ) = ( ( invg ` ( R |`s U ) ) ` ( ( Z x. K ) ( .g ` ( R |`s U ) ) x ) ) )
165 161 164 oveq12d 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( 1 ( .g ` ( R |`s U ) ) x ) ( +g ` ( R |`s U ) ) ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) x ) ) = ( x ( +g ` ( R |`s U ) ) ( ( invg ` ( R |`s U ) ) ` ( ( Z x. K ) ( .g ` ( R |`s U ) ) x ) ) ) )
166 151 152 122 3jca 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( Z e. ZZ /\ K e. ZZ /\ x e. ( Base ` ( R |`s U ) ) ) )
167 156 118 mulgass 
 |-  ( ( ( R |`s U ) e. Grp /\ ( Z e. ZZ /\ K e. ZZ /\ x e. ( Base ` ( R |`s U ) ) ) ) -> ( ( Z x. K ) ( .g ` ( R |`s U ) ) x ) = ( Z ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) x ) ) )
168 149 166 167 syl2anc 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( Z x. K ) ( .g ` ( R |`s U ) ) x ) = ( Z ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) x ) ) )
169 121 simp2d 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( K ( .g ` ( R |`s U ) ) x ) = ( 0g ` ( R |`s U ) ) )
170 169 oveq2d 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( Z ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) x ) ) = ( Z ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) )
171 eqid 
 |-  ( 0g ` ( R |`s U ) ) = ( 0g ` ( R |`s U ) )
172 156 118 171 mulgz 
 |-  ( ( ( R |`s U ) e. Grp /\ Z e. ZZ ) -> ( Z ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
173 149 151 172 syl2anc 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( Z ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
174 170 173 eqtrd 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( Z ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) x ) ) = ( 0g ` ( R |`s U ) ) )
175 168 174 eqtrd 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( Z x. K ) ( .g ` ( R |`s U ) ) x ) = ( 0g ` ( R |`s U ) ) )
176 175 fveq2d 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( invg ` ( R |`s U ) ) ` ( ( Z x. K ) ( .g ` ( R |`s U ) ) x ) ) = ( ( invg ` ( R |`s U ) ) ` ( 0g ` ( R |`s U ) ) ) )
177 171 162 grpinvid 
 |-  ( ( R |`s U ) e. Grp -> ( ( invg ` ( R |`s U ) ) ` ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
178 76 177 syl 
 |-  ( ph -> ( ( invg ` ( R |`s U ) ) ` ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
179 178 adantr 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( invg ` ( R |`s U ) ) ` ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
180 176 179 eqtrd 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( invg ` ( R |`s U ) ) ` ( ( Z x. K ) ( .g ` ( R |`s U ) ) x ) ) = ( 0g ` ( R |`s U ) ) )
181 180 oveq2d 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( x ( +g ` ( R |`s U ) ) ( ( invg ` ( R |`s U ) ) ` ( ( Z x. K ) ( .g ` ( R |`s U ) ) x ) ) ) = ( x ( +g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) )
182 149 77 syl 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( R |`s U ) e. Mnd )
183 156 157 171 mndrid 
 |-  ( ( ( R |`s U ) e. Mnd /\ x e. ( Base ` ( R |`s U ) ) ) -> ( x ( +g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = x )
184 182 122 183 syl2anc 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( x ( +g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = x )
185 181 184 eqtrd 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( x ( +g ` ( R |`s U ) ) ( ( invg ` ( R |`s U ) ) ` ( ( Z x. K ) ( .g ` ( R |`s U ) ) x ) ) ) = x )
186 165 185 eqtrd 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( 1 ( .g ` ( R |`s U ) ) x ) ( +g ` ( R |`s U ) ) ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) x ) ) = x )
187 159 186 eqtrd 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( 1 + -u ( Z x. K ) ) ( .g ` ( R |`s U ) ) x ) = x )
188 148 187 eqtrd 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( J x. I ) ( .g ` ( R |`s U ) ) x ) = x )
189 130 188 eqtrd 
 |-  ( ( ph /\ x e. ( ( R |`s U ) PrimRoots K ) ) -> ( ( J x. I ) ( .g ` R ) x ) = x )
190 189 ex 
 |-  ( ph -> ( x e. ( ( R |`s U ) PrimRoots K ) -> ( ( J x. I ) ( .g ` R ) x ) = x ) )
191 190 imim2d 
 |-  ( ph -> ( ( x e. ( R PrimRoots K ) -> x e. ( ( R |`s U ) PrimRoots K ) ) -> ( x e. ( R PrimRoots K ) -> ( ( J x. I ) ( .g ` R ) x ) = x ) ) )
192 73 191 mpd 
 |-  ( ph -> ( x e. ( R PrimRoots K ) -> ( ( J x. I ) ( .g ` R ) x ) = x ) )
193 192 imp 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( ( J x. I ) ( .g ` R ) x ) = x )
194 69 193 eqtr3d 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( J ( .g ` R ) ( I ( .g ` R ) x ) ) = x )
195 66 194 eqtrd 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) ` ( I ( .g ` R ) x ) ) = x )
196 52 195 eqtrd 
 |-  ( ( ph /\ x e. ( R PrimRoots K ) ) -> ( ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) ` ( F ` x ) ) = x )
197 196 ralrimiva 
 |-  ( ph -> A. x e. ( R PrimRoots K ) ( ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) ` ( F ` x ) ) = x )
198 eqidd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) = ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) )
199 simpr 
 |-  ( ( ( ph /\ y e. ( R PrimRoots K ) ) /\ n = y ) -> n = y )
200 199 oveq2d 
 |-  ( ( ( ph /\ y e. ( R PrimRoots K ) ) /\ n = y ) -> ( J ( .g ` R ) n ) = ( J ( .g ` R ) y ) )
201 simpr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> y e. ( R PrimRoots K ) )
202 38 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> R e. Mnd )
203 62 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> J e. NN0 )
204 2 42 43 isprimroot 
 |-  ( ph -> ( y e. ( R PrimRoots K ) <-> ( y e. ( Base ` R ) /\ ( K ( .g ` R ) y ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) y ) = ( 0g ` R ) -> K || l ) ) ) )
205 204 biimpd 
 |-  ( ph -> ( y e. ( R PrimRoots K ) -> ( y e. ( Base ` R ) /\ ( K ( .g ` R ) y ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) y ) = ( 0g ` R ) -> K || l ) ) ) )
206 205 imp 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( y e. ( Base ` R ) /\ ( K ( .g ` R ) y ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) y ) = ( 0g ` R ) -> K || l ) ) )
207 206 simp1d 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> y e. ( Base ` R ) )
208 48 43 mulgnn0cl 
 |-  ( ( R e. Mnd /\ J e. NN0 /\ y e. ( Base ` R ) ) -> ( J ( .g ` R ) y ) e. ( Base ` R ) )
209 202 203 207 208 syl3anc 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( J ( .g ` R ) y ) e. ( Base ` R ) )
210 198 200 201 209 fvmptd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) ` y ) = ( J ( .g ` R ) y ) )
211 210 fveq2d 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( F ` ( ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) ` y ) ) = ( F ` ( J ( .g ` R ) y ) ) )
212 1 a1i 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> F = ( m e. ( R PrimRoots K ) |-> ( I ( .g ` R ) m ) ) )
213 simpr 
 |-  ( ( ( ph /\ y e. ( R PrimRoots K ) ) /\ m = ( J ( .g ` R ) y ) ) -> m = ( J ( .g ` R ) y ) )
214 213 oveq2d 
 |-  ( ( ( ph /\ y e. ( R PrimRoots K ) ) /\ m = ( J ( .g ` R ) y ) ) -> ( I ( .g ` R ) m ) = ( I ( .g ` R ) ( J ( .g ` R ) y ) ) )
215 2 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> R e. CMnd )
216 3 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> K e. NN )
217 5 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> J e. NN )
218 32 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( J gcd K ) = 1 )
219 215 216 217 218 201 60 primrootscoprmpow 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( J ( .g ` R ) y ) e. ( R PrimRoots K ) )
220 40 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> I e. NN0 )
221 48 43 mulgnn0cl 
 |-  ( ( R e. Mnd /\ I e. NN0 /\ ( J ( .g ` R ) y ) e. ( Base ` R ) ) -> ( I ( .g ` R ) ( J ( .g ` R ) y ) ) e. ( Base ` R ) )
222 202 220 209 221 syl3anc 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( I ( .g ` R ) ( J ( .g ` R ) y ) ) e. ( Base ` R ) )
223 212 214 219 222 fvmptd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( F ` ( J ( .g ` R ) y ) ) = ( I ( .g ` R ) ( J ( .g ` R ) y ) ) )
224 220 203 207 3jca 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( I e. NN0 /\ J e. NN0 /\ y e. ( Base ` R ) ) )
225 48 43 mulgnn0ass 
 |-  ( ( R e. Mnd /\ ( I e. NN0 /\ J e. NN0 /\ y e. ( Base ` R ) ) ) -> ( ( I x. J ) ( .g ` R ) y ) = ( I ( .g ` R ) ( J ( .g ` R ) y ) ) )
226 202 224 225 syl2anc 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( I x. J ) ( .g ` R ) y ) = ( I ( .g ` R ) ( J ( .g ` R ) y ) ) )
227 112 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> U e. ( SubMnd ` R ) )
228 220 203 nn0mulcld 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( I x. J ) e. NN0 )
229 128 ex 
 |-  ( ph -> ( x e. ( ( R |`s U ) PrimRoots K ) -> x e. U ) )
230 229 ssrdv 
 |-  ( ph -> ( ( R |`s U ) PrimRoots K ) C_ U )
231 71 sseq1d 
 |-  ( ph -> ( ( R PrimRoots K ) C_ U <-> ( ( R |`s U ) PrimRoots K ) C_ U ) )
232 230 231 mpbird 
 |-  ( ph -> ( R PrimRoots K ) C_ U )
233 232 sseld 
 |-  ( ph -> ( y e. ( R PrimRoots K ) -> y e. U ) )
234 233 imp 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> y e. U )
235 43 123 118 submmulg 
 |-  ( ( U e. ( SubMnd ` R ) /\ ( I x. J ) e. NN0 /\ y e. U ) -> ( ( I x. J ) ( .g ` R ) y ) = ( ( I x. J ) ( .g ` ( R |`s U ) ) y ) )
236 227 228 234 235 syl3anc 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( I x. J ) ( .g ` R ) y ) = ( ( I x. J ) ( .g ` ( R |`s U ) ) y ) )
237 145 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( I x. J ) = ( 1 + -u ( Z x. K ) ) )
238 237 oveq1d 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( I x. J ) ( .g ` ( R |`s U ) ) y ) = ( ( 1 + -u ( Z x. K ) ) ( .g ` ( R |`s U ) ) y ) )
239 76 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( R |`s U ) e. Grp )
240 1zzd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> 1 e. ZZ )
241 6 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> Z e. ZZ )
242 10 adantr 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> K e. ZZ )
243 241 242 zmulcld 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( Z x. K ) e. ZZ )
244 243 znegcld 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> -u ( Z x. K ) e. ZZ )
245 232 125 sseqtrd 
 |-  ( ph -> ( R PrimRoots K ) C_ ( Base ` ( R |`s U ) ) )
246 245 sseld 
 |-  ( ph -> ( y e. ( R PrimRoots K ) -> y e. ( Base ` ( R |`s U ) ) ) )
247 246 imp 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> y e. ( Base ` ( R |`s U ) ) )
248 240 244 247 3jca 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( 1 e. ZZ /\ -u ( Z x. K ) e. ZZ /\ y e. ( Base ` ( R |`s U ) ) ) )
249 156 118 157 mulgdir 
 |-  ( ( ( R |`s U ) e. Grp /\ ( 1 e. ZZ /\ -u ( Z x. K ) e. ZZ /\ y e. ( Base ` ( R |`s U ) ) ) ) -> ( ( 1 + -u ( Z x. K ) ) ( .g ` ( R |`s U ) ) y ) = ( ( 1 ( .g ` ( R |`s U ) ) y ) ( +g ` ( R |`s U ) ) ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) y ) ) )
250 239 248 249 syl2anc 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( 1 + -u ( Z x. K ) ) ( .g ` ( R |`s U ) ) y ) = ( ( 1 ( .g ` ( R |`s U ) ) y ) ( +g ` ( R |`s U ) ) ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) y ) ) )
251 156 118 mulg1 
 |-  ( y e. ( Base ` ( R |`s U ) ) -> ( 1 ( .g ` ( R |`s U ) ) y ) = y )
252 247 251 syl 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( 1 ( .g ` ( R |`s U ) ) y ) = y )
253 156 118 162 mulgneg 
 |-  ( ( ( R |`s U ) e. Grp /\ ( Z x. K ) e. ZZ /\ y e. ( Base ` ( R |`s U ) ) ) -> ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) y ) = ( ( invg ` ( R |`s U ) ) ` ( ( Z x. K ) ( .g ` ( R |`s U ) ) y ) ) )
254 239 243 247 253 syl3anc 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) y ) = ( ( invg ` ( R |`s U ) ) ` ( ( Z x. K ) ( .g ` ( R |`s U ) ) y ) ) )
255 241 242 247 3jca 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( Z e. ZZ /\ K e. ZZ /\ y e. ( Base ` ( R |`s U ) ) ) )
256 156 118 mulgass 
 |-  ( ( ( R |`s U ) e. Grp /\ ( Z e. ZZ /\ K e. ZZ /\ y e. ( Base ` ( R |`s U ) ) ) ) -> ( ( Z x. K ) ( .g ` ( R |`s U ) ) y ) = ( Z ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) y ) ) )
257 239 255 256 syl2anc 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( Z x. K ) ( .g ` ( R |`s U ) ) y ) = ( Z ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) y ) ) )
258 117 42 118 isprimroot 
 |-  ( ph -> ( y e. ( ( R |`s U ) PrimRoots K ) <-> ( y e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
259 258 biimpd 
 |-  ( ph -> ( y e. ( ( R |`s U ) PrimRoots K ) -> ( y e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
260 259 imp 
 |-  ( ( ph /\ y e. ( ( R |`s U ) PrimRoots K ) ) -> ( y e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
261 260 simp2d 
 |-  ( ( ph /\ y e. ( ( R |`s U ) PrimRoots K ) ) -> ( K ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) )
262 261 ex 
 |-  ( ph -> ( y e. ( ( R |`s U ) PrimRoots K ) -> ( K ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) ) )
263 71 eleq2d 
 |-  ( ph -> ( y e. ( R PrimRoots K ) <-> y e. ( ( R |`s U ) PrimRoots K ) ) )
264 263 imbi1d 
 |-  ( ph -> ( ( y e. ( R PrimRoots K ) -> ( K ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) ) <-> ( y e. ( ( R |`s U ) PrimRoots K ) -> ( K ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) ) ) )
265 262 264 mpbird 
 |-  ( ph -> ( y e. ( R PrimRoots K ) -> ( K ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) ) )
266 265 imp 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( K ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) )
267 266 oveq2d 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( Z ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) y ) ) = ( Z ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) )
268 239 241 172 syl2anc 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( Z ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
269 267 268 eqtrd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( Z ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) y ) ) = ( 0g ` ( R |`s U ) ) )
270 257 269 eqtrd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( Z x. K ) ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) )
271 270 fveq2d 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( invg ` ( R |`s U ) ) ` ( ( Z x. K ) ( .g ` ( R |`s U ) ) y ) ) = ( ( invg ` ( R |`s U ) ) ` ( 0g ` ( R |`s U ) ) ) )
272 239 177 syl 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( invg ` ( R |`s U ) ) ` ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
273 271 272 eqtrd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( invg ` ( R |`s U ) ) ` ( ( Z x. K ) ( .g ` ( R |`s U ) ) y ) ) = ( 0g ` ( R |`s U ) ) )
274 254 273 eqtrd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) y ) = ( 0g ` ( R |`s U ) ) )
275 252 274 oveq12d 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( 1 ( .g ` ( R |`s U ) ) y ) ( +g ` ( R |`s U ) ) ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) y ) ) = ( y ( +g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) )
276 156 157 171 239 247 grpridd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( y ( +g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = y )
277 275 276 eqtrd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( 1 ( .g ` ( R |`s U ) ) y ) ( +g ` ( R |`s U ) ) ( -u ( Z x. K ) ( .g ` ( R |`s U ) ) y ) ) = y )
278 250 277 eqtrd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( 1 + -u ( Z x. K ) ) ( .g ` ( R |`s U ) ) y ) = y )
279 238 278 eqtrd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( I x. J ) ( .g ` ( R |`s U ) ) y ) = y )
280 236 279 eqtrd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( ( I x. J ) ( .g ` R ) y ) = y )
281 226 280 eqtr3d 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( I ( .g ` R ) ( J ( .g ` R ) y ) ) = y )
282 223 281 eqtrd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( F ` ( J ( .g ` R ) y ) ) = y )
283 211 282 eqtrd 
 |-  ( ( ph /\ y e. ( R PrimRoots K ) ) -> ( F ` ( ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) ` y ) ) = y )
284 283 ralrimiva 
 |-  ( ph -> A. y e. ( R PrimRoots K ) ( F ` ( ( n e. ( R PrimRoots K ) |-> ( J ( .g ` R ) n ) ) ` y ) ) = y )
285 19 33 197 284 2fvidf1od 
 |-  ( ph -> F : ( R PrimRoots K ) -1-1-onto-> ( R PrimRoots K ) )