Metamath Proof Explorer

Theorem primrootscoprmpow

Description: Coprime powers of primitive roots are primitive roots. (Contributed by metakunt, 25-Apr-2025)

Ref Expression
Hypotheses primrootscoprmpow.1 
|- ( ph -> R e. CMnd )
primrootscoprmpow.2 
|- ( ph -> K e. NN )
primrootscoprmpow.3 
|- ( ph -> E e. NN )
primrootscoprmpow.4 
|- ( ph -> ( E gcd K ) = 1 )
primrootscoprmpow.5 
|- ( ph -> M e. ( R PrimRoots K ) )
primrootscoprmpow.6 
|- U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
Assertion primrootscoprmpow 
|- ( ph -> ( E ( .g ` R ) M ) e. ( R PrimRoots K ) )

Proof

Step Hyp Ref Expression
1 primrootscoprmpow.1 
 |-  ( ph -> R e. CMnd )
2 primrootscoprmpow.2 
 |-  ( ph -> K e. NN )
3 primrootscoprmpow.3 
 |-  ( ph -> E e. NN )
4 primrootscoprmpow.4 
 |-  ( ph -> ( E gcd K ) = 1 )
5 primrootscoprmpow.5 
 |-  ( ph -> M e. ( R PrimRoots K ) )
6 primrootscoprmpow.6 
 |-  U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
7 eqid 
 |-  ( Base ` ( R |`s U ) ) = ( Base ` ( R |`s U ) )
8 eqid 
 |-  ( .g ` ( R |`s U ) ) = ( .g ` ( R |`s U ) )
9 1 2 6 primrootsunit 
 |-  ( ph -> ( ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) /\ ( R |`s U ) e. Abel ) )
10 9 simprd 
 |-  ( ph -> ( R |`s U ) e. Abel )
11 10 ablcmnd 
 |-  ( ph -> ( R |`s U ) e. CMnd )
12 11 cmnmndd 
 |-  ( ph -> ( R |`s U ) e. Mnd )
13 3 nnnn0d 
 |-  ( ph -> E e. NN0 )
14 9 simpld 
 |-  ( ph -> ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) )
15 14 eleq2d 
 |-  ( ph -> ( M e. ( R PrimRoots K ) <-> M e. ( ( R |`s U ) PrimRoots K ) ) )
16 5 15 mpbid 
 |-  ( ph -> M e. ( ( R |`s U ) PrimRoots K ) )
17 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
18 11 17 8 isprimroot 
 |-  ( ph -> ( M e. ( ( R |`s U ) PrimRoots K ) <-> ( M e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
19 18 biimpd 
 |-  ( ph -> ( M e. ( ( R |`s U ) PrimRoots K ) -> ( M e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
20 16 19 mpd 
 |-  ( ph -> ( M e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
21 20 simp1d 
 |-  ( ph -> M e. ( Base ` ( R |`s U ) ) )
22 7 8 12 13 21 mulgnn0cld 
 |-  ( ph -> ( E ( .g ` ( R |`s U ) ) M ) e. ( Base ` ( R |`s U ) ) )
23 6 eleq2i 
 |-  ( c e. U <-> c e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
24 oveq2 
 |-  ( a = c -> ( i ( +g ` R ) a ) = ( i ( +g ` R ) c ) )
25 24 eqeq1d 
 |-  ( a = c -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( i ( +g ` R ) c ) = ( 0g ` R ) ) )
26 25 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 ) ) )
27 26 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 ) ) )
28 23 27 bitri 
 |-  ( c e. U <-> ( c e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) c ) = ( 0g ` R ) ) )
29 28 biimpi 
 |-  ( c e. U -> ( c e. ( Base ` R ) /\ E. i e. ( Base ` R ) ( i ( +g ` R ) c ) = ( 0g ` R ) ) )
30 29 simpld 
 |-  ( c e. U -> c e. ( Base ` R ) )
31 30 adantl 
 |-  ( ( ph /\ c e. U ) -> c e. ( Base ` R ) )
32 31 ex 
 |-  ( ph -> ( c e. U -> c e. ( Base ` R ) ) )
33 32 ssrdv 
 |-  ( ph -> U C_ ( Base ` R ) )
34 oveq2 
 |-  ( a = ( 0g ` R ) -> ( i ( +g ` R ) a ) = ( i ( +g ` R ) ( 0g ` R ) ) )
35 34 eqeq1d 
 |-  ( a = ( 0g ` R ) -> ( ( i ( +g ` R ) a ) = ( 0g ` R ) <-> ( i ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
36 35 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 ) ) )
37 1 cmnmndd 
 |-  ( ph -> R e. Mnd )
38 eqid 
 |-  ( Base ` R ) = ( Base ` R )
39 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
40 38 39 mndidcl 
 |-  ( R e. Mnd -> ( 0g ` R ) e. ( Base ` R ) )
41 37 40 syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
42 simpr 
 |-  ( ( ph /\ i = ( 0g ` R ) ) -> i = ( 0g ` R ) )
43 42 oveq1d 
 |-  ( ( ph /\ i = ( 0g ` R ) ) -> ( i ( +g ` R ) ( 0g ` R ) ) = ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) )
44 43 eqeq1d 
 |-  ( ( ph /\ i = ( 0g ` R ) ) -> ( ( i ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) <-> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
45 eqid 
 |-  ( +g ` R ) = ( +g ` R )
46 38 45 39 mndlid 
 |-  ( ( R e. Mnd /\ ( 0g ` R ) e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
47 37 41 46 syl2anc 
 |-  ( ph -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
48 41 44 47 rspcedvd 
 |-  ( ph -> E. i e. ( Base ` R ) ( i ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
49 36 41 48 elrabd 
 |-  ( ph -> ( 0g ` R ) e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
50 6 a1i 
 |-  ( ph -> U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } )
51 50 eleq2d 
 |-  ( ph -> ( ( 0g ` R ) e. U <-> ( 0g ` R ) e. { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) } ) )
52 49 51 mpbird 
 |-  ( ph -> ( 0g ` R ) e. U )
53 33 52 12 3jca 
 |-  ( ph -> ( U C_ ( Base ` R ) /\ ( 0g ` R ) e. U /\ ( R |`s U ) e. Mnd ) )
54 eqid 
 |-  ( R |`s U ) = ( R |`s U )
55 38 39 54 issubm2 
 |-  ( R e. Mnd -> ( U e. ( SubMnd ` R ) <-> ( U C_ ( Base ` R ) /\ ( 0g ` R ) e. U /\ ( R |`s U ) e. Mnd ) ) )
56 37 55 syl 
 |-  ( ph -> ( U e. ( SubMnd ` R ) <-> ( U C_ ( Base ` R ) /\ ( 0g ` R ) e. U /\ ( R |`s U ) e. Mnd ) ) )
57 53 56 mpbird 
 |-  ( ph -> U e. ( SubMnd ` R ) )
58 54 38 ressbas2 
 |-  ( U C_ ( Base ` R ) -> U = ( Base ` ( R |`s U ) ) )
59 33 58 syl 
 |-  ( ph -> U = ( Base ` ( R |`s U ) ) )
60 59 eleq2d 
 |-  ( ph -> ( M e. U <-> M e. ( Base ` ( R |`s U ) ) ) )
