Metamath Proof Explorer

Theorem aks6d1c6lem2

Description: Every primitive root is root of G(u)-G(v). (Contributed by metakunt, 8-May-2025)

Ref Expression
Hypotheses aks6d1c6.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 ) ) ) }
aks6d1c6.2 
|- P = ( chr ` K )
aks6d1c6.3 
|- ( ph -> K e. Field )
aks6d1c6.4 
|- ( ph -> P e. Prime )
aks6d1c6.5 
|- ( ph -> R e. NN )
aks6d1c6.6 
|- ( ph -> N e. NN )
aks6d1c6.7 
|- ( ph -> P || N )
aks6d1c6.8 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c6.9 
|- ( ph -> A < P )
aks6d1c6.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 ) ) ) ) ) ) )
aks6d1c6.11 
|- ( ph -> A e. NN0 )
aks6d1c6.12 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
aks6d1c6.13 
|- L = ( ZRHom ` ( Z/nZ ` R ) )
aks6d1c6.14 
|- ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
aks6d1c6.15 
|- ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
aks6d1c6.16 
|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
aks6d1c6.17 
|- H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
aks6d1c6.18 
|- D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) )
aks6d1c6.19 
|- S = { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) }
aks6d1c6lem2.1 
|- ( ph -> U e. S )
aks6d1c6lem2.2 
|- ( ph -> V e. S )
aks6d1c6lem2.3 
|- ( ph -> ( ( H |` S ) ` U ) = ( ( H |` S ) ` V ) )
aks6d1c6lem2.4 
|- ( ph -> U =/= V )
aks6d1c6lem2.5 
|- J = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) )
aks6d1c6lem2.6 
|- ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( # ` ( J " ( NN0 X. NN0 ) ) ) )
Assertion aks6d1c6lem2 
|- ( ph -> D <_ ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c6.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 aks6d1c6.2 
 |-  P = ( chr ` K )
3 aks6d1c6.3 
 |-  ( ph -> K e. Field )
4 aks6d1c6.4 
 |-  ( ph -> P e. Prime )
5 aks6d1c6.5 
 |-  ( ph -> R e. NN )
6 aks6d1c6.6 
 |-  ( ph -> N e. NN )
7 aks6d1c6.7 
 |-  ( ph -> P || N )
8 aks6d1c6.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks6d1c6.9 
 |-  ( ph -> A < P )
10 aks6d1c6.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 aks6d1c6.11 
 |-  ( ph -> A e. NN0 )
12 aks6d1c6.12 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
13 aks6d1c6.13 
 |-  L = ( ZRHom ` ( Z/nZ ` R ) )
14 aks6d1c6.14 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
15 aks6d1c6.15 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
16 aks6d1c6.16 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
17 aks6d1c6.17 
 |-  H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
18 aks6d1c6.18 
 |-  D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) )
19 aks6d1c6.19 
 |-  S = { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) }
20 aks6d1c6lem2.1 
 |-  ( ph -> U e. S )
21 aks6d1c6lem2.2 
 |-  ( ph -> V e. S )
22 aks6d1c6lem2.3 
 |-  ( ph -> ( ( H |` S ) ` U ) = ( ( H |` S ) ` V ) )
23 aks6d1c6lem2.4 
 |-  ( ph -> U =/= V )
24 aks6d1c6lem2.5 
 |-  J = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) )
25 aks6d1c6lem2.6 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( # ` ( J " ( NN0 X. NN0 ) ) ) )
26 fvexd 
 |-  ( ph -> ( ZRHom ` ( Z/nZ ` R ) ) e. _V )
27 13 26 eqeltrid 
 |-  ( ph -> L e. _V )
28 27 imaexd 
 |-  ( ph -> ( L " ( E " ( NN0 X. NN0 ) ) ) e. _V )
29 hashxrcl 
 |-  ( ( L " ( E " ( NN0 X. NN0 ) ) ) e. _V -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR* )
