Metamath Proof Explorer

Theorem primrootsunit1

Description: Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025)

Ref Expression
Hypotheses primrootsunit1.1 
|- ( ph -> R e. CMnd )
primrootsunit1.2 
|- ( ph -> K e. NN )
primrootsunit1.3 
|- U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
Assertion primrootsunit1 
|- ( ph -> ( ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) /\ ( R |`s U ) e. Abel ) )

Proof

Step Hyp Ref Expression
1 primrootsunit1.1 
 |-  ( ph -> R e. CMnd )
2 primrootsunit1.2 
 |-  ( ph -> K e. NN )
3 primrootsunit1.3 
 |-  U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
4 1 adantr 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> R e. CMnd )
5 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
6 5 adantr 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> K e. NN0 )
7 eqid 
 |-  ( .g ` R ) = ( .g ` R )
8 4 6 7 isprimroot 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( c e. ( R PrimRoots K ) <-> ( c e. ( Base ` R ) /\ ( K ( .g ` R ) c ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) c ) = ( 0g ` R ) -> K || l ) ) ) )
9 8 biimpd 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( c e. ( R PrimRoots K ) -> ( c e. ( Base ` R ) /\ ( K ( .g ` R ) c ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) c ) = ( 0g ` R ) -> K || l ) ) ) )
10 9 syldbl2 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( c e. ( Base ` R ) /\ ( K ( .g ` R ) c ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) c ) = ( 0g ` R ) -> K || l ) ) )
11 10 simp1d 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> c e. ( Base ` R ) )
12 1 cmnmndd 
 |-  ( ph -> R e. Mnd )
13 12 adantr 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> R e. Mnd )
14 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
15 2 14 syl 
 |-  ( ph -> ( K - 1 ) e. NN0 )
16 15 adantr 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( K - 1 ) e. NN0 )
17 eqid 
 |-  ( Base ` R ) = ( Base ` R )
18 17 7 mulgnn0cl 
 |-  ( ( R e. Mnd /\ ( K - 1 ) e. NN0 /\ c e. ( Base ` R ) ) -> ( ( K - 1 ) ( .g ` R ) c ) e. ( Base ` R ) )
19 13 16 11 18 syl3anc 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( ( K - 1 ) ( .g ` R ) c ) e. ( Base ` R ) )
20 simpr 
 |-  ( ( ( ph /\ c e. ( R PrimRoots K ) ) /\ i = ( ( K - 1 ) ( .g ` R ) c ) ) -> i = ( ( K - 1 ) ( .g ` R ) c ) )
21 20 oveq1d 
 |-  ( ( ( ph /\ c e. ( R PrimRoots K ) ) /\ i = ( ( K - 1 ) ( .g ` R ) c ) ) -> ( i ( +g ` R ) c ) = ( ( ( K - 1 ) ( .g ` R ) c ) ( +g ` R ) c ) )
22 21 eqeq1d 
 |-  ( ( ( ph /\ c e. ( R PrimRoots K ) ) /\ i = ( ( K - 1 ) ( .g ` R ) c ) ) -> ( ( i ( +g ` R ) c ) = ( 0g ` R ) <-> ( ( ( K - 1 ) ( .g ` R ) c ) ( +g ` R ) c ) = ( 0g ` R ) ) )
23 2 nncnd 
 |-  ( ph -> K e. CC )
24 1cnd 
 |-  ( ph -> 1 e. CC )
25 23 24 npcand 
 |-  ( ph -> ( ( K - 1 ) + 1 ) = K )
26 25 eqcomd 
 |-  ( ph -> K = ( ( K - 1 ) + 1 ) )
27 26 adantr 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> K = ( ( K - 1 ) + 1 ) )
28 27 oveq1d 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( K ( .g ` R ) c ) = ( ( ( K - 1 ) + 1 ) ( .g ` R ) c ) )
29 eqid 
 |-  ( +g ` R ) = ( +g ` R )
30 17 7 29 mulgnn0p1 
 |-  ( ( R e. Mnd /\ ( K - 1 ) e. NN0 /\ c e. ( Base ` R ) ) -> ( ( ( K - 1 ) + 1 ) ( .g ` R ) c ) = ( ( ( K - 1 ) ( .g ` R ) c ) ( +g ` R ) c ) )
31 13 16 11 30 syl3anc 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( ( ( K - 1 ) + 1 ) ( .g ` R ) c ) = ( ( ( K - 1 ) ( .g ` R ) c ) ( +g ` R ) c ) )
32 28 31 eqtr2d 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( ( ( K - 1 ) ( .g ` R ) c ) ( +g ` R ) c ) = ( K ( .g ` R ) c ) )
33 10 simp2d 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( K ( .g ` R ) c ) = ( 0g ` R ) )
34 32 33 eqtrd 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( ( ( K - 1 ) ( .g ` R ) c ) ( +g ` R ) c ) = ( 0g ` R ) )
35 19 22 34 rspcedvd 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> E. i e. ( Base ` R ) ( i ( +g ` R ) c ) = ( 0g ` R ) )
36 11 35 jca 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( c e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) c ) = ( 0g ` R ) ) )
37 oveq2 
 |-  ( a = c -> ( i ( +g ` R ) a ) = ( i ( +g ` R ) c ) )
38 37 eqeq1d 
 |-  ( a = c -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( i ( +g ` R ) c ) = ( 0g ` R ) ) )
39 38 rexbidv 
 |-  ( a = c -> ( E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) <-> E. i e. ( Base ` R ) ( i ( +g ` R ) c ) = ( 0g ` R ) ) )
40 39 elrab 
 |-  ( c e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } <-> ( c e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) c ) = ( 0g ` R ) ) )
41 36 40 sylibr 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> c e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
42 3 eleq2i 
 |-  ( c e. U <-> c e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
43 41 42 sylibr 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> c e. U )
44 simpl 
 |-  ( ( ph /\ b e. U ) -> ph )
45 3 a1i 
 |-  ( ph -> U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
46 45 eleq2d 
 |-  ( ph -> ( b e. U <-> b e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
47 46 biimpd 
 |-  ( ph -> ( b e. U -> b e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
48 47 imp 
 |-  ( ( ph /\ b e. U ) -> b e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
49 44 48 jca 
 |-  ( ( ph /\ b e. U ) -> ( ph /\ b e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
50 elrabi 
 |-  ( b e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } -> b e. ( Base ` R ) )