61 21 60 mpbird 
 |-  ( ph -> M e. U )
62 eqid 
 |-  ( .g ` R ) = ( .g ` R )
63 62 54 8 submmulg 
 |-  ( ( U e. ( SubMnd ` R ) /\ E e. NN0 /\ M e. U ) -> ( E ( .g ` R ) M ) = ( E ( .g ` ( R |`s U ) ) M ) )
64 57 13 61 63 syl3anc 
 |-  ( ph -> ( E ( .g ` R ) M ) = ( E ( .g ` ( R |`s U ) ) M ) )
65 64 eleq1d 
 |-  ( ph -> ( ( E ( .g ` R ) M ) e. ( Base ` ( R |`s U ) ) <-> ( E ( .g ` ( R |`s U ) ) M ) e. ( Base ` ( R |`s U ) ) ) )
66 22 65 mpbird 
 |-  ( ph -> ( E ( .g ` R ) M ) e. ( Base ` ( R |`s U ) ) )
67 64 oveq2d 
 |-  ( ph -> ( K ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( K ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) )
68 10 ablgrpd 
 |-  ( ph -> ( R |`s U ) e. Grp )
69 17 nn0zd 
 |-  ( ph -> K e. ZZ )
70 13 nn0zd 
 |-  ( ph -> E e. ZZ )
71 69 70 21 3jca 
 |-  ( ph -> ( K e. ZZ /\ E e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) )
72 7 8 mulgass 
 |-  ( ( ( R |`s U ) e. Grp /\ ( K e. ZZ /\ E e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) ) -> ( ( K x. E ) ( .g ` ( R |`s U ) ) M ) = ( K ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) )
73 68 71 72 syl2anc 
 |-  ( ph -> ( ( K x. E ) ( .g ` ( R |`s U ) ) M ) = ( K ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) )
74 2 nncnd 
 |-  ( ph -> K e. CC )
75 3 nncnd 
 |-  ( ph -> E e. CC )
76 74 75 mulcomd 
 |-  ( ph -> ( K x. E ) = ( E x. K ) )
77 76 oveq1d 
 |-  ( ph -> ( ( K x. E ) ( .g ` ( R |`s U ) ) M ) = ( ( E x. K ) ( .g ` ( R |`s U ) ) M ) )
78 70 69 21 3jca 
 |-  ( ph -> ( E e. ZZ /\ K e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) )
79 7 8 mulgass 
 |-  ( ( ( R |`s U ) e. Grp /\ ( E e. ZZ /\ K e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) ) -> ( ( E x. K ) ( .g ` ( R |`s U ) ) M ) = ( E ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) )
80 68 78 79 syl2anc 
 |-  ( ph -> ( ( E x. K ) ( .g ` ( R |`s U ) ) M ) = ( E ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) )
81 20 simp2d 
 |-  ( ph -> ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
82 81 oveq2d 
 |-  ( ph -> ( E ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) = ( E ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) )
83 eqid 
 |-  ( 0g ` ( R |`s U ) ) = ( 0g ` ( R |`s U ) )
84 7 8 83 mulgz 
 |-  ( ( ( R |`s U ) e. Grp /\ E e. ZZ ) -> ( E ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
85 68 70 84 syl2anc 
 |-  ( ph -> ( E ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
86 82 85 eqtrd 
 |-  ( ph -> ( E ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) = ( 0g ` ( R |`s U ) ) )
87 80 86 eqtrd 
 |-  ( ph -> ( ( E x. K ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
88 77 87 eqtrd 
 |-  ( ph -> ( ( K x. E ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
89 73 88 eqtr3d 
 |-  ( ph -> ( K ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) = ( 0g ` ( R |`s U ) ) )
90 67 89 eqtrd 
 |-  ( ph -> ( K ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) )
91 20 simp3d 
 |-  ( ph -> A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) )
92 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> l e. NN0 )
93 92 nn0cnd 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> l e. CC )
94 93 mullidd 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( 1 x. l ) = l )
95 94 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> l = ( 1 x. l ) )
96 simpr 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) )
97 4 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( E gcd K ) = 1 )
98 96 97 eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( ( E x. x ) + ( K x. y ) ) = 1 )
99 96 98 eqtr2d 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> 1 = ( E gcd K ) )
100 99 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( 1 x. l ) = ( ( E gcd K ) x. l ) )
101 95 100 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> l = ( ( E gcd K ) x. l ) )
102 101 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( l ( .g ` ( R |`s U ) ) M ) = ( ( ( E gcd K ) x. l ) ( .g ` ( R |`s U ) ) M ) )
103 96 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( ( E gcd K ) x. l ) = ( ( ( E x. x ) + ( K x. y ) ) x. l ) )
104 103 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( ( ( E gcd K ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( ( ( ( E x. x ) + ( K x. y ) ) x. l ) ( .g ` ( R |`s U ) ) M ) )
105 simp-4l 
 |-  ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ph /\ l e. NN0 ) )
106 simpllr 
 |-  ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) )
107 simplr 
 |-  ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> x e. ZZ )
108 105 106 107 jca31 
 |-  ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) )
109 simpr 
 |-  ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> y e. ZZ )
110 108 109 jca 
 |-  ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) )
111 75 ad4antr 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> E e. CC )
112 simplr 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> x e. ZZ )
113 112 zcnd 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> x e. CC )
114 111 113 mulcld 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( E x. x ) e. CC )
115 74 ad4antr 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> K e. CC )
116 simpr 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> y e. ZZ )
117 116 zcnd 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> y e. CC )
118 115 117 mulcld 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( K x. y ) e. CC )
119 simp-4r 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> l e. NN0 )
120 119 nn0cnd 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> l e. CC )
121 114 118 120 adddird 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( E x. x ) + ( K x. y ) ) x. l ) = ( ( ( E x. x ) x. l ) + ( ( K x. y ) x. l ) ) )
122 121 oveq1d 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( ( E x. x ) + ( K x. y ) ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( ( ( ( E x. x ) x. l ) + ( ( K x. y ) x. l ) ) ( .g ` ( R |`s U ) ) M ) )
123 68 ad4antr 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( R |`s U ) e. Grp )
124 70 ad4antr 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> E e. ZZ )
125 124 112 zmulcld 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( E x. x ) e. ZZ )
126 119 nn0zd 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> l e. ZZ )
127 125 126 zmulcld 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( E x. x ) x. l ) e. ZZ )
128 69 ad4antr 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> K e. ZZ )
129 128 116 zmulcld 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( K x. y ) e. ZZ )
130 129 126 zmulcld 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( K x. y ) x. l ) e. ZZ )
131 21 ad4antr 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> M e. ( Base ` ( R |`s U ) ) )
132 127 130 131 3jca 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( E x. x ) x. l ) e. ZZ /\ ( ( K x. y ) x. l ) e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) )
133 eqid 
 |-  ( +g ` ( R |`s U ) ) = ( +g ` ( R |`s U ) )
134 7 8 133 mulgdir 
 |-  ( ( ( R |`s U ) e. Grp /\ ( ( ( E x. x ) x. l ) e. ZZ /\ ( ( K x. y ) x. l ) e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) ) -> ( ( ( ( E x. x ) x. l ) + ( ( K x. y ) x. l ) ) ( .g ` ( R |`s U ) ) M ) = ( ( ( ( E x. x ) x. l ) ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( ( ( K x. y ) x. l ) ( .g ` ( R |`s U ) ) M ) ) )
135 123 132 134 syl2anc 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( ( E x. x ) x. l ) + ( ( K x. y ) x. l ) ) ( .g ` ( R |`s U ) ) M ) = ( ( ( ( E x. x ) x. l ) ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( ( ( K x. y ) x. l ) ( .g ` ( R |`s U ) ) M ) ) )
136 75 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> E e. CC )
137 simpr 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> x e. ZZ )
138 137 zcnd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> x e. CC )
139 simpllr 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> l e. NN0 )
140 139 nn0cnd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> l e. CC )
141 136 138 140 mulassd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( ( E x. x ) x. l ) = ( E x. ( x x. l ) ) )
142 138 140 mulcld 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( x x. l ) e. CC )
143 136 142 mulcomd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( E x. ( x x. l ) ) = ( ( x x. l ) x. E ) )
144 141 143 eqtrd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( ( E x. x ) x. l ) = ( ( x x. l ) x. E ) )
145 144 oveq1d 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( ( ( E x. x ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( ( ( x x. l ) x. E ) ( .g ` ( R |`s U ) ) M ) )
146 68 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( R |`s U ) e. Grp )
147 139 nn0zd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> l e. ZZ )
148 137 147 zmulcld 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( x x. l ) e. ZZ )
149 70 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> E e. ZZ )
150 21 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> M e. ( Base ` ( R |`s U ) ) )
151 148 149 150 3jca 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( ( x x. l ) e. ZZ /\ E e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) )
152 7 8 mulgass 
 |-  ( ( ( R |`s U ) e. Grp /\ ( ( x x. l ) e. ZZ /\ E e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) ) -> ( ( ( x x. l ) x. E ) ( .g ` ( R |`s U ) ) M ) = ( ( x x. l ) ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) )
153 146 151 152 syl2anc 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( ( ( x x. l ) x. E ) ( .g ` ( R |`s U ) ) M ) = ( ( x x. l ) ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) )
154 22 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( E ( .g ` ( R |`s U ) ) M ) e. ( Base ` ( R |`s U ) ) )
155 137 147 154 3jca 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( x e. ZZ /\ l e. ZZ /\ ( E ( .g ` ( R |`s U ) ) M ) e. ( Base ` ( R |`s U ) ) ) )
156 7 8 mulgass 
 |-  ( ( ( R |`s U ) e. Grp /\ ( x e. ZZ /\ l e. ZZ /\ ( E ( .g ` ( R |`s U ) ) M ) e. ( Base ` ( R |`s U ) ) ) ) -> ( ( x x. l ) ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) = ( x ( .g ` ( R |`s U ) ) ( l ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) ) )
157 146 155 156 syl2anc 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( ( x x. l ) ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) = ( x ( .g ` ( R |`s U ) ) ( l ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) ) )
158 57 adantr 
 |-  ( ( ph /\ l e. NN0 ) -> U e. ( SubMnd ` R ) )
159 13 adantr 
 |-  ( ( ph /\ l e. NN0 ) -> E e. NN0 )
160 61 adantr 
 |-  ( ( ph /\ l e. NN0 ) -> M e. U )
161 158 159 160 63 syl3anc 
 |-  ( ( ph /\ l e. NN0 ) -> ( E ( .g ` R ) M ) = ( E ( .g ` ( R |`s U ) ) M ) )
162 161 ad2antrr 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( E ( .g ` R ) M ) = ( E ( .g ` ( R |`s U ) ) M ) )
163 162 eqcomd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( E ( .g ` ( R |`s U ) ) M ) = ( E ( .g ` R ) M ) )
164 163 oveq2d 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( l ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) = ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) )
165 simplr 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) )
166 164 165 eqtrd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( l ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) = ( 0g ` ( R |`s U ) ) )
167 166 oveq2d 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( x ( .g ` ( R |`s U ) ) ( l ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) ) = ( x ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) )
168 7 8 83 mulgz 
 |-  ( ( ( R |`s U ) e. Grp /\ x e. ZZ ) -> ( x ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
169 146 137 168 syl2anc 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( x ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
170 167 169 eqtrd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( x ( .g ` ( R |`s U ) ) ( l ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) ) = ( 0g ` ( R |`s U ) ) )
171 157 170 eqtrd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( ( x x. l ) ( .g ` ( R |`s U ) ) ( E ( .g ` ( R |`s U ) ) M ) ) = ( 0g ` ( R |`s U ) ) )
172 153 171 eqtrd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( ( ( x x. l ) x. E ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
173 145 172 eqtrd 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) -> ( ( ( E x. x ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
174 173 adantr 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( E x. x ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
175 simplll 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ph /\ l e. NN0 ) )
176 175 116 jca 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) )
177 74 ad2antrr 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> K e. CC )
178 simpr 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> y e. ZZ )
179 178 zcnd 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> y e. CC )
180 simplr 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> l e. NN0 )
181 180 nn0cnd 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> l e. CC )
182 177 179 181 mulassd 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( ( K x. y ) x. l ) = ( K x. ( y x. l ) ) )
183 179 181 mulcld 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( y x. l ) e. CC )
184 177 183 mulcomd 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( K x. ( y x. l ) ) = ( ( y x. l ) x. K ) )
185 182 184 eqtrd 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( ( K x. y ) x. l ) = ( ( y x. l ) x. K ) )
186 185 oveq1d 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( ( ( K x. y ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( ( ( y x. l ) x. K ) ( .g ` ( R |`s U ) ) M ) )
187 68 ad2antrr 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( R |`s U ) e. Grp )
188 180 nn0zd 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> l e. ZZ )
189 178 188 zmulcld 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( y x. l ) e. ZZ )
190 69 ad2antrr 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> K e. ZZ )
191 21 ad2antrr 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> M e. ( Base ` ( R |`s U ) ) )
192 189 190 191 3jca 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( ( y x. l ) e. ZZ /\ K e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) )
193 7 8 mulgass 
 |-  ( ( ( R |`s U ) e. Grp /\ ( ( y x. l ) e. ZZ /\ K e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) ) -> ( ( ( y x. l ) x. K ) ( .g ` ( R |`s U ) ) M ) = ( ( y x. l ) ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) )
194 187 192 193 syl2anc 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( ( ( y x. l ) x. K ) ( .g ` ( R |`s U ) ) M ) = ( ( y x. l ) ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) )
195 81 ad2antrr 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
196 195 oveq2d 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( ( y x. l ) ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) = ( ( y x. l ) ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) )
197 7 8 83 mulgz 
 |-  ( ( ( R |`s U ) e. Grp /\ ( y x. l ) e. ZZ ) -> ( ( y x. l ) ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
198 187 189 197 syl2anc 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( ( y x. l ) ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
199 196 198 eqtrd 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( ( y x. l ) ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) = ( 0g ` ( R |`s U ) ) )
200 194 199 eqtrd 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( ( ( y x. l ) x. K ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
201 186 200 eqtrd 
 |-  ( ( ( ph /\ l e. NN0 ) /\ y e. ZZ ) -> ( ( ( K x. y ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
202 176 201 syl 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( K x. y ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
203 174 202 oveq12d 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( ( E x. x ) x. l ) ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( ( ( K x. y ) x. l ) ( .g ` ( R |`s U ) ) M ) ) = ( ( 0g ` ( R |`s U ) ) ( +g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) )
204 7 83 grpidcl 
 |-  ( ( R |`s U ) e. Grp -> ( 0g ` ( R |`s U ) ) e. ( Base ` ( R |`s U ) ) )
205 123 204 syl 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( 0g ` ( R |`s U ) ) e. ( Base ` ( R |`s U ) ) )
206 7 133 83 123 205 grpridd 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( 0g ` ( R |`s U ) ) ( +g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
207 203 206 eqtrd 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( ( E x. x ) x. l ) ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( ( ( K x. y ) x. l ) ( .g ` ( R |`s U ) ) M ) ) = ( 0g ` ( R |`s U ) ) )
208 135 207 eqtrd 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( ( E x. x ) x. l ) + ( ( K x. y ) x. l ) ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
209 122 208 eqtrd 
 |-  ( ( ( ( ( ph /\ l e. NN0 ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( ( E x. x ) + ( K x. y ) ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
210 110 209 syl 
 |-  ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( ( ( E x. x ) + ( K x. y ) ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
211 210 adantr 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( ( ( ( E x. x ) + ( K x. y ) ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
212 104 211 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( ( ( E gcd K ) x. l ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
213 102 212 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
214 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) )
215 213 214 mpd 
 |-  ( ( ( ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) /\ x e. ZZ ) /\ y e. ZZ ) /\ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) ) -> K || l )
216 bezout 
 |-  ( ( E e. ZZ /\ K e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) )
217 70 69 216 syl2anc 
 |-  ( ph -> E. x e. ZZ E. y e. ZZ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) )
218 217 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) -> E. x e. ZZ E. y e. ZZ ( E gcd K ) = ( ( E x. x ) + ( K x. y ) ) )
219 215 218 r19.29vva 
 |-  ( ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) /\ ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) ) -> K || l )
220 219 ex 
 |-  ( ( ( ph /\ l e. NN0 ) /\ ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) -> ( ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) -> K || l ) )
221 220 ex 
 |-  ( ( ph /\ l e. NN0 ) -> ( ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) -> ( ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
222 221 ralimdva 
 |-  ( ph -> ( A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) -> A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
223 91 222 mpd 
 |-  ( ph -> A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) -> K || l ) )
224 66 90 223 3jca 
 |-  ( ph -> ( ( E ( .g ` R ) M ) e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
225 nnnn0 
 |-  ( K e. NN -> K e. NN0 )
226 2 225 syl 
 |-  ( ph -> K e. NN0 )
227 11 226 8 isprimroot 
 |-  ( ph -> ( ( E ( .g ` R ) M ) e. ( ( R |`s U ) PrimRoots K ) <-> ( ( E ( .g ` R ) M ) e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) ( E ( .g ` R ) M ) ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
228 224 227 mpbird 
 |-  ( ph -> ( E ( .g ` R ) M ) e. ( ( R |`s U ) PrimRoots K ) )
229 14 eleq2d 
 |-  ( ph -> ( ( E ( .g ` R ) M ) e. ( R PrimRoots K ) <-> ( E ( .g ` R ) M ) e. ( ( R |`s U ) PrimRoots K ) ) )
230 228 229 mpbird 
 |-  ( ph -> ( E ( .g ` R ) M ) e. ( R PrimRoots K ) )