30 28 29 syl 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR* )
31 18 30 eqeltrid 
 |-  ( ph -> D e. RR* )
32 24 a1i 
 |-  ( ph -> J = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) )
33 nn0ex 
 |-  NN0 e. _V
34 33 a1i 
 |-  ( ph -> NN0 e. _V )
35 34 34 xpexd 
 |-  ( ph -> ( NN0 X. NN0 ) e. _V )
36 35 mptexd 
 |-  ( ph -> ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) e. _V )
37 32 36 eqeltrd 
 |-  ( ph -> J e. _V )
38 37 imaexd 
 |-  ( ph -> ( J " ( NN0 X. NN0 ) ) e. _V )
39 hashxrcl 
 |-  ( ( J " ( NN0 X. NN0 ) ) e. _V -> ( # ` ( J " ( NN0 X. NN0 ) ) ) e. RR* )
40 38 39 syl 
 |-  ( ph -> ( # ` ( J " ( NN0 X. NN0 ) ) ) e. RR* )
41 fvexd 
 |-  ( ph -> ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) e. _V )
42 cnvexg 
 |-  ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) e. _V -> `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) e. _V )
43 41 42 syl 
 |-  ( ph -> `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) e. _V )
44 43 imaexd 
 |-  ( ph -> ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) e. _V )
45 hashxrcl 
 |-  ( ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) e. _V -> ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) ) e. RR* )
46 44 45 syl 
 |-  ( ph -> ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) ) e. RR* )
47 18 a1i 
 |-  ( ph -> D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
48 47 25 eqbrtrd 
 |-  ( ph -> D <_ ( # ` ( J " ( NN0 X. NN0 ) ) ) )
49 44 elexd 
 |-  ( ph -> ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) e. _V )
50 nfv 
 |-  F/ w ph
51 ovexd 
 |-  ( ( ph /\ j e. ( NN0 X. NN0 ) ) -> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) e. _V )
52 51 24 fmptd 
 |-  ( ph -> J : ( NN0 X. NN0 ) --> _V )
53 ffun 
 |-  ( J : ( NN0 X. NN0 ) --> _V -> Fun J )
54 52 53 syl 
 |-  ( ph -> Fun J )
55 24 a1i 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> J = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) )
56 simpr 
 |-  ( ( ( ph /\ w e. ( NN0 X. NN0 ) ) /\ j = w ) -> j = w )
57 56 fveq2d 
 |-  ( ( ( ph /\ w e. ( NN0 X. NN0 ) ) /\ j = w ) -> ( E ` j ) = ( E ` w ) )
58 57 oveq1d 
 |-  ( ( ( ph /\ w e. ( NN0 X. NN0 ) ) /\ j = w ) -> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) = ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) )
59 simpr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> w e. ( NN0 X. NN0 ) )
60 ovexd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) e. _V )
61 55 58 59 60 fvmptd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( J ` w ) = ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) )
62 eqid 
 |-  ( eval1 ` K ) = ( eval1 ` K )
63 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
64 eqid 
 |-  ( Base ` K ) = ( Base ` K )
65 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
66 3 fldcrngd 
 |-  ( ph -> K e. CRing )
67 66 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> K e. CRing )
68 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
69 68 64 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
70 eqid 
 |-  ( .g ` ( mulGrp ` K ) ) = ( .g ` ( mulGrp ` K ) )
71 66 crngringd 
 |-  ( ph -> K e. Ring )
72 68 ringmgp 
 |-  ( K e. Ring -> ( mulGrp ` K ) e. Mnd )
73 71 72 syl 
 |-  ( ph -> ( mulGrp ` K ) e. Mnd )
74 73 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( mulGrp ` K ) e. Mnd )
75 6 4 7 12 aks6d1c2p1 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> NN )
76 75 ffvelcdmda 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( E ` w ) e. NN )
77 76 nnnn0d 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( E ` w ) e. NN0 )
78 68 crngmgp 
 |-  ( K e. CRing -> ( mulGrp ` K ) e. CMnd )
79 66 78 syl 
 |-  ( ph -> ( mulGrp ` K ) e. CMnd )