51 50 adantl 
 |-  ( ( ph /\ b e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) -> b e. ( Base ` R ) )
52 49 51 syl 
 |-  ( ( ph /\ b e. U ) -> b e. ( Base ` R ) )
53 52 ex 
 |-  ( ph -> ( b e. U -> b e. ( Base ` R ) ) )
54 53 ssrdv 
 |-  ( ph -> U C_ ( Base ` R ) )
55 eqid 
 |-  ( R |`s U ) = ( R |`s U )
56 55 17 ressbas2 
 |-  ( U C_ ( Base ` R ) -> U = ( Base ` ( R |`s U ) ) )
57 54 56 syl 
 |-  ( ph -> U = ( Base ` ( R |`s U ) ) )
58 57 adantr 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> U = ( Base ` ( R |`s U ) ) )
59 58 eleq2d 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( c e. U <-> c e. ( Base ` ( R |`s U ) ) ) )
60 43 59 mpbid 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> c e. ( Base ` ( R |`s U ) ) )
61 12 ad2antrr 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> R e. Mnd )
62 52 adantr 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> b e. ( Base ` R ) )
63 simpl 
 |-  ( ( ph /\ d e. U ) -> ph )
64 45 eleq2d 
 |-  ( ph -> ( d e. U <-> d e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
65 64 biimpd 
 |-  ( ph -> ( d e. U -> d e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
66 65 imp 
 |-  ( ( ph /\ d e. U ) -> d e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
67 63 66 jca 
 |-  ( ( ph /\ d e. U ) -> ( ph /\ d e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
68 elrabi 
 |-  ( d e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } -> d e. ( Base ` R ) )
69 68 adantl 
 |-  ( ( ph /\ d e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) -> d e. ( Base ` R ) )
70 67 69 syl 
 |-  ( ( ph /\ d e. U ) -> d e. ( Base ` R ) )
71 44 70 sylan 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> d e. ( Base ` R ) )
72 17 29 mndcl 
 |-  ( ( R e. Mnd /\ b e. ( Base ` R ) /\ d e. ( Base ` R ) ) -> ( b ( +g ` R ) d ) e. ( Base ` R ) )
73 61 62 71 72 syl3anc 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( b ( +g ` R ) d ) e. ( Base ` R ) )
74 3 eleq2i 
 |-  ( d e. U <-> d e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
75 oveq2 
 |-  ( a = d -> ( i ( +g ` R ) a ) = ( i ( +g ` R ) d ) )
76 75 eqeq1d 
 |-  ( a = d -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( i ( +g ` R ) d ) = ( 0g ` R ) ) )
77 76 rexbidv 
 |-  ( a = d -> ( E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) <-> E. i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) ) )
78 77 elrab 
 |-  ( d e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } <-> ( d e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) ) )
79 74 78 bitri 
 |-  ( d e. U <-> ( d e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) ) )
80 79 biimpi 
 |-  ( d e. U -> ( d e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) ) )
81 80 simprd 
 |-  ( d e. U -> E. i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) )
82 81 adantl 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> E. i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) )
83 1 ad4antr 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) d ) = ( 0g ` R ) ) -> R e. CMnd )
84 71 ad2antrr 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) d ) = ( 0g ` R ) ) -> d e. ( Base ` R ) )
85 simplr 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) d ) = ( 0g ` R ) ) -> i e. ( Base ` R ) )
86 17 29 cmncom 
 |-  ( ( R e. CMnd /\ d e. ( Base ` R ) /\ i e. ( Base ` R ) ) -> ( d ( +g ` R ) i ) = ( i ( +g ` R ) d ) )
87 83 84 85 86 syl3anc 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) d ) = ( 0g ` R ) ) -> ( d ( +g ` R ) i ) = ( i ( +g ` R ) d ) )
88 simpr 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) d ) = ( 0g ` R ) ) -> ( i ( +g ` R ) d ) = ( 0g ` R ) )
89 87 88 eqtrd 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) d ) = ( 0g ` R ) ) -> ( d ( +g ` R ) i ) = ( 0g ` R ) )
90 89 ex 
 |-  ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) -> ( ( i ( +g ` R ) d ) = ( 0g ` R ) -> ( d ( +g ` R ) i ) = ( 0g ` R ) ) )
91 90 reximdva 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( E. i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) -> E. i e. ( Base ` R ) ( d ( +g ` R ) i ) = ( 0g ` R ) ) )
92 82 91 mpd 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> E. i e. ( Base ` R ) ( d ( +g ` R ) i ) = ( 0g ` R ) )
93 17 61 71 92 mndmolinv 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> E* i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) )
94 82 93 jca 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( E. i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) /\ E* i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) ) )
95 reu5 
 |-  ( E! i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) <-> ( E. i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) /\ E* i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) ) )
96 94 95 sylibr 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> E! i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) )
97 riotacl 
 |-  ( E! i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) -> ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) ) e. ( Base ` R ) )
98 96 97 syl 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) ) e. ( Base ` R ) )
99 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
100 eqid 
 |-  ( invg ` R ) = ( invg ` R )
101 17 29 99 100 grpinvval 
 |-  ( d e. ( Base ` R ) -> ( ( invg ` R ) ` d ) = ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) ) )
102 71 101 syl 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( invg ` R ) ` d ) = ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) ) )
103 102 eleq1d 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` d ) e. ( Base ` R ) <-> ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) d ) = ( 0g ` R ) ) e. ( Base ` R ) ) )
104 98 103 mpbird 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( invg ` R ) ` d ) e. ( Base ` R ) )
105 3 eleq2i 
 |-  ( b e. U <-> b e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
106 oveq2 
 |-  ( a = b -> ( i ( +g ` R ) a ) = ( i ( +g ` R ) b ) )
107 106 eqeq1d 
 |-  ( a = b -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( i ( +g ` R ) b ) = ( 0g ` R ) ) )
108 107 rexbidv 
 |-  ( a = b -> ( E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) <-> E. i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) ) )
109 108 elrab 
 |-  ( b e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } <-> ( b e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) ) )
110 105 109 bitri 
 |-  ( b e. U <-> ( b e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) ) )
