Metamath Proof Explorer

Theorem aks6d1c2lem3

Description: Lemma for aks6d1c2 to simplify context. (Contributed by metakunt, 1-May-2025)

Ref Expression
Hypotheses aks6d1c2.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
aks6d1c2.2 
|- P = ( chr ` K )
aks6d1c2.3 
|- ( ph -> K e. Field )
aks6d1c2.4 
|- ( ph -> P e. Prime )
aks6d1c2.5 
|- ( ph -> R e. NN )
aks6d1c2.6 
|- ( ph -> N e. NN )
aks6d1c2.7 
|- ( ph -> P || N )
aks6d1c2.8 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c2.9 
|- ( ph -> F : ( 0 ... A ) --> NN0 )
aks6d1c2.10 
|- G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
aks6d1c2.11 
|- ( ph -> A e. NN0 )
aks6d1c2.12 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
aks6d1c2.13 
|- L = ( ZRHom ` ( Z/nZ ` R ) )
aks6d1c2.14 
|- ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
aks6d1c2.15 
|- ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
aks6d1c2.16 
|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
aks6d1c2.17 
|- H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
aks6d1c2.18 
|- B = ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
aks6d1c2.19 
|- C = ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) )
aks6d1c2.20 
|- ( ph -> I e. C )
aks6d1c2.21 
|- ( ph -> J e. C )
aks6d1c2.22 
|- ( ph -> I < J )
aks6d1c2.23 
|- .^ = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
aks6d1c2.24 
|- X = ( var1 ` K )
aks6d1c2.25 
|- S = ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) )
aks6d1c2.26 
|- ( ph -> U e. NN )
aks6d1c2.27 
|- ( ph -> J = ( I + ( U x. R ) ) )
aks6d1c2p3.1 
|- ( ph -> s e. ( NN0 ^m ( 0 ... A ) ) )
aks6d1c2p3.2 
|- ( ph -> r e. ( 0 ... B ) )
aks6d1c2p3.3 
|- ( ph -> o e. ( 0 ... B ) )
aks6d1c2p3.4 
|- ( ph -> J = ( r E o ) )
aks6d1c2p3.5 
|- ( ph -> p e. ( 0 ... B ) )
aks6d1c2p3.6 
|- ( ph -> q e. ( 0 ... B ) )
aks6d1c2p3.7 
|- ( ph -> I = ( p E q ) )
aks6d1c2p3.8 
|- ( ph -> I e. NN0 )
Assertion aks6d1c2lem3 
|- ( ph -> ( J ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( I ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c2.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
2 aks6d1c2.2 
 |-  P = ( chr ` K )
3 aks6d1c2.3 
 |-  ( ph -> K e. Field )
4 aks6d1c2.4 
 |-  ( ph -> P e. Prime )
5 aks6d1c2.5 
 |-  ( ph -> R e. NN )
6 aks6d1c2.6 
 |-  ( ph -> N e. NN )
7 aks6d1c2.7 
 |-  ( ph -> P || N )
8 aks6d1c2.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks6d1c2.9 
 |-  ( ph -> F : ( 0 ... A ) --> NN0 )
10 aks6d1c2.10 
 |-  G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
11 aks6d1c2.11 
 |-  ( ph -> A e. NN0 )
12 aks6d1c2.12 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
13 aks6d1c2.13 
 |-  L = ( ZRHom ` ( Z/nZ ` R ) )
14 aks6d1c2.14 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
15 aks6d1c2.15 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
16 aks6d1c2.16 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
17 aks6d1c2.17 
 |-  H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
18 aks6d1c2.18 
 |-  B = ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
19 aks6d1c2.19 
 |-  C = ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) )
20 aks6d1c2.20 
 |-  ( ph -> I e. C )
21 aks6d1c2.21 
 |-  ( ph -> J e. C )
22 aks6d1c2.22 
 |-  ( ph -> I < J )
23 aks6d1c2.23 
 |-  .^ = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
24 aks6d1c2.24 
 |-  X = ( var1 ` K )
25 aks6d1c2.25 
 |-  S = ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) )
26 aks6d1c2.26 
 |-  ( ph -> U e. NN )
27 aks6d1c2.27 
 |-  ( ph -> J = ( I + ( U x. R ) ) )
28 aks6d1c2p3.1 
 |-  ( ph -> s e. ( NN0 ^m ( 0 ... A ) ) )
29 aks6d1c2p3.2 
 |-  ( ph -> r e. ( 0 ... B ) )
30 aks6d1c2p3.3 
 |-  ( ph -> o e. ( 0 ... B ) )
31 aks6d1c2p3.4 
 |-  ( ph -> J = ( r E o ) )
32 aks6d1c2p3.5 
 |-  ( ph -> p e. ( 0 ... B ) )
33 aks6d1c2p3.6 
 |-  ( ph -> q e. ( 0 ... B ) )
34 aks6d1c2p3.7 
 |-  ( ph -> I = ( p E q ) )
35 aks6d1c2p3.8 
 |-  ( ph -> I e. NN0 )
36 12 a1i 
 |-  ( ph -> E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) )
37 simprl 
 |-  ( ( ph /\ ( k = r /\ l = o ) ) -> k = r )
38 37 oveq2d 
 |-  ( ( ph /\ ( k = r /\ l = o ) ) -> ( P ^ k ) = ( P ^ r ) )
39 simprr 
 |-  ( ( ph /\ ( k = r /\ l = o ) ) -> l = o )
40 39 oveq2d 
 |-  ( ( ph /\ ( k = r /\ l = o ) ) -> ( ( N / P ) ^ l ) = ( ( N / P ) ^ o ) )
41 38 40 oveq12d 
 |-  ( ( ph /\ ( k = r /\ l = o ) ) -> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) = ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) )
