Metamath Proof Explorer

Theorem unitscyglem5

Description: Lemma for unitscyg (Contributed by metakunt, 9-Aug-2025)

Ref Expression
Hypotheses unitscyglem5.1 
|- G = ( ( mulGrp ` R ) |`s ( Unit ` R ) )
unitscyglem5.2 
|- ( ph -> R e. IDomn )
unitscyglem5.3 
|- ( ph -> ( Base ` R ) e. Fin )
unitscyglem5.4 
|- ( ph -> D e. NN )
unitscyglem5.5 
|- ( ph -> D || ( # ` ( Base ` G ) ) )
Assertion unitscyglem5 
|- ( ph -> ( ( mulGrp ` R ) PrimRoots D ) =/= (/) )

Proof

Step Hyp Ref Expression
1 unitscyglem5.1 
 |-  G = ( ( mulGrp ` R ) |`s ( Unit ` R ) )
2 unitscyglem5.2 
 |-  ( ph -> R e. IDomn )
3 unitscyglem5.3 
 |-  ( ph -> ( Base ` R ) e. Fin )
4 unitscyglem5.4 
 |-  ( ph -> D e. NN )
5 unitscyglem5.5 
 |-  ( ph -> D || ( # ` ( Base ` G ) ) )
6 4 phicld 
 |-  ( ph -> ( phi ` D ) e. NN )
7 eqid 
 |-  ( Base ` G ) = ( Base ` G )
8 eqid 
 |-  ( .g ` G ) = ( .g ` G )
9 2 idomringd 
 |-  ( ph -> R e. Ring )
10 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
11 10 1 unitgrp 
 |-  ( R e. Ring -> G e. Grp )
12 9 11 syl 
 |-  ( ph -> G e. Grp )
13 eqid 
 |-  ( Base ` ( mulGrp ` R ) ) = ( Base ` ( mulGrp ` R ) )
14 1 13 ressbasss 
 |-  ( Base ` G ) C_ ( Base ` ( mulGrp ` R ) )
15 14 a1i 
 |-  ( ph -> ( Base ` G ) C_ ( Base ` ( mulGrp ` R ) ) )
16 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
17 eqid 
 |-  ( Base ` R ) = ( Base ` R )
18 16 17 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
19 18 a1i 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( mulGrp ` R ) ) )
20 19 eqimsscd 
 |-  ( ph -> ( Base ` ( mulGrp ` R ) ) C_ ( Base ` R ) )
21 15 20 sstrd 
 |-  ( ph -> ( Base ` G ) C_ ( Base ` R ) )
22 3 21 ssfid 
 |-  ( ph -> ( Base ` G ) e. Fin )
23 18 eqcomi 
 |-  ( Base ` ( mulGrp ` R ) ) = ( Base ` R )
24 23 10 unitss 
 |-  ( Unit ` R ) C_ ( Base ` ( mulGrp ` R ) )
25 24 a1i 
 |-  ( ph -> ( Unit ` R ) C_ ( Base ` ( mulGrp ` R ) ) )
26 25 adantr 
 |-  ( ( ph /\ y e. NN ) -> ( Unit ` R ) C_ ( Base ` ( mulGrp ` R ) ) )
27 26 adantr 
 |-  ( ( ( ph /\ y e. NN ) /\ z e. ( Base ` G ) ) -> ( Unit ` R ) C_ ( Base ` ( mulGrp ` R ) ) )
28 1 13 ressbasssg 
 |-  ( Base ` G ) C_ ( ( Unit ` R ) i^i ( Base ` ( mulGrp ` R ) ) )
29 28 a1i 
 |-  ( ph -> ( Base ` G ) C_ ( ( Unit ` R ) i^i ( Base ` ( mulGrp ` R ) ) ) )
30 inss1 
 |-  ( ( Unit ` R ) i^i ( Base ` ( mulGrp ` R ) ) ) C_ ( Unit ` R )
31 30 a1i 
 |-  ( ph -> ( ( Unit ` R ) i^i ( Base ` ( mulGrp ` R ) ) ) C_ ( Unit ` R ) )
32 29 31 sstrd 
 |-  ( ph -> ( Base ` G ) C_ ( Unit ` R ) )
33 32 adantr 
 |-  ( ( ph /\ y e. NN ) -> ( Base ` G ) C_ ( Unit ` R ) )
34 33 sseld 
 |-  ( ( ph /\ y e. NN ) -> ( z e. ( Base ` G ) -> z e. ( Unit ` R ) ) )
35 34 imp 
 |-  ( ( ( ph /\ y e. NN ) /\ z e. ( Base ` G ) ) -> z e. ( Unit ` R ) )
36 simpr 
 |-  ( ( ph /\ y e. NN ) -> y e. NN )
37 36 adantr 
 |-  ( ( ( ph /\ y e. NN ) /\ z e. ( Base ` G ) ) -> y e. NN )
38 1 27 35 37 ressmulgnnd 
 |-  ( ( ( ph /\ y e. NN ) /\ z e. ( Base ` G ) ) -> ( y ( .g ` G ) z ) = ( y ( .g ` ( mulGrp ` R ) ) z ) )
39 38 eqeq1d 
 |-  ( ( ( ph /\ y e. NN ) /\ z e. ( Base ` G ) ) -> ( ( y ( .g ` G ) z ) = ( 0g ` G ) <-> ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) ) )
40 39 rabbidva 
 |-  ( ( ph /\ y e. NN ) -> { z e. ( Base ` G ) | ( y ( .g ` G ) z ) = ( 0g ` G ) } = { z e. ( Base ` G ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } )
41 40 fveq2d 
 |-  ( ( ph /\ y e. NN ) -> ( # ` { z e. ( Base ` G ) | ( y ( .g ` G ) z ) = ( 0g ` G ) } ) = ( # ` { z e. ( Base ` G ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) )
42 fvex 
 |-  ( Base ` G ) e. _V
43 42 rabex 
 |-  { z e. ( Base ` G ) | ( y ( .g ` G ) z ) = ( 0g ` G ) } e. _V
44 43 a1i 
 |-  ( ( ph /\ y e. NN ) -> { z e. ( Base ` G ) | ( y ( .g ` G ) z ) = ( 0g ` G ) } e. _V )
45 hashxrcl 
 |-  ( { z e. ( Base ` G ) | ( y ( .g ` G ) z ) = ( 0g ` G ) } e. _V -> ( # ` { z e. ( Base ` G ) | ( y ( .g ` G ) z ) = ( 0g ` G ) } ) e. RR* )
46 44 45 syl 
 |-  ( ( ph /\ y e. NN ) -> ( # ` { z e. ( Base ` G ) | ( y ( .g ` G ) z ) = ( 0g ` G ) } ) e. RR* )
47 41 46 eqeltrrd 
 |-  ( ( ph /\ y e. NN ) -> ( # ` { z e. ( Base ` G ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) e. RR* )
48 fvex 
 |-  ( Base ` R ) e. _V
49 48 rabex 
 |-  { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } e. _V
50 49 a1i 
 |-  ( ( ph /\ y e. NN ) -> { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } e. _V )
51 hashxrcl 
 |-  ( { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } e. _V -> ( # ` { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) e. RR* )
52 50 51 syl 
 |-  ( ( ph /\ y e. NN ) -> ( # ` { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) e. RR* )
53 nnre 
 |-  ( y e. NN -> y e. RR )
54 53 adantl 
 |-  ( ( ph /\ y e. NN ) -> y e. RR )
55 54 rexrd 
 |-  ( ( ph /\ y e. NN ) -> y e. RR* )
56 simprl 
 |-  ( ( ( ph /\ y e. NN ) /\ ( z e. ( Base ` G ) /\ ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) ) ) -> z e. ( Base ` G ) )
57 21 ad2antrr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( z e. ( Base ` G ) /\ ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) ) ) -> ( Base ` G ) C_ ( Base ` R ) )
58 57 sseld 
 |-  ( ( ( ph /\ y e. NN ) /\ ( z e. ( Base ` G ) /\ ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) ) ) -> ( z e. ( Base ` G ) -> z e. ( Base ` R ) ) )
59 56 58 mpd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( z e. ( Base ` G ) /\ ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) ) ) -> z e. ( Base ` R ) )
60 59 rabss3d 
 |-  ( ( ph /\ y e. NN ) -> { z e. ( Base ` G ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } C_ { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } )
61 50 60 jca 
 |-  ( ( ph /\ y e. NN ) -> ( { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } e. _V /\ { z e. ( Base ` G ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } C_ { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) )
62 hashss 
 |-  ( ( { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } e. _V /\ { z e. ( Base ` G ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } C_ { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) -> ( # ` { z e. ( Base ` G ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) <_ ( # ` { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) )
63 61 62 syl 
 |-  ( ( ph /\ y e. NN ) -> ( # ` { z e. ( Base ` G ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) <_ ( # ` { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) )
64 2 adantr 
 |-  ( ( ph /\ y e. NN ) -> R e. IDomn )
65 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
66 10 1 65 unitgrpid 
 |-  ( R e. Ring -> ( 1r ` R ) = ( 0g ` G ) )
67 9 66 syl 
 |-  ( ph -> ( 1r ` R ) = ( 0g ` G ) )
68 67 eqcomd 
 |-  ( ph -> ( 0g ` G ) = ( 1r ` R ) )
69 17 65 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
70 9 69 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
71 68 70 eqeltrd 
 |-  ( ph -> ( 0g ` G ) e. ( Base ` R ) )
72 71 adantr 
 |-  ( ( ph /\ y e. NN ) -> ( 0g ` G ) e. ( Base ` R ) )
73 eqid 
 |-  ( .g ` ( mulGrp ` R ) ) = ( .g ` ( mulGrp ` R ) )
74 17 73 idomrootle 
 |-  ( ( R e. IDomn /\ ( 0g ` G ) e. ( Base ` R ) /\ y e. NN ) -> ( # ` { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) <_ y )
75 64 72 36 74 syl3anc 
 |-  ( ( ph /\ y e. NN ) -> ( # ` { z e. ( Base ` R ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) <_ y )
76 47 52 55 63 75 xrletrd 
 |-  ( ( ph /\ y e. NN ) -> ( # ` { z e. ( Base ` G ) | ( y ( .g ` ( mulGrp ` R ) ) z ) = ( 0g ` G ) } ) <_ y )
77 41 76 eqbrtrd 
 |-  ( ( ph /\ y e. NN ) -> ( # ` { z e. ( Base ` G ) | ( y ( .g ` G ) z ) = ( 0g ` G ) } ) <_ y )
78 77 ralrimiva 
 |-  ( ph -> A. y e. NN ( # ` { z e. ( Base ` G ) | ( y ( .g ` G ) z ) = ( 0g ` G ) } ) <_ y )
79 7 8 12 22 78 4 5 unitscyglem4 
 |-  ( ph -> ( # ` { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) = ( phi ` D ) )
80 79 eleq1d 
 |-  ( ph -> ( ( # ` { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) e. NN <-> ( phi ` D ) e. NN ) )
81 6 80 mpbird 
 |-  ( ph -> ( # ` { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) e. NN )
82 81 nngt0d 
 |-  ( ph -> 0 < ( # ` { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) )
83 42 rabex 
 |-  { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } e. _V
84 83 a1i 
 |-  ( ph -> { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } e. _V )
85 hashneq0 
 |-  ( { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } e. _V -> ( 0 < ( # ` { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) <-> { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } =/= (/) ) )
86 84 85 syl 
 |-  ( ph -> ( 0 < ( # ` { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) <-> { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } =/= (/) ) )
87 82 86 mpbid 
 |-  ( ph -> { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } =/= (/) )
88 n0 
 |-  ( { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } =/= (/) <-> E. m m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } )
89 87 88 sylib 
 |-  ( ph -> E. m m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } )
90 nfv 
 |-  F/ m ph
91 fveqeq2 
 |-  ( w = m -> ( ( ( od ` G ) ` w ) = D <-> ( ( od ` G ) ` m ) = D ) )
92 91 elrab 
 |-  ( m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } <-> ( m e. ( Base ` G ) /\ ( ( od ` G ) ` m ) = D ) )
93 92 biimpi 
 |-  ( m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } -> ( m e. ( Base ` G ) /\ ( ( od ` G ) ` m ) = D ) )
94 93 adantl 
 |-  ( ( ph /\ m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) -> ( m e. ( Base ` G ) /\ ( ( od ` G ) ` m ) = D ) )
95 simpll 
 |-  ( ( ( ph /\ m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) /\ ( m e. ( Base ` G ) /\ ( ( od ` G ) ` m ) = D ) ) -> ph )
96 simprl 
 |-  ( ( ( ph /\ m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) /\ ( m e. ( Base ` G ) /\ ( ( od ` G ) ` m ) = D ) ) -> m e. ( Base ` G ) )
97 simprr 
 |-  ( ( ( ph /\ m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) /\ ( m e. ( Base ` G ) /\ ( ( od ` G ) ` m ) = D ) ) -> ( ( od ` G ) ` m ) = D )
98 95 96 97 jca31 
 |-  ( ( ( ph /\ m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) /\ ( m e. ( Base ` G ) /\ ( ( od ` G ) ` m ) = D ) ) -> ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) )
99 2 idomcringd 
 |-  ( ph -> R e. CRing )
100 16 crngmgp 
 |-  ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
101 99 100 syl 
 |-  ( ph -> ( mulGrp ` R ) e. CMnd )
102 101 ad2antrr 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( mulGrp ` R ) e. CMnd )
103 4 ad2antrr 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> D e. NN )
104 15 sselda 
 |-  ( ( ph /\ m e. ( Base ` G ) ) -> m e. ( Base ` ( mulGrp ` R ) ) )
105 104 adantr 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> m e. ( Base ` ( mulGrp ` R ) ) )
106 9 ad2antrr 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> R e. Ring )
107 10 16 unitsubm 
 |-  ( R e. Ring -> ( Unit ` R ) e. ( SubMnd ` ( mulGrp ` R ) ) )
108 106 107 syl 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( Unit ` R ) e. ( SubMnd ` ( mulGrp ` R ) ) )
109 105 23 eleqtrdi 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> m e. ( Base ` R ) )
110 102 cmnmndd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( mulGrp ` R ) e. Mnd )
111 4 nnzd 
 |-  ( ph -> D e. ZZ )
112 1zzd 
 |-  ( ph -> 1 e. ZZ )
113 111 112 zsubcld 
 |-  ( ph -> ( D - 1 ) e. ZZ )
114 1cnd 
 |-  ( ph -> 1 e. CC )
115 114 addridd 
 |-  ( ph -> ( 1 + 0 ) = 1 )
116 4 nnge1d 
 |-  ( ph -> 1 <_ D )
117 115 116 eqbrtrd 
 |-  ( ph -> ( 1 + 0 ) <_ D )
118 1red 
 |-  ( ph -> 1 e. RR )
119 0red 
 |-  ( ph -> 0 e. RR )
120 4 nnred 
 |-  ( ph -> D e. RR )
121 118 119 120 leaddsub2d 
 |-  ( ph -> ( ( 1 + 0 ) <_ D <-> 0 <_ ( D - 1 ) ) )
122 117 121 mpbid 
 |-  ( ph -> 0 <_ ( D - 1 ) )
123 113 122 jca 
 |-  ( ph -> ( ( D - 1 ) e. ZZ /\ 0 <_ ( D - 1 ) ) )
124 elnn0z 
 |-  ( ( D - 1 ) e. NN0 <-> ( ( D - 1 ) e. ZZ /\ 0 <_ ( D - 1 ) ) )
125 123 124 sylibr 
 |-  ( ph -> ( D - 1 ) e. NN0 )
126 125 adantr 
 |-  ( ( ph /\ m e. ( Base ` G ) ) -> ( D - 1 ) e. NN0 )
127 126 adantr 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( D - 1 ) e. NN0 )
128 18 73 110 127 109 mulgnn0cld 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) e. ( Base ` R ) )
129 simpr 
 |-  ( ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) /\ o = ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ) -> o = ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) )
130 129 oveq1d 
 |-  ( ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) /\ o = ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ) -> ( o ( .r ` R ) m ) = ( ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ( .r ` R ) m ) )
131 130 eqeq1d 
 |-  ( ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) /\ o = ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ) -> ( ( o ( .r ` R ) m ) = ( 1r ` R ) <-> ( ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ( .r ` R ) m ) = ( 1r ` R ) ) )
132 eqid 
 |-  ( .r ` R ) = ( .r ` R )
133 16 132 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
134 133 a1i 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( .r ` R ) = ( +g ` ( mulGrp ` R ) ) )
135 134 oveqd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ( .r ` R ) m ) = ( ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ( +g ` ( mulGrp ` R ) ) m ) )
136 103 nncnd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> D e. CC )
137 1cnd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> 1 e. CC )
138 136 137 npcand 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( D - 1 ) + 1 ) = D )
139 138 eqcomd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> D = ( ( D - 1 ) + 1 ) )
140 139 oveq1d 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( D ( .g ` ( mulGrp ` R ) ) m ) = ( ( ( D - 1 ) + 1 ) ( .g ` ( mulGrp ` R ) ) m ) )
141 eqid 
 |-  ( +g ` ( mulGrp ` R ) ) = ( +g ` ( mulGrp ` R ) )
142 13 73 141 mulgnn0p1 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ ( D - 1 ) e. NN0 /\ m e. ( Base ` ( mulGrp ` R ) ) ) -> ( ( ( D - 1 ) + 1 ) ( .g ` ( mulGrp ` R ) ) m ) = ( ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ( +g ` ( mulGrp ` R ) ) m ) )
143 110 127 105 142 syl3anc 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( ( D - 1 ) + 1 ) ( .g ` ( mulGrp ` R ) ) m ) = ( ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ( +g ` ( mulGrp ` R ) ) m ) )
144 140 143 eqtr2d 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ( +g ` ( mulGrp ` R ) ) m ) = ( D ( .g ` ( mulGrp ` R ) ) m ) )
145 16 65 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
146 145 a1i 
 |-  ( ph -> ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) ) )
147 146 eqcomd 
 |-  ( ph -> ( 0g ` ( mulGrp ` R ) ) = ( 1r ` R ) )
148 10 65 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Unit ` R ) )
149 9 148 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Unit ` R ) )
150 147 149 eqeltrd 
 |-  ( ph -> ( 0g ` ( mulGrp ` R ) ) e. ( Unit ` R ) )
151 150 adantr 
 |-  ( ( ph /\ m e. ( Base ` G ) ) -> ( 0g ` ( mulGrp ` R ) ) e. ( Unit ` R ) )
152 151 adantr 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( 0g ` ( mulGrp ` R ) ) e. ( Unit ` R ) )
153 24 a1i 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( Unit ` R ) C_ ( Base ` ( mulGrp ` R ) ) )
154 eqid 
 |-  ( 0g ` ( mulGrp ` R ) ) = ( 0g ` ( mulGrp ` R ) )
155 1 13 154 ress0g 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ ( 0g ` ( mulGrp ` R ) ) e. ( Unit ` R ) /\ ( Unit ` R ) C_ ( Base ` ( mulGrp ` R ) ) ) -> ( 0g ` ( mulGrp ` R ) ) = ( 0g ` G ) )
156 110 152 153 155 syl3anc 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( 0g ` ( mulGrp ` R ) ) = ( 0g ` G ) )
157 simpr 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( od ` G ) ` m ) = D )
158 157 eqcomd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> D = ( ( od ` G ) ` m ) )
159 158 oveq1d 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( D ( .g ` G ) m ) = ( ( ( od ` G ) ` m ) ( .g ` G ) m ) )
160 eqid 
 |-  ( od ` G ) = ( od ` G )
161 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
162 7 160 8 161 odid 
 |-  ( m e. ( Base ` G ) -> ( ( ( od ` G ) ` m ) ( .g ` G ) m ) = ( 0g ` G ) )
163 162 ad2antlr 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( ( od ` G ) ` m ) ( .g ` G ) m ) = ( 0g ` G ) )
164 159 163 eqtrd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( D ( .g ` G ) m ) = ( 0g ` G ) )
165 164 eqcomd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( 0g ` G ) = ( D ( .g ` G ) m ) )
166 156 165 eqtrd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( 0g ` ( mulGrp ` R ) ) = ( D ( .g ` G ) m ) )
167 32 sselda 
 |-  ( ( ph /\ m e. ( Base ` G ) ) -> m e. ( Unit ` R ) )
168 167 adantr 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> m e. ( Unit ` R ) )
169 1 153 168 103 ressmulgnnd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( D ( .g ` G ) m ) = ( D ( .g ` ( mulGrp ` R ) ) m ) )
170 166 169 eqtr2d 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( D ( .g ` ( mulGrp ` R ) ) m ) = ( 0g ` ( mulGrp ` R ) ) )
171 144 170 eqtrd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ( +g ` ( mulGrp ` R ) ) m ) = ( 0g ` ( mulGrp ` R ) ) )
172 145 a1i 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) ) )
173 172 eqcomd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( 0g ` ( mulGrp ` R ) ) = ( 1r ` R ) )
174 171 173 eqtrd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ( +g ` ( mulGrp ` R ) ) m ) = ( 1r ` R ) )
175 135 174 eqtrd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( ( D - 1 ) ( .g ` ( mulGrp ` R ) ) m ) ( .r ` R ) m ) = ( 1r ` R ) )
176 128 131 175 rspcedvd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> E. o e. ( Base ` R ) ( o ( .r ` R ) m ) = ( 1r ` R ) )
177 109 176 jca 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( m e. ( Base ` R ) /\ E. o e. ( Base ` R ) ( o ( .r ` R ) m ) = ( 1r ` R ) ) )
178 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
179 17 178 132 dvdsr 
 |-  ( m ( ||r ` R ) ( 1r ` R ) <-> ( m e. ( Base ` R ) /\ E. o e. ( Base ` R ) ( o ( .r ` R ) m ) = ( 1r ` R ) ) )
180 177 179 sylibr 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> m ( ||r ` R ) ( 1r ` R ) )
181 99 adantr 
 |-  ( ( ph /\ m e. ( Base ` G ) ) -> R e. CRing )
182 181 adantr 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> R e. CRing )
183 10 65 178 crngunit 
 |-  ( R e. CRing -> ( m e. ( Unit ` R ) <-> m ( ||r ` R ) ( 1r ` R ) ) )
184 182 183 syl 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( m e. ( Unit ` R ) <-> m ( ||r ` R ) ( 1r ` R ) ) )
185 180 184 mpbird 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> m e. ( Unit ` R ) )
186 eqid 
 |-  ( od ` ( mulGrp ` R ) ) = ( od ` ( mulGrp ` R ) )
187 1 186 160 submod 
 |-  ( ( ( Unit ` R ) e. ( SubMnd ` ( mulGrp ` R ) ) /\ m e. ( Unit ` R ) ) -> ( ( od ` ( mulGrp ` R ) ) ` m ) = ( ( od ` G ) ` m ) )
188 108 185 187 syl2anc 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( od ` ( mulGrp ` R ) ) ` m ) = ( ( od ` G ) ` m ) )
189 188 157 eqtrd 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> ( ( od ` ( mulGrp ` R ) ) ` m ) = D )
190 102 103 105 189 isprimroot2 
 |-  ( ( ( ph /\ m e. ( Base ` G ) ) /\ ( ( od ` G ) ` m ) = D ) -> m e. ( ( mulGrp ` R ) PrimRoots D ) )
191 98 190 syl 
 |-  ( ( ( ph /\ m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) /\ ( m e. ( Base ` G ) /\ ( ( od ` G ) ` m ) = D ) ) -> m e. ( ( mulGrp ` R ) PrimRoots D ) )
192 94 191 mpdan 
 |-  ( ( ph /\ m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } ) -> m e. ( ( mulGrp ` R ) PrimRoots D ) )
193 192 ex 
 |-  ( ph -> ( m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } -> m e. ( ( mulGrp ` R ) PrimRoots D ) ) )
194 90 193 eximd 
 |-  ( ph -> ( E. m m e. { w e. ( Base ` G ) | ( ( od ` G ) ` w ) = D } -> E. m m e. ( ( mulGrp ` R ) PrimRoots D ) ) )
195 89 194 mpd 
 |-  ( ph -> E. m m e. ( ( mulGrp ` R ) PrimRoots D ) )
196 n0 
 |-  ( ( ( mulGrp ` R ) PrimRoots D ) =/= (/) <-> E. m m e. ( ( mulGrp ` R ) PrimRoots D ) )
197 195 196 sylibr 
 |-  ( ph -> ( ( mulGrp ` R ) PrimRoots D ) =/= (/) )