80 5 nnnn0d 
 |-  ( ph -> R e. NN0 )
81 79 80 70 isprimroot 
 |-  ( ph -> ( M e. ( ( mulGrp ` K ) PrimRoots R ) <-> ( M e. ( Base ` ( mulGrp ` K ) ) /\ ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) /\ A. o e. NN0 ( ( o ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) -> R || o ) ) ) )
82 16 81 mpbid 
 |-  ( ph -> ( M e. ( Base ` ( mulGrp ` K ) ) /\ ( R ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) /\ A. o e. NN0 ( ( o ( .g ` ( mulGrp ` K ) ) M ) = ( 0g ` ( mulGrp ` K ) ) -> R || o ) ) )
83 82 simp1d 
 |-  ( ph -> M e. ( Base ` ( mulGrp ` K ) ) )
84 83 69 eleqtrrdi 
 |-  ( ph -> M e. ( Base ` K ) )
85 84 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> M e. ( Base ` K ) )
86 69 70 74 77 85 mulgnn0cld 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) e. ( Base ` K ) )
87 eqid 
 |-  ( var1 ` K ) = ( var1 ` K )
88 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
89 3 4 2 11 9 87 88 10 aks6d1c5lem0 
 |-  ( ph -> G : ( NN0 ^m ( 0 ... A ) ) --> ( Base ` ( Poly1 ` K ) ) )
90 19 eleq2i 
 |-  ( U e. S <-> U e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } )
91 20 90 sylib 
 |-  ( ph -> U e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } )
92 elrabi 
 |-  ( U e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } -> U e. ( NN0 ^m ( 0 ... A ) ) )
93 92 a1i 
 |-  ( ph -> ( U e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } -> U e. ( NN0 ^m ( 0 ... A ) ) ) )
94 91 93 mpd 
 |-  ( ph -> U e. ( NN0 ^m ( 0 ... A ) ) )
95 89 94 ffvelcdmd 
 |-  ( ph -> ( G ` U ) e. ( Base ` ( Poly1 ` K ) ) )
96 95 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( G ` U ) e. ( Base ` ( Poly1 ` K ) ) )
97 eqidd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) )
98 96 97 jca 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( G ` U ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ) )
99 19 eleq2i 
 |-  ( V e. S <-> V e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } )
100 21 99 sylib 
 |-  ( ph -> V e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } )
101 elrabi 
 |-  ( V e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } -> V e. ( NN0 ^m ( 0 ... A ) ) )
102 101 a1i 
 |-  ( ph -> ( V e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } -> V e. ( NN0 ^m ( 0 ... A ) ) ) )
103 100 102 mpd 
 |-  ( ph -> V e. ( NN0 ^m ( 0 ... A ) ) )
104 89 103 ffvelcdmd 
 |-  ( ph -> ( G ` V ) e. ( Base ` ( Poly1 ` K ) ) )
105 104 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( G ` V ) e. ( Base ` ( Poly1 ` K ) ) )
106 eqidd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) )
107 105 106 jca 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( G ` V ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ) )
108 eqid 
 |-  ( -g ` ( Poly1 ` K ) ) = ( -g ` ( Poly1 ` K ) )
109 eqid 
 |-  ( -g ` K ) = ( -g ` K )
110 62 63 64 65 67 86 98 107 108 109 evl1subd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ( -g ` K ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ) ) )
111 110 simprd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ( -g ` K ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ) )
112 fveq2 
 |-  ( y = M -> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` y ) = ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) )
113 112 oveq2d 
 |-  ( y = M -> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` U ) ) ` y ) ) = ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) ) )
114 oveq2 
 |-  ( y = M -> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) y ) = ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) )
115 114 fveq2d 
 |-  ( y = M -> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) y ) ) = ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) )
116 113 115 eqeq12d 
 |-  ( y = M -> ( ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` U ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) y ) ) <-> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) ) = ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ) )
117 vex 
 |-  k e. _V
118 vex 
 |-  l e. _V
119 117 118 op1std 
 |-  ( s = <. k , l >. -> ( 1st ` s ) = k )
120 119 oveq2d 
 |-  ( s = <. k , l >. -> ( P ^ ( 1st ` s ) ) = ( P ^ k ) )
121 117 118 op2ndd 
 |-  ( s = <. k , l >. -> ( 2nd ` s ) = l )
122 121 oveq2d 
 |-  ( s = <. k , l >. -> ( ( N / P ) ^ ( 2nd ` s ) ) = ( ( N / P ) ^ l ) )
123 120 122 oveq12d 
 |-  ( s = <. k , l >. -> ( ( P ^ ( 1st ` s ) ) x. ( ( N / P ) ^ ( 2nd ` s ) ) ) = ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
124 123 mpompt 
 |-  ( s e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` s ) ) x. ( ( N / P ) ^ ( 2nd ` s ) ) ) ) = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
125 12 eqcomi 
 |-  ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) = E
126 124 125 eqtri 
 |-  ( s e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` s ) ) x. ( ( N / P ) ^ ( 2nd ` s ) ) ) ) = E
127 126 eqcomi 
 |-  E = ( s e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` s ) ) x. ( ( N / P ) ^ ( 2nd ` s ) ) ) )
128 127 a1i 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> E = ( s e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` s ) ) x. ( ( N / P ) ^ ( 2nd ` s ) ) ) ) )
129 simpr 
 |-  ( ( ( ph /\ w e. ( NN0 X. NN0 ) ) /\ s = w ) -> s = w )
130 129 fveq2d 
 |-  ( ( ( ph /\ w e. ( NN0 X. NN0 ) ) /\ s = w ) -> ( 1st ` s ) = ( 1st ` w ) )
131 130 oveq2d 
 |-  ( ( ( ph /\ w e. ( NN0 X. NN0 ) ) /\ s = w ) -> ( P ^ ( 1st ` s ) ) = ( P ^ ( 1st ` w ) ) )
132 129 fveq2d 
 |-  ( ( ( ph /\ w e. ( NN0 X. NN0 ) ) /\ s = w ) -> ( 2nd ` s ) = ( 2nd ` w ) )
133 132 oveq2d 
 |-  ( ( ( ph /\ w e. ( NN0 X. NN0 ) ) /\ s = w ) -> ( ( N / P ) ^ ( 2nd ` s ) ) = ( ( N / P ) ^ ( 2nd ` w ) ) )
134 131 133 oveq12d 
 |-  ( ( ( ph /\ w e. ( NN0 X. NN0 ) ) /\ s = w ) -> ( ( P ^ ( 1st ` s ) ) x. ( ( N / P ) ^ ( 2nd ` s ) ) ) = ( ( P ^ ( 1st ` w ) ) x. ( ( N / P ) ^ ( 2nd ` w ) ) ) )
135 ovexd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( P ^ ( 1st ` w ) ) x. ( ( N / P ) ^ ( 2nd ` w ) ) ) e. _V )
136 128 134 59 135 fvmptd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( E ` w ) = ( ( P ^ ( 1st ` w ) ) x. ( ( N / P ) ^ ( 2nd ` w ) ) ) )
137 3 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> K e. Field )
138 4 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> P e. Prime )
139 5 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> R e. NN )
140 6 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> N e. NN )
141 7 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> P || N )
142 8 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( N gcd R ) = 1 )
143 ovexd 
 |-  ( ph -> ( 0 ... A ) e. _V )
144 34 143 elmapd 
 |-  ( ph -> ( U e. ( NN0 ^m ( 0 ... A ) ) <-> U : ( 0 ... A ) --> NN0 ) )
145 94 144 mpbid 
 |-  ( ph -> U : ( 0 ... A ) --> NN0 )
146 145 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> U : ( 0 ... A ) --> NN0 )
147 11 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> A e. NN0 )
148 xp1st 
 |-  ( w e. ( NN0 X. NN0 ) -> ( 1st ` w ) e. NN0 )
149 148 adantl 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( 1st ` w ) e. NN0 )
150 xp2nd 
 |-  ( w e. ( NN0 X. NN0 ) -> ( 2nd ` w ) e. NN0 )
151 150 adantl 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( 2nd ` w ) e. NN0 )
152 eqid 
 |-  ( ( P ^ ( 1st ` w ) ) x. ( ( N / P ) ^ ( 2nd ` w ) ) ) = ( ( P ^ ( 1st ` w ) ) x. ( ( N / P ) ^ ( 2nd ` w ) ) )
153 14 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
154 15 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
155 1 2 137 138 139 140 141 142 146 10 147 149 151 152 153 154 aks6d1c1rh 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( P ^ ( 1st ` w ) ) x. ( ( N / P ) ^ ( 2nd ` w ) ) ) .~ ( G ` U ) )
156 136 155 eqbrtrd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( E ` w ) .~ ( G ` U ) )
157 1 96 76 aks6d1c1p1 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( E ` w ) .~ ( G ` U ) <-> A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` U ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) y ) ) ) )
158 156 157 mpbid 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` U ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) y ) ) )
159 16 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
160 116 158 159 rspcdva 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) ) = ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) )
161 160 eqcomd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) ) )
162 17 a1i 
 |-  ( ph -> H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) ) )
163 162 reseq1d 
 |-  ( ph -> ( H |` S ) = ( ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) ) |` S ) )
164 19 a1i 
 |-  ( ph -> S = { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } )
165 ssrab2 
 |-  { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } C_ ( NN0 ^m ( 0 ... A ) )
166 165 a1i 
 |-  ( ph -> { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } C_ ( NN0 ^m ( 0 ... A ) ) )
167 164 166 eqsstrd 
 |-  ( ph -> S C_ ( NN0 ^m ( 0 ... A ) ) )
168 167 resmptd 
 |-  ( ph -> ( ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) ) |` S ) = ( h e. S |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) ) )
169 163 168 eqtrd 
 |-  ( ph -> ( H |` S ) = ( h e. S |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) ) )
170 simpr 
 |-  ( ( ph /\ h = U ) -> h = U )
171 170 fveq2d 
 |-  ( ( ph /\ h = U ) -> ( G ` h ) = ( G ` U ) )
172 171 fveq2d 
 |-  ( ( ph /\ h = U ) -> ( ( eval1 ` K ) ` ( G ` h ) ) = ( ( eval1 ` K ) ` ( G ` U ) ) )
173 172 fveq1d 
 |-  ( ( ph /\ h = U ) -> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) = ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) )
174 fvexd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) e. _V )
175 169 173 20 174 fvmptd 
 |-  ( ph -> ( ( H |` S ) ` U ) = ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) )
176 175 eqcomd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) = ( ( H |` S ) ` U ) )
177 simpr 
 |-  ( ( ph /\ h = V ) -> h = V )
178 177 fveq2d 
 |-  ( ( ph /\ h = V ) -> ( G ` h ) = ( G ` V ) )
179 178 fveq2d 
 |-  ( ( ph /\ h = V ) -> ( ( eval1 ` K ) ` ( G ` h ) ) = ( ( eval1 ` K ) ` ( G ` V ) ) )
180 179 fveq1d 
 |-  ( ( ph /\ h = V ) -> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` M ) )
181 fvexd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( G ` V ) ) ` M ) e. _V )
182 169 180 21 181 fvmptd 
 |-  ( ph -> ( ( H |` S ) ` V ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` M ) )
183 176 22 182 3eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` M ) )
184 183 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` M ) )
185 184 oveq2d 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` U ) ) ` M ) ) = ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` M ) ) )
186 161 185 eqtrd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` M ) ) )
187 fveq2 
 |-  ( y = M -> ( ( ( eval1 ` K ) ` ( G ` V ) ) ` y ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` M ) )
188 187 oveq2d 
 |-  ( y = M -> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` y ) ) = ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` M ) ) )
189 114 fveq2d 
 |-  ( y = M -> ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) y ) ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) )
190 188 189 eqeq12d 
 |-  ( y = M -> ( ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) y ) ) <-> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` M ) ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ) )
191 34 143 elmapd 
 |-  ( ph -> ( V e. ( NN0 ^m ( 0 ... A ) ) <-> V : ( 0 ... A ) --> NN0 ) )
192 103 191 mpbid 
 |-  ( ph -> V : ( 0 ... A ) --> NN0 )
193 192 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> V : ( 0 ... A ) --> NN0 )
194 1 2 137 138 139 140 141 142 193 10 147 149 151 152 153 154 aks6d1c1rh 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( P ^ ( 1st ` w ) ) x. ( ( N / P ) ^ ( 2nd ` w ) ) ) .~ ( G ` V ) )
195 136 194 eqbrtrd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( E ` w ) .~ ( G ` V ) )
196 1 105 76 aks6d1c1p1 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( E ` w ) .~ ( G ` V ) <-> A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) y ) ) ) )
197 195 196 mpbid 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` y ) ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) y ) ) )
198 190 197 159 rspcdva 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` M ) ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) )
199 186 198 eqtrd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) )
200 66 crnggrpd 
 |-  ( ph -> K e. Grp )
201 200 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> K e. Grp )
202 62 63 64 65 67 86 96 fveval1fvcl 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) e. ( Base ` K ) )
203 62 63 64 65 67 86 105 fveval1fvcl 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) e. ( Base ` K ) )
204 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
205 64 204 109 grpsubeq0 
 |-  ( ( K e. Grp /\ ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) e. ( Base ` K ) /\ ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) e. ( Base ` K ) ) -> ( ( ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ( -g ` K ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ) = ( 0g ` K ) <-> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ) )
206 201 202 203 205 syl3anc 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ( -g ` K ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ) = ( 0g ` K ) <-> ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ) )
207 199 206 mpbird 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( ( eval1 ` K ) ` ( G ` U ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ( -g ` K ) ( ( ( eval1 ` K ) ` ( G ` V ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) ) = ( 0g ` K ) )
208 111 207 eqtrd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( 0g ` K ) )
209 fvexd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) e. _V )
210 elsng 
 |-  ( ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) e. _V -> ( ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) e. { ( 0g ` K ) } <-> ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( 0g ` K ) ) )
211 209 210 syl 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) e. { ( 0g ` K ) } <-> ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( 0g ` K ) ) )
212 208 211 mpbird 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) e. { ( 0g ` K ) } )
213 eqid 
 |-  ( K ^s ( Base ` K ) ) = ( K ^s ( Base ` K ) )
214 62 63 213 64 evl1rhm 
 |-  ( K e. CRing -> ( eval1 ` K ) e. ( ( Poly1 ` K ) RingHom ( K ^s ( Base ` K ) ) ) )
215 66 214 syl 
 |-  ( ph -> ( eval1 ` K ) e. ( ( Poly1 ` K ) RingHom ( K ^s ( Base ` K ) ) ) )
216 eqid 
 |-  ( Base ` ( K ^s ( Base ` K ) ) ) = ( Base ` ( K ^s ( Base ` K ) ) )
217 65 216 rhmf 
 |-  ( ( eval1 ` K ) e. ( ( Poly1 ` K ) RingHom ( K ^s ( Base ` K ) ) ) -> ( eval1 ` K ) : ( Base ` ( Poly1 ` K ) ) --> ( Base ` ( K ^s ( Base ` K ) ) ) )
218 215 217 syl 
 |-  ( ph -> ( eval1 ` K ) : ( Base ` ( Poly1 ` K ) ) --> ( Base ` ( K ^s ( Base ` K ) ) ) )
219 fvexd 
 |-  ( ph -> ( Base ` K ) e. _V )
220 213 64 pwsbas 
 |-  ( ( K e. Field /\ ( Base ` K ) e. _V ) -> ( ( Base ` K ) ^m ( Base ` K ) ) = ( Base ` ( K ^s ( Base ` K ) ) ) )
221 3 219 220 syl2anc 
 |-  ( ph -> ( ( Base ` K ) ^m ( Base ` K ) ) = ( Base ` ( K ^s ( Base ` K ) ) ) )