111 110 biimpi 
 |-  ( b e. U -> ( b e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) ) )
112 111 simprd 
 |-  ( b e. U -> E. i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) )
113 112 ad2antlr 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> E. i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) )
114 1 ad4antr 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) b ) = ( 0g ` R ) ) -> R e. CMnd )
115 62 ad2antrr 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) b ) = ( 0g ` R ) ) -> b e. ( Base ` R ) )
116 simplr 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) b ) = ( 0g ` R ) ) -> i e. ( Base ` R ) )
117 17 29 cmncom 
 |-  ( ( R e. CMnd /\ b e. ( Base ` R ) /\ i e. ( Base ` R ) ) -> ( b ( +g ` R ) i ) = ( i ( +g ` R ) b ) )
118 114 115 116 117 syl3anc 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) b ) = ( 0g ` R ) ) -> ( b ( +g ` R ) i ) = ( i ( +g ` R ) b ) )
119 simpr 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) b ) = ( 0g ` R ) ) -> ( i ( +g ` R ) b ) = ( 0g ` R ) )
120 118 119 eqtrd 
 |-  ( ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) /\ ( i ( +g ` R ) b ) = ( 0g ` R ) ) -> ( b ( +g ` R ) i ) = ( 0g ` R ) )
121 120 ex 
 |-  ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i e. ( Base ` R ) ) -> ( ( i ( +g ` R ) b ) = ( 0g ` R ) -> ( b ( +g ` R ) i ) = ( 0g ` R ) ) )
122 121 reximdva 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( E. i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) -> E. i e. ( Base ` R ) ( b ( +g ` R ) i ) = ( 0g ` R ) ) )
123 113 122 mpd 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> E. i e. ( Base ` R ) ( b ( +g ` R ) i ) = ( 0g ` R ) )
124 17 61 62 123 mndmolinv 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> E* i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) )
125 113 124 jca 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( E. i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) /\ E* i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) ) )
126 reu5 
 |-  ( E! i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) <-> ( E. i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) /\ E* i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) ) )
127 125 126 sylibr 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> E! i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) )
128 riotacl 
 |-  ( E! i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) -> ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) ) e. ( Base ` R ) )
129 127 128 syl 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) ) e. ( Base ` R ) )
130 17 29 99 100 grpinvval 
 |-  ( b e. ( Base ` R ) -> ( ( invg ` R ) ` b ) = ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) ) )
131 62 130 syl 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( invg ` R ) ` b ) = ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) ) )
132 131 eleq1d 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` b ) e. ( Base ` R ) <-> ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) b ) = ( 0g ` R ) ) e. ( Base ` R ) ) )
133 129 132 mpbird 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( invg ` R ) ` b ) e. ( Base ` R ) )
134 17 29 mndcl 
 |-  ( ( R e. Mnd /\ ( ( invg ` R ) ` d ) e. ( Base ` R ) /\ ( ( invg ` R ) ` b ) e. ( Base ` R ) ) -> ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( invg ` R ) ` b ) ) e. ( Base ` R ) )
135 61 104 133 134 syl3anc 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( invg ` R ) ` b ) ) e. ( Base ` R ) )
136 oveq1 
 |-  ( i = ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( invg ` R ) ` b ) ) -> ( i ( +g ` R ) ( b ( +g ` R ) d ) ) = ( ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( invg ` R ) ` b ) ) ( +g ` R ) ( b ( +g ` R ) d ) ) )
137 136 eqeq1d 
 |-  ( i = ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( invg ` R ) ` b ) ) -> ( ( i ( +g ` R ) ( b ( +g ` R ) d ) ) = ( 0g ` R ) <-> ( ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( invg ` R ) ` b ) ) ( +g ` R ) ( b ( +g ` R ) d ) ) = ( 0g ` R ) ) )
138 137 adantl 
 |-  ( ( ( ( ph /\ b e. U ) /\ d e. U ) /\ i = ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( invg ` R ) ` b ) ) ) -> ( ( i ( +g ` R ) ( b ( +g ` R ) d ) ) = ( 0g ` R ) <-> ( ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( invg ` R ) ` b ) ) ( +g ` R ) ( b ( +g ` R ) d ) ) = ( 0g ` R ) ) )
139 104 133 73 3jca 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` d ) e. ( Base ` R ) /\ ( ( invg ` R ) ` b ) e. ( Base ` R ) /\ ( b ( +g ` R ) d ) e. ( Base ` R ) ) )
140 17 29 mndass 
 |-  ( ( R e. Mnd /\ ( ( ( invg ` R ) ` d ) e. ( Base ` R ) /\ ( ( invg ` R ) ` b ) e. ( Base ` R ) /\ ( b ( +g ` R ) d ) e. ( Base ` R ) ) ) -> ( ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( invg ` R ) ` b ) ) ( +g ` R ) ( b ( +g ` R ) d ) ) = ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( ( invg ` R ) ` b ) ( +g ` R ) ( b ( +g ` R ) d ) ) ) )
141 61 139 140 syl2anc 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( invg ` R ) ` b ) ) ( +g ` R ) ( b ( +g ` R ) d ) ) = ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( ( invg ` R ) ` b ) ( +g ` R ) ( b ( +g ` R ) d ) ) ) )
142 133 62 71 3jca 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` b ) e. ( Base ` R ) /\ b e. ( Base ` R ) /\ d e. ( Base ` R ) ) )
143 17 29 mndass 
 |-  ( ( R e. Mnd /\ ( ( ( invg ` R ) ` b ) e. ( Base ` R ) /\ b e. ( Base ` R ) /\ d e. ( Base ` R ) ) ) -> ( ( ( ( invg ` R ) ` b ) ( +g ` R ) b ) ( +g ` R ) d ) = ( ( ( invg ` R ) ` b ) ( +g ` R ) ( b ( +g ` R ) d ) ) )
144 143 eqcomd 
 |-  ( ( R e. Mnd /\ ( ( ( invg ` R ) ` b ) e. ( Base ` R ) /\ b e. ( Base ` R ) /\ d e. ( Base ` R ) ) ) -> ( ( ( invg ` R ) ` b ) ( +g ` R ) ( b ( +g ` R ) d ) ) = ( ( ( ( invg ` R ) ` b ) ( +g ` R ) b ) ( +g ` R ) d ) )
145 61 142 144 syl2anc 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` b ) ( +g ` R ) ( b ( +g ` R ) d ) ) = ( ( ( ( invg ` R ) ` b ) ( +g ` R ) b ) ( +g ` R ) d ) )
146 145 oveq2d 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( ( invg ` R ) ` b ) ( +g ` R ) ( b ( +g ` R ) d ) ) ) = ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( ( ( invg ` R ) ` b ) ( +g ` R ) b ) ( +g ` R ) d ) ) )
147 62 127 linvh 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` b ) ( +g ` R ) b ) = ( 0g ` R ) )
148 147 oveq1d 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( ( invg ` R ) ` b ) ( +g ` R ) b ) ( +g ` R ) d ) = ( ( 0g ` R ) ( +g ` R ) d ) )
149 148 oveq2d 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( ( ( invg ` R ) ` b ) ( +g ` R ) b ) ( +g ` R ) d ) ) = ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( 0g ` R ) ( +g ` R ) d ) ) )
150 17 29 99 mndlid 
 |-  ( ( R e. Mnd /\ d e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) d ) = d )
151 61 71 150 syl2anc 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( 0g ` R ) ( +g ` R ) d ) = d )
152 151 oveq2d 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( 0g ` R ) ( +g ` R ) d ) ) = ( ( ( invg ` R ) ` d ) ( +g ` R ) d ) )
153 71 96 linvh 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` d ) ( +g ` R ) d ) = ( 0g ` R ) )
154 152 153 eqtrd 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( 0g ` R ) ( +g ` R ) d ) ) = ( 0g ` R ) )
155 149 154 eqtrd 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( ( ( invg ` R ) ` b ) ( +g ` R ) b ) ( +g ` R ) d ) ) = ( 0g ` R ) )
156 146 155 eqtrd 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( ( invg ` R ) ` b ) ( +g ` R ) ( b ( +g ` R ) d ) ) ) = ( 0g ` R ) )
157 141 156 eqtrd 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( ( ( invg ` R ) ` d ) ( +g ` R ) ( ( invg ` R ) ` b ) ) ( +g ` R ) ( b ( +g ` R ) d ) ) = ( 0g ` R ) )
158 135 138 157 rspcedvd 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> E. i e. ( Base ` R ) ( i ( +g ` R ) ( b ( +g ` R ) d ) ) = ( 0g ` R ) )
159 73 158 jca 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( b ( +g ` R ) d ) e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) ( b ( +g ` R ) d ) ) = ( 0g ` R ) ) )
160 oveq2 
 |-  ( a = ( b ( +g ` R ) d ) -> ( i ( +g ` R ) a ) = ( i ( +g ` R ) ( b ( +g ` R ) d ) ) )
161 160 eqeq1d 
 |-  ( a = ( b ( +g ` R ) d ) -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( i ( +g ` R ) ( b ( +g ` R ) d ) ) = ( 0g ` R ) ) )
162 161 rexbidv 
 |-  ( a = ( b ( +g ` R ) d ) -> ( E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) <-> E. i e. ( Base ` R ) ( i ( +g ` R ) ( b ( +g ` R ) d ) ) = ( 0g ` R ) ) )
163 162 elrab 
 |-  ( ( b ( +g ` R ) d ) e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } <-> ( ( b ( +g ` R ) d ) e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) ( b ( +g ` R ) d ) ) = ( 0g ` R ) ) )
164 159 163 sylibr 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( b ( +g ` R ) d ) e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
165 3 eleq2i 
 |-  ( ( b ( +g ` R ) d ) e. U <-> ( b ( +g ` R ) d ) e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
166 165 a1i 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( b ( +g ` R ) d ) e. U <-> ( b ( +g ` R ) d ) e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
167 164 166 mpbird 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( b ( +g ` R ) d ) e. U )
168 167 ralrimiva 
 |-  ( ( ph /\ b e. U ) -> A. d e. U ( b ( +g ` R ) d ) e. U )
169 168 ralrimiva 
 |-  ( ph -> A. b e. U A. d e. U ( b ( +g ` R ) d ) e. U )
170 oveq2 
 |-  ( a = ( 0g ` R ) -> ( i ( +g ` R ) a ) = ( i ( +g ` R ) ( 0g ` R ) ) )
171 170 eqeq1d 
 |-  ( a = ( 0g ` R ) -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( i ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
172 171 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 ) ) )
173 17 99 mndidcl 
 |-  ( R e. Mnd -> ( 0g ` R ) e. ( Base ` R ) )
174 12 173 syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
175 12 174 jca 
 |-  ( ph -> ( R e. Mnd /\ ( 0g ` R ) e. ( Base ` R ) ) )
176 17 29 99 mndlid 
 |-  ( ( R e. Mnd /\ ( 0g ` R ) e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
177 175 176 syl 
 |-  ( ph -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
178 174 177 jca 
 |-  ( ph -> ( ( 0g ` R ) e. ( Base ` R ) /\ ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
179 oveq1 
 |-  ( i = ( 0g ` R ) -> ( i ( +g ` R ) ( 0g ` R ) ) = ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) )
180 179 eqeq1d 
 |-  ( i = ( 0g ` R ) -> ( ( i ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) <-> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
181 180 rspcev 
 |-  ( ( ( 0g ` R ) e. ( Base ` R ) /\ ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) -> E. i e. ( Base ` R ) ( i ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
182 178 181 syl 
 |-  ( ph -> E. i e. ( Base ` R ) ( i ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
183 172 174 182 elrabd 
 |-  ( ph -> ( 0g ` R ) e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
184 45 eleq2d 
 |-  ( ph -> ( ( 0g ` R ) e. U <-> ( 0g ` R ) e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
185 183 184 mpbird 
 |-  ( ph -> ( 0g ` R ) e. U )
186 17 29 99 55 issubmnd 
 |-  ( ( R e. Mnd /\ U C_ ( Base ` R ) /\ ( 0g ` R ) e. U ) -> ( ( R |`s U ) e. Mnd <-> A. b e. U A. d e. U ( b ( +g ` R ) d ) e. U ) )
187 12 54 185 186 syl3anc 
 |-  ( ph -> ( ( R |`s U ) e. Mnd <-> A. b e. U A. d e. U ( b ( +g ` R ) d ) e. U ) )
188 169 187 mpbird 
 |-  ( ph -> ( R |`s U ) e. Mnd )
189 45 eleq2d 
 |-  ( ph -> ( q e. U <-> q e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
190 189 biimpd 
 |-  ( ph -> ( q e. U -> q e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
191 190 imp 
 |-  ( ( ph /\ q e. U ) -> q e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
192 oveq2 
 |-  ( a = q -> ( i ( +g ` R ) a ) = ( i ( +g ` R ) q ) )
193 192 eqeq1d 
 |-  ( a = q -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( i ( +g ` R ) q ) = ( 0g ` R ) ) )
194 193 rexbidv 
 |-  ( a = q -> ( E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) <-> E. i e. ( Base ` R ) ( i ( +g ` R ) q ) = ( 0g ` R ) ) )
195 194 elrab 
 |-  ( q e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } <-> ( q e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) q ) = ( 0g ` R ) ) )
196 191 195 sylib 
 |-  ( ( ph /\ q e. U ) -> ( q e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) q ) = ( 0g ` R ) ) )
197 196 simprd 
 |-  ( ( ph /\ q e. U ) -> E. i e. ( Base ` R ) ( i ( +g ` R ) q ) = ( 0g ` R ) )
198 simprl 
 |-  ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) -> i e. ( Base ` R ) )
199 196 simpld 
 |-  ( ( ph /\ q e. U ) -> q e. ( Base ` R ) )
200 199 adantr 
 |-  ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) -> q e. ( Base ` R ) )
201 simpr 
 |-  ( ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) /\ j = q ) -> j = q )
202 201 oveq1d 
 |-  ( ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) /\ j = q ) -> ( j ( +g ` R ) i ) = ( q ( +g ` R ) i ) )
203 202 eqeq1d 
 |-  ( ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) /\ j = q ) -> ( ( j ( +g ` R ) i ) = ( 0g ` R ) <-> ( q ( +g ` R ) i ) = ( 0g ` R ) ) )
204 1 ad2antrr 
 |-  ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) -> R e. CMnd )
205 17 29 cmncom 
 |-  ( ( R e. CMnd /\ i e. ( Base ` R ) /\ q e. ( Base ` R ) ) -> ( i ( +g ` R ) q ) = ( q ( +g ` R ) i ) )
206 204 198 200 205 syl3anc 
 |-  ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) -> ( i ( +g ` R ) q ) = ( q ( +g ` R ) i ) )
207 simprr 
 |-  ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) -> ( i ( +g ` R ) q ) = ( 0g ` R ) )
208 206 207 eqtr3d 
 |-  ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) -> ( q ( +g ` R ) i ) = ( 0g ` R ) )
209 200 203 208 rspcedvd 
 |-  ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) -> E. j e. ( Base ` R ) ( j ( +g ` R ) i ) = ( 0g ` R ) )
210 198 209 jca 
 |-  ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) -> ( i e. ( Base ` R ) /\ E. j e. ( Base ` R ) ( j ( +g ` R ) i ) = ( 0g ` R ) ) )
211 nfv 
 |-  F/ j ( i ( +g ` R ) a ) = ( 0g ` R )
212 nfv 
 |-  F/ i ( j ( +g ` R ) a ) = ( 0g ` R )
213 oveq1 
 |-  ( i = j -> ( i ( +g ` R ) a ) = ( j ( +g ` R ) a ) )
214 213 eqeq1d 
 |-  ( i = j -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( j ( +g ` R ) a ) = ( 0g ` R ) ) )
215 211 212 214 cbvrexw 
 |-  ( E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) <-> E. j e. ( Base ` R ) ( j ( +g ` R ) a ) = ( 0g ` R ) )
216 215 rabbii 
 |-  { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } = { a e. ( Base ` R ) | E. j e. ( Base ` R ) ( j ( +g ` R ) a ) = ( 0g ` R ) }
217 3 216 eqtri 
 |-  U = { a e. ( Base ` R ) | E. j e. ( Base ` R ) ( j ( +g ` R ) a ) = ( 0g ` R ) }
218 217 eleq2i 
 |-  ( i e. U <-> i e. { a e. ( Base ` R ) | E. j e. ( Base ` R ) ( j ( +g ` R ) a ) = ( 0g ` R ) } )
219 oveq2 
 |-  ( a = i -> ( j ( +g ` R ) a ) = ( j ( +g ` R ) i ) )
220 219 eqeq1d 
 |-  ( a = i -> ( ( j ( +g ` R ) a ) = ( 0g ` R ) <-> ( j ( +g ` R ) i ) = ( 0g ` R ) ) )
221 220 rexbidv 
 |-  ( a = i -> ( E. j e. ( Base ` R ) ( j ( +g ` R ) a ) = ( 0g ` R ) <-> E. j e. ( Base ` R ) ( j ( +g ` R ) i ) = ( 0g ` R ) ) )
222 221 elrab 
 |-  ( i e. { a e. ( Base ` R ) | E. j e. ( Base ` R ) ( j ( +g ` R ) a ) = ( 0g ` R ) } <-> ( i e. ( Base ` R ) /\ E. j e. ( Base ` R ) ( j ( +g ` R ) i ) = ( 0g ` R ) ) )
223 218 222 bitri 
 |-  ( i e. U <-> ( i e. ( Base ` R ) /\ E. j e. ( Base ` R ) ( j ( +g ` R ) i ) = ( 0g ` R ) ) )
224 210 223 sylibr 
 |-  ( ( ( ph /\ q e. U ) /\ ( i e. ( Base ` R ) /\ ( i ( +g ` R ) q ) = ( 0g ` R ) ) ) -> i e. U )
225 197 224 207 reximssdv 
 |-  ( ( ph /\ q e. U ) -> E. i e. U ( i ( +g ` R ) q ) = ( 0g ` R ) )
226 fvexd 
 |-  ( ph -> ( Base ` R ) e. _V )
227 3 226 rabexd 
 |-  ( ph -> U e. _V )
228 55 29 ressplusg 
 |-  ( U e. _V -> ( +g ` R ) = ( +g ` ( R |`s U ) ) )
229 227 228 syl 
 |-  ( ph -> ( +g ` R ) = ( +g ` ( R |`s U ) ) )
230 229 eqcomd 
 |-  ( ph -> ( +g ` ( R |`s U ) ) = ( +g ` R ) )
231 230 adantr 
 |-  ( ( ph /\ q e. U ) -> ( +g ` ( R |`s U ) ) = ( +g ` R ) )
232 231 adantr 
 |-  ( ( ( ph /\ q e. U ) /\ w = i ) -> ( +g ` ( R |`s U ) ) = ( +g ` R ) )
233 simpr 
 |-  ( ( ( ph /\ q e. U ) /\ w = i ) -> w = i )
234 eqidd 
 |-  ( ( ( ph /\ q e. U ) /\ w = i ) -> q = q )
235 232 233 234 oveq123d 
 |-  ( ( ( ph /\ q e. U ) /\ w = i ) -> ( w ( +g ` ( R |`s U ) ) q ) = ( i ( +g ` R ) q ) )
236 55 17 99 ress0g 
 |-  ( ( R e. Mnd /\ ( 0g ` R ) e. U /\ U C_ ( Base ` R ) ) -> ( 0g ` R ) = ( 0g ` ( R |`s U ) ) )
237 12 185 54 236 syl3anc 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` ( R |`s U ) ) )
238 237 eqcomd 
 |-  ( ph -> ( 0g ` ( R |`s U ) ) = ( 0g ` R ) )
239 238 adantr 
 |-  ( ( ph /\ q e. U ) -> ( 0g ` ( R |`s U ) ) = ( 0g ` R ) )
240 239 adantr 
 |-  ( ( ( ph /\ q e. U ) /\ w = i ) -> ( 0g ` ( R |`s U ) ) = ( 0g ` R ) )
241 235 240 eqeq12d 
 |-  ( ( ( ph /\ q e. U ) /\ w = i ) -> ( ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) <-> ( i ( +g ` R ) q ) = ( 0g ` R ) ) )
242 eqidd 
 |-  ( ( ( ph /\ q e. U ) /\ w = i ) -> U = U )
243 241 242 cbvrexdva2 
 |-  ( ( ph /\ q e. U ) -> ( E. w e. U ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) <-> E. i e. U ( i ( +g ` R ) q ) = ( 0g ` R ) ) )
244 225 243 mpbird 
 |-  ( ( ph /\ q e. U ) -> E. w e. U ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) )
245 57 eqcomd 
 |-  ( ph -> ( Base ` ( R |`s U ) ) = U )
246 245 adantr 
 |-  ( ( ph /\ q e. U ) -> ( Base ` ( R |`s U ) ) = U )
247 244 246 rexeqtrrdv 
 |-  ( ( ph /\ q e. U ) -> E. w e. ( Base ` ( R |`s U ) ) ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) )
248 247 ex 
 |-  ( ph -> ( q e. U -> E. w e. ( Base ` ( R |`s U ) ) ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) ) )
249 57 eleq2d 
 |-  ( ph -> ( q e. U <-> q e. ( Base ` ( R |`s U ) ) ) )
250 249 imbi1d 
 |-  ( ph -> ( ( q e. U -> E. w e. ( Base ` ( R |`s U ) ) ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) ) <-> ( q e. ( Base ` ( R |`s U ) ) -> E. w e. ( Base ` ( R |`s U ) ) ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) ) ) )
251 248 250 mpbid 
 |-  ( ph -> ( q e. ( Base ` ( R |`s U ) ) -> E. w e. ( Base ` ( R |`s U ) ) ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) ) )
252 251 imp 
 |-  ( ( ph /\ q e. ( Base ` ( R |`s U ) ) ) -> E. w e. ( Base ` ( R |`s U ) ) ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) )
253 252 ralrimiva 
 |-  ( ph -> A. q e. ( Base ` ( R |`s U ) ) E. w e. ( Base ` ( R |`s U ) ) ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) )