42 elfznn0 
 |-  ( r e. ( 0 ... B ) -> r e. NN0 )
43 29 42 syl 
 |-  ( ph -> r e. NN0 )
44 elfznn0 
 |-  ( o e. ( 0 ... B ) -> o e. NN0 )
45 30 44 syl 
 |-  ( ph -> o e. NN0 )
46 ovexd 
 |-  ( ph -> ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) e. _V )
47 36 41 43 45 46 ovmpod 
 |-  ( ph -> ( r E o ) = ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) )
48 31 47 eqtrd 
 |-  ( ph -> J = ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) )
49 48 oveq1d 
 |-  ( ph -> ( J ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
50 simprl 
 |-  ( ( ph /\ ( k = p /\ l = q ) ) -> k = p )
51 50 oveq2d 
 |-  ( ( ph /\ ( k = p /\ l = q ) ) -> ( P ^ k ) = ( P ^ p ) )
52 simprr 
 |-  ( ( ph /\ ( k = p /\ l = q ) ) -> l = q )
53 52 oveq2d 
 |-  ( ( ph /\ ( k = p /\ l = q ) ) -> ( ( N / P ) ^ l ) = ( ( N / P ) ^ q ) )
54 51 53 oveq12d 
 |-  ( ( ph /\ ( k = p /\ l = q ) ) -> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) = ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) )
55 elfznn0 
 |-  ( p e. ( 0 ... B ) -> p e. NN0 )
56 32 55 syl 
 |-  ( ph -> p e. NN0 )
57 elfznn0 
 |-  ( q e. ( 0 ... B ) -> q e. NN0 )
58 33 57 syl 
 |-  ( ph -> q e. NN0 )
59 ovexd 
 |-  ( ph -> ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) e. _V )
60 36 54 56 58 59 ovmpod 
 |-  ( ph -> ( p E q ) = ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) )
61 34 60 eqtrd 
 |-  ( ph -> I = ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) )