222 221 feq3d 
 |-  ( ph -> ( ( eval1 ` K ) : ( Base ` ( Poly1 ` K ) ) --> ( ( Base ` K ) ^m ( Base ` K ) ) <-> ( eval1 ` K ) : ( Base ` ( Poly1 ` K ) ) --> ( Base ` ( K ^s ( Base ` K ) ) ) ) )
223 218 222 mpbird 
 |-  ( ph -> ( eval1 ` K ) : ( Base ` ( Poly1 ` K ) ) --> ( ( Base ` K ) ^m ( Base ` K ) ) )
224 63 ply1ring 
 |-  ( K e. Ring -> ( Poly1 ` K ) e. Ring )
225 71 224 syl 
 |-  ( ph -> ( Poly1 ` K ) e. Ring )
226 ringgrp 
 |-  ( ( Poly1 ` K ) e. Ring -> ( Poly1 ` K ) e. Grp )
227 225 226 syl 
 |-  ( ph -> ( Poly1 ` K ) e. Grp )
228 65 108 grpsubcl 
 |-  ( ( ( Poly1 ` K ) e. Grp /\ ( G ` U ) e. ( Base ` ( Poly1 ` K ) ) /\ ( G ` V ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) e. ( Base ` ( Poly1 ` K ) ) )
229 227 95 104 228 syl3anc 
 |-  ( ph -> ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) e. ( Base ` ( Poly1 ` K ) ) )
230 223 229 ffvelcdmd 
 |-  ( ph -> ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) e. ( ( Base ` K ) ^m ( Base ` K ) ) )
231 219 219 elmapd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) e. ( ( Base ` K ) ^m ( Base ` K ) ) <-> ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) : ( Base ` K ) --> ( Base ` K ) ) )
232 230 231 mpbid 
 |-  ( ph -> ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) : ( Base ` K ) --> ( Base ` K ) )
233 232 ffund 
 |-  ( ph -> Fun ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) )
234 233 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> Fun ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) )
235 232 ffnd 
 |-  ( ph -> ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) Fn ( Base ` K ) )
236 235 adantr 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) Fn ( Base ` K ) )
237 236 fndmd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> dom ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) = ( Base ` K ) )
238 237 eqcomd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( Base ` K ) = dom ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) )
239 86 238 eleqtrd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) e. dom ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) )
240 fvimacnv 
 |-  ( ( Fun ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) /\ ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) e. dom ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ) -> ( ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) e. { ( 0g ` K ) } <-> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) e. ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) ) )
241 234 239 240 syl2anc 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) ` ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) ) e. { ( 0g ` K ) } <-> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) e. ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) ) )
242 212 241 mpbid 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( ( E ` w ) ( .g ` ( mulGrp ` K ) ) M ) e. ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) )
243 61 242 eqeltrd 
 |-  ( ( ph /\ w e. ( NN0 X. NN0 ) ) -> ( J ` w ) e. ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) )
244 50 54 243 funimassd 
 |-  ( ph -> ( J " ( NN0 X. NN0 ) ) C_ ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) )
245 hashss 
 |-  ( ( ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) e. _V /\ ( J " ( NN0 X. NN0 ) ) C_ ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) ) -> ( # ` ( J " ( NN0 X. NN0 ) ) ) <_ ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) ) )
246 49 244 245 syl2anc 
 |-  ( ph -> ( # ` ( J " ( NN0 X. NN0 ) ) ) <_ ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) ) )
247 31 40 46 48 246 xrletrd 
 |-  ( ph -> D <_ ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` U ) ( -g ` ( Poly1 ` K ) ) ( G ` V ) ) ) " { ( 0g ` K ) } ) ) )