254 188 253 jca 
 |-  ( ph -> ( ( R |`s U ) e. Mnd /\ A. q e. ( Base ` ( R |`s U ) ) E. w e. ( Base ` ( R |`s U ) ) ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) ) )
255 eqid 
 |-  ( Base ` ( R |`s U ) ) = ( Base ` ( R |`s U ) )
256 eqid 
 |-  ( +g ` ( R |`s U ) ) = ( +g ` ( R |`s U ) )
257 eqid 
 |-  ( 0g ` ( R |`s U ) ) = ( 0g ` ( R |`s U ) )
258 255 256 257 isgrp 
 |-  ( ( R |`s U ) e. Grp <-> ( ( R |`s U ) e. Mnd /\ A. q e. ( Base ` ( R |`s U ) ) E. w e. ( Base ` ( R |`s U ) ) ( w ( +g ` ( R |`s U ) ) q ) = ( 0g ` ( R |`s U ) ) ) )
259 254 258 sylibr 
 |-  ( ph -> ( R |`s U ) e. Grp )
260 259 ad2antrr 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( R |`s U ) e. Grp )
261 simplr 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> b e. U )
262 57 adantr 
 |-  ( ( ph /\ b e. U ) -> U = ( Base ` ( R |`s U ) ) )
263 262 adantr 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> U = ( Base ` ( R |`s U ) ) )
264 263 eleq2d 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( b e. U <-> b e. ( Base ` ( R |`s U ) ) ) )
265 261 264 mpbid 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> b e. ( Base ` ( R |`s U ) ) )
266 simpr 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> d e. U )
267 263 eleq2d 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( d e. U <-> d e. ( Base ` ( R |`s U ) ) ) )
268 266 267 mpbid 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> d e. ( Base ` ( R |`s U ) ) )
269 255 256 grpcl 
 |-  ( ( ( R |`s U ) e. Grp /\ b e. ( Base ` ( R |`s U ) ) /\ d e. ( Base ` ( R |`s U ) ) ) -> ( b ( +g ` ( R |`s U ) ) d ) e. ( Base ` ( R |`s U ) ) )
270 260 265 268 269 syl3anc 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( b ( +g ` ( R |`s U ) ) d ) e. ( Base ` ( R |`s U ) ) )
271 263 eleq2d 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( b ( +g ` ( R |`s U ) ) d ) e. U <-> ( b ( +g ` ( R |`s U ) ) d ) e. ( Base ` ( R |`s U ) ) ) )
272 270 271 mpbird 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( b ( +g ` ( R |`s U ) ) d ) e. U )
273 229 adantr 
 |-  ( ( ph /\ b e. U ) -> ( +g ` R ) = ( +g ` ( R |`s U ) ) )
274 273 oveqdr 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( b ( +g ` R ) d ) = ( b ( +g ` ( R |`s U ) ) d ) )
275 274 eleq1d 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( ( b ( +g ` R ) d ) e. U <-> ( b ( +g ` ( R |`s U ) ) d ) e. U ) )
276 272 275 mpbird 
 |-  ( ( ( ph /\ b e. U ) /\ d e. U ) -> ( b ( +g ` R ) d ) e. U )
277 276 ralrimiva 
 |-  ( ( ph /\ b e. U ) -> A. d e. U ( b ( +g ` R ) d ) e. U )
278 277 ralrimiva 
 |-  ( ph -> A. b e. U A. d e. U ( b ( +g ` R ) d ) e. U )
279 278 187 mpbird 
 |-  ( ph -> ( R |`s U ) e. Mnd )
280 12 279 jca 
 |-  ( ph -> ( R e. Mnd /\ ( R |`s U ) e. Mnd ) )
281 54 185 jca 
 |-  ( ph -> ( U C_ ( Base ` R ) /\ ( 0g ` R ) e. U ) )
282 280 281 jca 
 |-  ( ph -> ( ( R e. Mnd /\ ( R |`s U ) e. Mnd ) /\ ( U C_ ( Base ` R ) /\ ( 0g ` R ) e. U ) ) )
283 17 99 issubmndb 
 |-  ( U e. ( SubMnd ` R ) <-> ( ( R e. Mnd /\ ( R |`s U ) e. Mnd ) /\ ( U C_ ( Base ` R ) /\ ( 0g ` R ) e. U ) ) )
284 282 283 sylibr 
 |-  ( ph -> U e. ( SubMnd ` R ) )
285 284 adantr 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> U e. ( SubMnd ` R ) )
286 285 6 43 3jca 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( U e. ( SubMnd ` R ) /\ K e. NN0 /\ c e. U ) )
287 eqid 
 |-  ( .g ` ( R |`s U ) ) = ( .g ` ( R |`s U ) )
288 7 55 287 submmulg 
 |-  ( ( U e. ( SubMnd ` R ) /\ K e. NN0 /\ c e. U ) -> ( K ( .g ` R ) c ) = ( K ( .g ` ( R |`s U ) ) c ) )
289 288 eqcomd 
 |-  ( ( U e. ( SubMnd ` R ) /\ K e. NN0 /\ c e. U ) -> ( K ( .g ` ( R |`s U ) ) c ) = ( K ( .g ` R ) c ) )
290 286 289 syl 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( K ( .g ` ( R |`s U ) ) c ) = ( K ( .g ` R ) c ) )
291 238 adantr 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( 0g ` ( R |`s U ) ) = ( 0g ` R ) )
292 290 291 eqeq12d 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( ( K ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) <-> ( K ( .g ` R ) c ) = ( 0g ` R ) ) )
293 33 292 mpbird 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( K ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) )
294 10 simp3d 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> A. l e. NN0 ( ( l ( .g ` R ) c ) = ( 0g ` R ) -> K || l ) )
295 eqidd 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> NN0 = NN0 )
296 285 adantr 
 |-  ( ( ( ph /\ c e. ( R PrimRoots K ) ) /\ l e. NN0 ) -> U e. ( SubMnd ` R ) )
297 simpr 
 |-  ( ( ( ph /\ c e. ( R PrimRoots K ) ) /\ l e. NN0 ) -> l e. NN0 )
298 43 adantr 
 |-  ( ( ( ph /\ c e. ( R PrimRoots K ) ) /\ l e. NN0 ) -> c e. U )
299 296 297 298 3jca 
 |-  ( ( ( ph /\ c e. ( R PrimRoots K ) ) /\ l e. NN0 ) -> ( U e. ( SubMnd ` R ) /\ l e. NN0 /\ c e. U ) )
300 7 55 287 submmulg 
 |-  ( ( U e. ( SubMnd ` R ) /\ l e. NN0 /\ c e. U ) -> ( l ( .g ` R ) c ) = ( l ( .g ` ( R |`s U ) ) c ) )
301 299 300 syl 
 |-  ( ( ( ph /\ c e. ( R PrimRoots K ) ) /\ l e. NN0 ) -> ( l ( .g ` R ) c ) = ( l ( .g ` ( R |`s U ) ) c ) )
302 237 ad2antrr 
 |-  ( ( ( ph /\ c e. ( R PrimRoots K ) ) /\ l e. NN0 ) -> ( 0g ` R ) = ( 0g ` ( R |`s U ) ) )
303 301 302 eqeq12d 
 |-  ( ( ( ph /\ c e. ( R PrimRoots K ) ) /\ l e. NN0 ) -> ( ( l ( .g ` R ) c ) = ( 0g ` R ) <-> ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) ) )
304 303 imbi1d 
 |-  ( ( ( ph /\ c e. ( R PrimRoots K ) ) /\ l e. NN0 ) -> ( ( ( l ( .g ` R ) c ) = ( 0g ` R ) -> K || l ) <-> ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
305 295 304 raleqbidva 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( A. l e. NN0 ( ( l ( .g ` R ) c ) = ( 0g ` R ) -> K || l ) <-> A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
306 294 305 mpbid 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) )
307 60 293 306 3jca 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( c e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
308 1 3ad2ant1 
 |-  ( ( ph /\ b e. U /\ d e. U ) -> R e. CMnd )
309 62 3impa 
 |-  ( ( ph /\ b e. U /\ d e. U ) -> b e. ( Base ` R ) )
310 71 3impa 
 |-  ( ( ph /\ b e. U /\ d e. U ) -> d e. ( Base ` R ) )
311 17 29 cmncom 
 |-  ( ( R e. CMnd /\ b e. ( Base ` R ) /\ d e. ( Base ` R ) ) -> ( b ( +g ` R ) d ) = ( d ( +g ` R ) b ) )
312 308 309 310 311 syl3anc 
 |-  ( ( ph /\ b e. U /\ d e. U ) -> ( b ( +g ` R ) d ) = ( d ( +g ` R ) b ) )
313 57 229 279 312 iscmnd 
 |-  ( ph -> ( R |`s U ) e. CMnd )
314 313 5 287 isprimroot 
 |-  ( ph -> ( c e. ( ( R |`s U ) PrimRoots K ) <-> ( c e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
315 314 adantr 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> ( c e. ( ( R |`s U ) PrimRoots K ) <-> ( c e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
316 307 315 mpbird 
 |-  ( ( ph /\ c e. ( R PrimRoots K ) ) -> c e. ( ( R |`s U ) PrimRoots K ) )
317 316 ex 
 |-  ( ph -> ( c e. ( R PrimRoots K ) -> c e. ( ( R |`s U ) PrimRoots K ) ) )
318 317 ssrdv 
 |-  ( ph -> ( R PrimRoots K ) C_ ( ( R |`s U ) PrimRoots K ) )
319 313 adantr 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( R |`s U ) e. CMnd )
320 5 adantr 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> K e. NN0 )
321 319 320 287 isprimroot 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( c e. ( ( R |`s U ) PrimRoots K ) <-> ( c e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
322 321 biimpd 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( c e. ( ( R |`s U ) PrimRoots K ) -> ( c e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
323 322 syldbl2 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( c e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
324 323 simp1d 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> c e. ( Base ` ( R |`s U ) ) )
325 54 sselda 
 |-  ( ( ph /\ c e. U ) -> c e. ( Base ` R ) )
326 325 ex 
 |-  ( ph -> ( c e. U -> c e. ( Base ` R ) ) )
327 57 eleq2d 
 |-  ( ph -> ( c e. U <-> c e. ( Base ` ( R |`s U ) ) ) )
328 327 imbi1d 
 |-  ( ph -> ( ( c e. U -> c e. ( Base ` R ) ) <-> ( c e. ( Base ` ( R |`s U ) ) -> c e. ( Base ` R ) ) ) )
329 326 328 mpbid 
 |-  ( ph -> ( c e. ( Base ` ( R |`s U ) ) -> c e. ( Base ` R ) ) )
330 329 adantr 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( c e. ( Base ` ( R |`s U ) ) -> c e. ( Base ` R ) ) )
331 330 imp 
 |-  ( ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) /\ c e. ( Base ` ( R |`s U ) ) ) -> c e. ( Base ` R ) )
332 324 331 mpdan 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> c e. ( Base ` R ) )
333 284 adantr 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> U e. ( SubMnd ` R ) )
334 327 adantr 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( c e. U <-> c e. ( Base ` ( R |`s U ) ) ) )
335 324 334 mpbird 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> c e. U )
336 333 320 335 288 syl3anc 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( K ( .g ` R ) c ) = ( K ( .g ` ( R |`s U ) ) c ) )
337 323 simp2d 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( K ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) )
338 238 adantr 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( 0g ` ( R |`s U ) ) = ( 0g ` R ) )
339 336 337 338 3eqtrd 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( K ( .g ` R ) c ) = ( 0g ` R ) )
340 323 simp3d 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) )
341 333 adantr 
 |-  ( ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) /\ l e. NN0 ) -> U e. ( SubMnd ` R ) )
342 simpr 
 |-  ( ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) /\ l e. NN0 ) -> l e. NN0 )
343 335 adantr 
 |-  ( ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) /\ l e. NN0 ) -> c e. U )
344 341 342 343 300 syl3anc 
 |-  ( ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) /\ l e. NN0 ) -> ( l ( .g ` R ) c ) = ( l ( .g ` ( R |`s U ) ) c ) )
345 344 eqcomd 
 |-  ( ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) /\ l e. NN0 ) -> ( l ( .g ` ( R |`s U ) ) c ) = ( l ( .g ` R ) c ) )
346 338 adantr 
 |-  ( ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) /\ l e. NN0 ) -> ( 0g ` ( R |`s U ) ) = ( 0g ` R ) )
347 345 346 eqeq12d 
 |-  ( ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) /\ l e. NN0 ) -> ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) <-> ( l ( .g ` R ) c ) = ( 0g ` R ) ) )
348 347 imbi1d 
 |-  ( ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) /\ l e. NN0 ) -> ( ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) <-> ( ( l ( .g ` R ) c ) = ( 0g ` R ) -> K || l ) ) )
349 348 ralbidva 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) c ) = ( 0g ` ( R |`s U ) ) -> K || l ) <-> A. l e. NN0 ( ( l ( .g ` R ) c ) = ( 0g ` R ) -> K || l ) ) )
350 340 349 mpbid 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> A. l e. NN0 ( ( l ( .g ` R ) c ) = ( 0g ` R ) -> K || l ) )
351 332 339 350 3jca 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( c e. ( Base ` R ) /\ ( K ( .g ` R ) c ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) c ) = ( 0g ` R ) -> K || l ) ) )
352 1 adantr 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> R e. CMnd )
353 352 320 7 isprimroot 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> ( c e. ( R PrimRoots K ) <-> ( c e. ( Base ` R ) /\ ( K ( .g ` R ) c ) = ( 0g ` R ) /\ A. l e. NN0 ( ( l ( .g ` R ) c ) = ( 0g ` R ) -> K || l ) ) ) )
354 351 353 mpbird 
 |-  ( ( ph /\ c e. ( ( R |`s U ) PrimRoots K ) ) -> c e. ( R PrimRoots K ) )
355 354 ex 
 |-  ( ph -> ( c e. ( ( R |`s U ) PrimRoots K ) -> c e. ( R PrimRoots K ) ) )
356 355 ssrdv 
 |-  ( ph -> ( ( R |`s U ) PrimRoots K ) C_ ( R PrimRoots K ) )
357 318 356 eqssd 
 |-  ( ph -> ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) )
358 259 313 jca 
 |-  ( ph -> ( ( R |`s U ) e. Grp /\ ( R |`s U ) e. CMnd ) )
359 isabl 
 |-  ( ( R |`s U ) e. Abel <-> ( ( R |`s U ) e. Grp /\ ( R |`s U ) e. CMnd ) )
360 358 359 sylibr 
 |-  ( ph -> ( R |`s U ) e. Abel )
361 357 360 jca 
 |-  ( ph -> ( ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) /\ ( R |`s U ) e. Abel ) )