62 61 oveq1d 
 |-  ( ph -> ( I ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
63 fveq2 
 |-  ( y = M -> ( ( ( eval1 ` K ) ` ( G ` s ) ) ` y ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) )
64 63 oveq2d 
 |-  ( y = M -> ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` y ) ) = ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
65 oveq2 
 |-  ( y = M -> ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) y ) = ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) M ) )
66 65 fveq2d 
 |-  ( y = M -> ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) y ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) M ) ) )
67 64 66 eqeq12d 
 |-  ( y = M -> ( ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) y ) ) <-> ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) M ) ) ) )
68 nn0ex 
 |-  NN0 e. _V
69 68 a1i 
 |-  ( ph -> NN0 e. _V )
70 ovexd 
 |-  ( ph -> ( 0 ... A ) e. _V )
71 elmapg 
 |-  ( ( NN0 e. _V /\ ( 0 ... A ) e. _V ) -> ( s e. ( NN0 ^m ( 0 ... A ) ) <-> s : ( 0 ... A ) --> NN0 ) )
72 69 70 71 syl2anc 
 |-  ( ph -> ( s e. ( NN0 ^m ( 0 ... A ) ) <-> s : ( 0 ... A ) --> NN0 ) )
73 28 72 mpbid 
 |-  ( ph -> s : ( 0 ... A ) --> NN0 )
74 eqid 
 |-  ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) = ( ( P ^ p ) x. ( ( N / P ) ^ q ) )
75 1 2 3 4 5 6 7 8 73 10 11 56 58 74 14 15 aks6d1c1rh 
 |-  ( ph -> ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) .~ ( G ` s ) )
76 1 75 aks6d1c1p1rcl 
 |-  ( ph -> ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) e. NN /\ ( G ` s ) e. ( Base ` ( Poly1 ` K ) ) ) )
77 76 simprd 
 |-  ( ph -> ( G ` s ) e. ( Base ` ( Poly1 ` K ) ) )
78 76 simpld 
 |-  ( ph -> ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) e. NN )
79 1 77 78 aks6d1c1p1 
 |-  ( ph -> ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) .~ ( G ` s ) <-> A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) y ) ) ) )
80 75 79 mpbid 
 |-  ( ph -> A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) y ) ) )
81 67 80 16 rspcdva 
 |-  ( ph -> ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) M ) ) )
82 61 eqcomd 
 |-  ( ph -> ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) = I )
83 82 oveq1d 
 |-  ( ph -> ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) M ) = ( I ( .g ` ( mulGrp ` K ) ) M ) )
84 48 eqcomd 
 |-  ( ph -> ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) = J )
85 84 oveq1d 
 |-  ( ph -> ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) M ) = ( J ( .g ` ( mulGrp ` K ) ) M ) )
86 27 oveq1d 
 |-  ( ph -> ( J ( .g ` ( mulGrp ` K ) ) M ) = ( ( I + ( U x. R ) ) ( .g ` ( mulGrp ` K ) ) M ) )
87 3 fldcrngd 
 |-  ( ph -> K e. CRing )
88 crngring 
 |-  ( K e. CRing -> K e. Ring )
89 87 88 syl 
 |-  ( ph -> K e. Ring )
90 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
91 90 ringmgp 
 |-  ( K e. Ring -> ( mulGrp ` K ) e. Mnd )
92 89 91 syl 
 |-  ( ph -> ( mulGrp ` K ) e. Mnd )
93 26 nnnn0d 
 |-  ( ph -> U e. NN0 )
94 5 nnnn0d 
 |-  ( ph -> R e. NN0 )
95 93 94 nn0mulcld 
 |-  ( ph -> ( U x. R ) e. NN0 )
96 90 crngmgp 
 |-  ( K e. CRing -> ( mulGrp ` K ) e. CMnd )
97 87 96 syl 
 |-  ( ph -> ( mulGrp ` K ) e. CMnd )
98 eqid 
 |-  ( .g ` ( mulGrp ` K ) ) = ( .g ` ( mulGrp ` K ) )
99 97 94 98 isprimroot 
 |-  ( ph -> ( M e. ( ( mulGrp ` K ) PrimRoots R ) <-> ( M e. ( Base ` ( mulGrp ` K ) ) /\ ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) /\ A. v e. NN0 ( ( v ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) -> R || v ) ) ) )
100 99 biimpd 
 |-  ( ph -> ( M e. ( ( mulGrp ` K ) PrimRoots R ) -> ( M e. ( Base ` ( mulGrp ` K ) ) /\ ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) /\ A. v e. NN0 ( ( v ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) -> R || v ) ) ) )
101 16 100 mpd 
 |-  ( ph -> ( M e. ( Base ` ( mulGrp ` K ) ) /\ ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) /\ A. v e. NN0 ( ( v ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) -> R || v ) ) )
102 101 simp1d 
 |-  ( ph -> M e. ( Base ` ( mulGrp ` K ) ) )
103 35 95 102 3jca 
 |-  ( ph -> ( I e. NN0 /\ ( U x. R ) e. NN0 /\ M e. ( Base ` ( mulGrp ` K ) ) ) )
104 eqid 
 |-  ( Base ` ( mulGrp ` K ) ) = ( Base ` ( mulGrp ` K ) )
105 eqid 
 |-  ( +g ` ( mulGrp ` K ) ) = ( +g ` ( mulGrp ` K ) )
106 104 98 105 mulgnn0dir 
 |-  ( ( ( mulGrp ` K ) e. Mnd /\ ( I e. NN0 /\ ( U x. R ) e. NN0 /\ M e. ( Base ` ( mulGrp ` K ) ) ) ) -> ( ( I + ( U x. R ) ) ( .g ` ( mulGrp ` K ) ) M ) = ( ( I ( .g ` ( mulGrp ` K ) ) M ) ( +g ` ( mulGrp ` K ) ) ( ( U x. R ) ( .g ` ( mulGrp ` K ) ) M ) ) )
107 92 103 106 syl2anc 
 |-  ( ph -> ( ( I + ( U x. R ) ) ( .g ` ( mulGrp ` K ) ) M ) = ( ( I ( .g ` ( mulGrp ` K ) ) M ) ( +g ` ( mulGrp ` K ) ) ( ( U x. R ) ( .g ` ( mulGrp ` K ) ) M ) ) )
108 93 94 102 3jca 
 |-  ( ph -> ( U e. NN0 /\ R e. NN0 /\ M e. ( Base ` ( mulGrp ` K ) ) ) )
109 104 98 mulgnn0ass 
 |-  ( ( ( mulGrp ` K ) e. Mnd /\ ( U e. NN0 /\ R e. NN0 /\ M e. ( Base ` ( mulGrp ` K ) ) ) ) -> ( ( U x. R ) ( .g ` ( mulGrp ` K ) ) M ) = ( U ( .g ` ( mulGrp ` K ) ) ( R ( .g ` ( mulGrp ` K ) ) M ) ) )
110 92 108 109 syl2anc 
 |-  ( ph -> ( ( U x. R ) ( .g ` ( mulGrp ` K ) ) M ) = ( U ( .g ` ( mulGrp ` K ) ) ( R ( .g ` ( mulGrp ` K ) ) M ) ) )
111 101 simp2d 
 |-  ( ph -> ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) )
112 111 oveq2d 
 |-  ( ph -> ( U ( .g ` ( mulGrp ` K ) ) ( R ( .g ` ( mulGrp ` K ) ) M ) ) = ( U ( .g ` ( mulGrp ` K ) ) ( 0g ` ( mulGrp ` K ) ) ) )
113 eqid 
 |-  ( 0g ` ( mulGrp ` K ) ) = ( 0g ` ( mulGrp ` K ) )
114 104 98 113 mulgnn0z 
 |-  ( ( ( mulGrp ` K ) e. Mnd /\ U e. NN0 ) -> ( U ( .g ` ( mulGrp ` K ) ) ( 0g ` ( mulGrp ` K ) ) ) = ( 0g ` ( mulGrp ` K ) ) )
115 92 93 114 syl2anc 
 |-  ( ph -> ( U ( .g ` ( mulGrp ` K ) ) ( 0g ` ( mulGrp ` K ) ) ) = ( 0g ` ( mulGrp ` K ) ) )
116 112 115 eqtrd 
 |-  ( ph -> ( U ( .g ` ( mulGrp ` K ) ) ( R ( .g ` ( mulGrp ` K ) ) M ) ) = ( 0g ` ( mulGrp ` K ) ) )
117 110 116 eqtrd 
 |-  ( ph -> ( ( U x. R ) ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) )
118 117 oveq2d 
 |-  ( ph -> ( ( I ( .g ` ( mulGrp ` K ) ) M ) ( +g ` ( mulGrp ` K ) ) ( ( U x. R ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( I ( .g ` ( mulGrp ` K ) ) M ) ( +g ` ( mulGrp ` K ) ) ( 0g ` ( mulGrp ` K ) ) ) )
119 104 98 92 35 102 mulgnn0cld 
 |-  ( ph -> ( I ( .g ` ( mulGrp ` K ) ) M ) e. ( Base ` ( mulGrp ` K ) ) )
120 104 105 113 mndrid 
 |-  ( ( ( mulGrp ` K ) e. Mnd /\ ( I ( .g ` ( mulGrp ` K ) ) M ) e. ( Base ` ( mulGrp ` K ) ) ) -> ( ( I ( .g ` ( mulGrp ` K ) ) M ) ( +g ` ( mulGrp ` K ) ) ( 0g ` ( mulGrp ` K ) ) ) = ( I ( .g ` ( mulGrp ` K ) ) M ) )
121 92 119 120 syl2anc 
 |-  ( ph -> ( ( I ( .g ` ( mulGrp ` K ) ) M ) ( +g ` ( mulGrp ` K ) ) ( 0g ` ( mulGrp ` K ) ) ) = ( I ( .g ` ( mulGrp ` K ) ) M ) )
122 118 121 eqtrd 
 |-  ( ph -> ( ( I ( .g ` ( mulGrp ` K ) ) M ) ( +g ` ( mulGrp ` K ) ) ( ( U x. R ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( I ( .g ` ( mulGrp ` K ) ) M ) )
123 107 122 eqtrd 
 |-  ( ph -> ( ( I + ( U x. R ) ) ( .g ` ( mulGrp ` K ) ) M ) = ( I ( .g ` ( mulGrp ` K ) ) M ) )
124 86 123 eqtrd 
 |-  ( ph -> ( J ( .g ` ( mulGrp ` K ) ) M ) = ( I ( .g ` ( mulGrp ` K ) ) M ) )
125 85 124 eqtr2d 
 |-  ( ph -> ( I ( .g ` ( mulGrp ` K ) ) M ) = ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) M ) )
126 83 125 eqtrd 
 |-  ( ph -> ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) M ) = ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) M ) )
127 126 fveq2d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) M ) ) )
128 63 oveq2d 
 |-  ( y = M -> ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` y ) ) = ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
129 oveq2 
 |-  ( y = M -> ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) y ) = ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) M ) )
130 129 fveq2d 
 |-  ( y = M -> ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) y ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) M ) ) )
131 128 130 eqeq12d 
 |-  ( y = M -> ( ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) y ) ) <-> ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) M ) ) ) )
132 eqid 
 |-  ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) = ( ( P ^ r ) x. ( ( N / P ) ^ o ) )
133 1 2 3 4 5 6 7 8 73 10 11 43 45 132 14 15 aks6d1c1rh 
 |-  ( ph -> ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) .~ ( G ` s ) )
134 1 133 aks6d1c1p1rcl 
 |-  ( ph -> ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) e. NN /\ ( G ` s ) e. ( Base ` ( Poly1 ` K ) ) ) )
135 134 simpld 
 |-  ( ph -> ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) e. NN )
136 1 77 135 aks6d1c1p1 
 |-  ( ph -> ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) .~ ( G ` s ) <-> A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) y ) ) ) )
137 133 136 mpbid 
 |-  ( ph -> A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) y ) ) )
138 131 137 16 rspcdva 
 |-  ( ph -> ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) M ) ) )
139 138 eqcomd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
140 127 139 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( G ` s ) ) ` ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
141 81 140 eqtrd 
 |-  ( ph -> ( ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
142 62 141 eqtr2d 
 |-  ( ph -> ( ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( I ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
143 49 142 eqtrd 
 |-  ( ph -> ( J ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( I ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )