Metamath Proof Explorer

Theorem aks6d1c2lem4

Description: Claim 2 of Theorem 6.1 AKS, Preparation for injectivity proof. (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 ) ) )
Assertion aks6d1c2lem4 
|- ( ph -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) )

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 fvexd 
 |-  ( ph -> ( ( eval1 ` K ) ` S ) e. _V )
29 cnvexg 
 |-  ( ( ( eval1 ` K ) ` S ) e. _V -> `' ( ( eval1 ` K ) ` S ) e. _V )
30 28 29 syl 
 |-  ( ph -> `' ( ( eval1 ` K ) ` S ) e. _V )
31 30 imaexd 
 |-  ( ph -> ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) e. _V )
32 nfv 
 |-  F/ s ph
33 fvexd 
 |-  ( ( ph /\ h e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) e. _V )
34 33 17 fmptd 
 |-  ( ph -> H : ( NN0 ^m ( 0 ... A ) ) --> _V )
35 34 ffnd 
 |-  ( ph -> H Fn ( NN0 ^m ( 0 ... A ) ) )
36 35 fnfund 
 |-  ( ph -> Fun H )
37 25 a1i 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> S = ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) )
38 37 fveq2d 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( eval1 ` K ) ` S ) = ( ( eval1 ` K ) ` ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) ) )
39 38 fveq1d 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` S ) ` ( H ` s ) ) = ( ( ( eval1 ` K ) ` ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) ) ` ( H ` s ) ) )
40 eqid 
 |-  ( eval1 ` K ) = ( eval1 ` K )
41 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
42 eqid 
 |-  ( Base ` K ) = ( Base ` K )
43 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
44 3 fldcrngd 
 |-  ( ph -> K e. CRing )
45 44 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> K e. CRing )
46 17 a1i 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) ) )
47 simpr 
 |-  ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ h = s ) -> h = s )
48 47 fveq2d 
 |-  ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ h = s ) -> ( G ` h ) = ( G ` s ) )
49 48 fveq2d 
 |-  ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ h = s ) -> ( ( eval1 ` K ) ` ( G ` h ) ) = ( ( eval1 ` K ) ` ( G ` s ) ) )
50 49 fveq1d 
 |-  ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ h = s ) -> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) )
51 simpr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> s e. ( NN0 ^m ( 0 ... A ) ) )
52 fvexd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) e. _V )
53 46 50 51 52 fvmptd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( H ` s ) = ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) )
54 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
55 54 crngmgp 
 |-  ( K e. CRing -> ( mulGrp ` K ) e. CMnd )
56 44 55 syl 
 |-  ( ph -> ( mulGrp ` K ) e. CMnd )
57 5 nnnn0d 
 |-  ( ph -> R e. NN0 )
58 eqid 
 |-  ( .g ` ( mulGrp ` K ) ) = ( .g ` ( mulGrp ` K ) )
59 56 57 58 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 ) ) ) )
60 59 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 ) ) ) )
61 16 60 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 ) ) )
62 61 simp1d 
 |-  ( ph -> M e. ( Base ` ( mulGrp ` K ) ) )
63 54 42 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
64 62 63 eleqtrrdi 
 |-  ( ph -> M e. ( Base ` K ) )
65 64 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> M e. ( Base ` K ) )
66 3 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> K e. Field )
67 4 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> P e. Prime )
68 5 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> R e. NN )
69 6 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> N e. NN )
70 7 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> P || N )
71 8 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( N gcd R ) = 1 )
72 elmapi 
 |-  ( s e. ( NN0 ^m ( 0 ... A ) ) -> s : ( 0 ... A ) --> NN0 )
73 72 adantl 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> s : ( 0 ... A ) --> NN0 )
74 11 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> A e. NN0 )
75 0nn0 
 |-  0 e. NN0
76 75 a1i 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> 0 e. NN0 )
77 eqid 
 |-  ( ( P ^ 0 ) x. ( ( N / P ) ^ 0 ) ) = ( ( P ^ 0 ) x. ( ( N / P ) ^ 0 ) )
78 14 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
79 15 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
80 1 2 66 67 68 69 70 71 73 10 74 76 76 77 78 79 aks6d1c1rh 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( P ^ 0 ) x. ( ( N / P ) ^ 0 ) ) .~ ( G ` s ) )
81 1 80 aks6d1c1p1rcl 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( P ^ 0 ) x. ( ( N / P ) ^ 0 ) ) e. NN /\ ( G ` s ) e. ( Base ` ( Poly1 ` K ) ) ) )
82 81 simprd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( G ` s ) e. ( Base ` ( Poly1 ` K ) ) )
83 40 41 42 43 45 65 82 fveval1fvcl 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) e. ( Base ` K ) )
84 53 83 eqeltrd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( H ` s ) e. ( Base ` K ) )
85 eqid 
 |-  ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
86 41 ply1crng 
 |-  ( K e. CRing -> ( Poly1 ` K ) e. CRing )
87 44 86 syl 
 |-  ( ph -> ( Poly1 ` K ) e. CRing )
88 eqid 
 |-  ( mulGrp ` ( Poly1 ` K ) ) = ( mulGrp ` ( Poly1 ` K ) )
89 88 crngmgp 
 |-  ( ( Poly1 ` K ) e. CRing -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
90 87 89 syl 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
91 90 cmnmndd 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
92 simpr 
 |-  ( ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) -> J = ( r E o ) )
93 12 a1i 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) )
94 simprl 
 |-  ( ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ ( k = r /\ l = o ) ) -> k = r )
95 94 oveq2d 
 |-  ( ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ ( k = r /\ l = o ) ) -> ( P ^ k ) = ( P ^ r ) )
96 simprr 
 |-  ( ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ ( k = r /\ l = o ) ) -> l = o )
97 96 oveq2d 
 |-  ( ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ ( k = r /\ l = o ) ) -> ( ( N / P ) ^ l ) = ( ( N / P ) ^ o ) )
98 95 97 oveq12d 
 |-  ( ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ ( k = r /\ l = o ) ) -> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) = ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) )
99 fz0ssnn0 
 |-  ( 0 ... B ) C_ NN0
100 99 a1i 
 |-  ( ph -> ( 0 ... B ) C_ NN0 )
101 100 sselda 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> r e. NN0 )
102 101 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> r e. NN0 )
103 99 sseli 
 |-  ( o e. ( 0 ... B ) -> o e. NN0 )
104 103 adantl 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> o e. NN0 )
105 ovexd 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) e. _V )
106 93 98 102 104 105 ovmpod 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( r E o ) = ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) )
107 prmnn 
 |-  ( P e. Prime -> P e. NN )
108 4 107 syl 
 |-  ( ph -> P e. NN )
109 108 nnnn0d 
 |-  ( ph -> P e. NN0 )
110 109 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> P e. NN0 )
111 110 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> P e. NN0 )
112 111 102 nn0expcld 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( P ^ r ) e. NN0 )
113 109 nn0zd 
 |-  ( ph -> P e. ZZ )
114 108 nnne0d 
 |-  ( ph -> P =/= 0 )
115 6 nnnn0d 
 |-  ( ph -> N e. NN0 )
116 115 nn0zd 
 |-  ( ph -> N e. ZZ )
117 dvdsval2 
 |-  ( ( P e. ZZ /\ P =/= 0 /\ N e. ZZ ) -> ( P || N <-> ( N / P ) e. ZZ ) )
118 113 114 116 117 syl3anc 
 |-  ( ph -> ( P || N <-> ( N / P ) e. ZZ ) )
119 7 118 mpbid 
 |-  ( ph -> ( N / P ) e. ZZ )
120 6 nnred 
 |-  ( ph -> N e. RR )
121 108 nnrpd 
 |-  ( ph -> P e. RR+ )
122 115 nn0ge0d 
 |-  ( ph -> 0 <_ N )
123 120 121 122 divge0d 
 |-  ( ph -> 0 <_ ( N / P ) )
124 119 123 jca 
 |-  ( ph -> ( ( N / P ) e. ZZ /\ 0 <_ ( N / P ) ) )
125 elnn0z 
 |-  ( ( N / P ) e. NN0 <-> ( ( N / P ) e. ZZ /\ 0 <_ ( N / P ) ) )
126 124 125 sylibr 
 |-  ( ph -> ( N / P ) e. NN0 )
127 126 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> ( N / P ) e. NN0 )
128 127 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( N / P ) e. NN0 )
129 128 104 nn0expcld 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( N / P ) ^ o ) e. NN0 )
130 112 129 nn0mulcld 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) e. NN0 )
131 106 130 eqeltrd 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( r E o ) e. NN0 )
132 131 adantr 
 |-  ( ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) -> ( r E o ) e. NN0 )
133 92 132 eqeltrd 
 |-  ( ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) -> J e. NN0 )
134 19 a1i 
 |-  ( ph -> C = ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
135 21 134 eleqtrd 
 |-  ( ph -> J e. ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
136 6 4 7 12 aks6d1c2p1 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> NN )
137 136 ffnd 
 |-  ( ph -> E Fn ( NN0 X. NN0 ) )
138 100 100 jca 
 |-  ( ph -> ( ( 0 ... B ) C_ NN0 /\ ( 0 ... B ) C_ NN0 ) )
139 18 a1i 
 |-  ( ph -> B = ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
140 eqid 
 |-  ( Z/nZ ` R ) = ( Z/nZ ` R )
141 6 4 7 5 8 12 13 140 hashscontpowcl 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )
142 141 nn0red 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR )
143 141 nn0ge0d 
 |-  ( ph -> 0 <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
144 142 143 resqrtcld 
 |-  ( ph -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR )
145 144 flcld 
 |-  ( ph -> ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. ZZ )
146 142 143 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
147 0zd 
 |-  ( ph -> 0 e. ZZ )
148 flge 
 |-  ( ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) <-> 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
149 144 147 148 syl2anc 
 |-  ( ph -> ( 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) <-> 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
150 146 149 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
151 145 150 jca 
 |-  ( ph -> ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
152 elnn0z 
 |-  ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. NN0 <-> ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
153 151 152 sylibr 
 |-  ( ph -> ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. NN0 )
154 139 153 eqeltrd 
 |-  ( ph -> B e. NN0 )
155 elnn0z 
 |-  ( B e. NN0 <-> ( B e. ZZ /\ 0 <_ B ) )
156 154 155 sylib 
 |-  ( ph -> ( B e. ZZ /\ 0 <_ B ) )
157 0z 
 |-  0 e. ZZ
158 eluz1 
 |-  ( 0 e. ZZ -> ( B e. ( ZZ>= ` 0 ) <-> ( B e. ZZ /\ 0 <_ B ) ) )
159 157 158 ax-mp 
 |-  ( B e. ( ZZ>= ` 0 ) <-> ( B e. ZZ /\ 0 <_ B ) )
160 156 159 sylibr 
 |-  ( ph -> B e. ( ZZ>= ` 0 ) )
161 fzn0 
 |-  ( ( 0 ... B ) =/= (/) <-> B e. ( ZZ>= ` 0 ) )
162 160 161 sylibr 
 |-  ( ph -> ( 0 ... B ) =/= (/) )
163 162 162 jca 
 |-  ( ph -> ( ( 0 ... B ) =/= (/) /\ ( 0 ... B ) =/= (/) ) )
164 xpnz 
 |-  ( ( ( 0 ... B ) =/= (/) /\ ( 0 ... B ) =/= (/) ) <-> ( ( 0 ... B ) X. ( 0 ... B ) ) =/= (/) )
165 163 164 sylib 
 |-  ( ph -> ( ( 0 ... B ) X. ( 0 ... B ) ) =/= (/) )
166 ssxpb 
 |-  ( ( ( 0 ... B ) X. ( 0 ... B ) ) =/= (/) -> ( ( ( 0 ... B ) X. ( 0 ... B ) ) C_ ( NN0 X. NN0 ) <-> ( ( 0 ... B ) C_ NN0 /\ ( 0 ... B ) C_ NN0 ) ) )
167 165 166 syl 
 |-  ( ph -> ( ( ( 0 ... B ) X. ( 0 ... B ) ) C_ ( NN0 X. NN0 ) <-> ( ( 0 ... B ) C_ NN0 /\ ( 0 ... B ) C_ NN0 ) ) )
168 138 167 mpbird 
 |-  ( ph -> ( ( 0 ... B ) X. ( 0 ... B ) ) C_ ( NN0 X. NN0 ) )
169 ovelimab 
 |-  ( ( E Fn ( NN0 X. NN0 ) /\ ( ( 0 ... B ) X. ( 0 ... B ) ) C_ ( NN0 X. NN0 ) ) -> ( J e. ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) <-> E. r e. ( 0 ... B ) E. o e. ( 0 ... B ) J = ( r E o ) ) )
170 137 168 169 syl2anc 
 |-  ( ph -> ( J e. ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) <-> E. r e. ( 0 ... B ) E. o e. ( 0 ... B ) J = ( r E o ) ) )
171 135 170 mpbid 
 |-  ( ph -> E. r e. ( 0 ... B ) E. o e. ( 0 ... B ) J = ( r E o ) )
172 133 171 r19.29vva 
 |-  ( ph -> J e. NN0 )
173 44 crngringd 
 |-  ( ph -> K e. Ring )
174 24 41 43 vr1cl 
 |-  ( K e. Ring -> X e. ( Base ` ( Poly1 ` K ) ) )
175 173 174 syl 
 |-  ( ph -> X e. ( Base ` ( Poly1 ` K ) ) )
176 88 43 mgpbas 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
177 176 eqcomi 
 |-  ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( Poly1 ` K ) )
178 177 eleq2i 
 |-  ( X e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) <-> X e. ( Base ` ( Poly1 ` K ) ) )
179 175 178 sylibr 
 |-  ( ph -> X e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
180 85 23 91 172 179 mulgnn0cld 
 |-  ( ph -> ( J .^ X ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
181 180 176 eleqtrrdi 
 |-  ( ph -> ( J .^ X ) e. ( Base ` ( Poly1 ` K ) ) )
182 181 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( J .^ X ) e. ( Base ` ( Poly1 ` K ) ) )
183 175 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> X e. ( Base ` ( Poly1 ` K ) ) )
184 40 24 42 41 43 45 84 evl1vard 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( X e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` X ) ` ( H ` s ) ) = ( H ` s ) ) )
185 184 simprd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` X ) ` ( H ` s ) ) = ( H ` s ) )
186 183 185 jca 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( X e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` X ) ` ( H ` s ) ) = ( H ` s ) ) )
187 172 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> J e. NN0 )
188 40 41 42 43 45 84 186 23 58 187 evl1expd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( J .^ X ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( J .^ X ) ) ` ( H ` s ) ) = ( J ( .g ` ( mulGrp ` K ) ) ( H ` s ) ) ) )
189 188 simprd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( J .^ X ) ) ` ( H ` s ) ) = ( J ( .g ` ( mulGrp ` K ) ) ( H ` s ) ) )
190 53 oveq2d 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( J ( .g ` ( mulGrp ` K ) ) ( H ` s ) ) = ( J ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
191 3 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> K e. Field )
192 4 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> P e. Prime )
193 5 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> R e. NN )
194 6 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> N e. NN )
195 7 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> P || N )
196 8 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> ( N gcd R ) = 1 )
197 9 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> F : ( 0 ... A ) --> NN0 )
198 11 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> A e. NN0 )
199 14 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
200 15 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
201 16 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
202 20 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> I e. C )
203 21 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> J e. C )
204 22 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> I < J )
205 26 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> U e. NN )
206 27 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> J = ( I + ( U x. R ) ) )
207 51 ad6antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> s e. ( NN0 ^m ( 0 ... A ) ) )
208 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> r e. ( 0 ... B ) )
209 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> o e. ( 0 ... B ) )
210 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> J = ( r E o ) )
211 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> p e. ( 0 ... B ) )
212 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> q e. ( 0 ... B ) )
213 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> I = ( p E q ) )
214 simpr 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> I = ( p E q ) )
215 12 a1i 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) )
216 simprl 
 |-  ( ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) /\ ( k = p /\ l = q ) ) -> k = p )
217 216 oveq2d 
 |-  ( ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) /\ ( k = p /\ l = q ) ) -> ( P ^ k ) = ( P ^ p ) )
218 simprr 
 |-  ( ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) /\ ( k = p /\ l = q ) ) -> l = q )
219 218 oveq2d 
 |-  ( ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) /\ ( k = p /\ l = q ) ) -> ( ( N / P ) ^ l ) = ( ( N / P ) ^ q ) )
220 217 219 oveq12d 
 |-  ( ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) /\ ( k = p /\ l = q ) ) -> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) = ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) )
221 100 sselda 
 |-  ( ( ph /\ p e. ( 0 ... B ) ) -> p e. NN0 )
222 221 adantr 
 |-  ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) -> p e. NN0 )
223 222 adantr 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> p e. NN0 )
224 99 sseli 
 |-  ( q e. ( 0 ... B ) -> q e. NN0 )
225 224 adantl 
 |-  ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) -> q e. NN0 )
226 225 adantr 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> q e. NN0 )
227 ovexd 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) e. _V )
228 215 220 223 226 227 ovmpod 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> ( p E q ) = ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) )
229 214 228 eqtrd 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> I = ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) )
230 109 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> P e. NN0 )
231 230 223 nn0expcld 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> ( P ^ p ) e. NN0 )
232 126 ad2antrr 
 |-  ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) -> ( N / P ) e. NN0 )
233 232 adantr 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> ( N / P ) e. NN0 )
234 233 226 nn0expcld 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> ( ( N / P ) ^ q ) e. NN0 )
235 231 234 nn0mulcld 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> ( ( P ^ p ) x. ( ( N / P ) ^ q ) ) e. NN0 )
236 229 235 eqeltrd 
 |-  ( ( ( ( ph /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> I e. NN0 )
237 20 134 eleqtrd 
 |-  ( ph -> I e. ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
238 ovelimab 
 |-  ( ( E Fn ( NN0 X. NN0 ) /\ ( ( 0 ... B ) X. ( 0 ... B ) ) C_ ( NN0 X. NN0 ) ) -> ( I e. ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) <-> E. p e. ( 0 ... B ) E. q e. ( 0 ... B ) I = ( p E q ) ) )
239 137 168 238 syl2anc 
 |-  ( ph -> ( I e. ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) <-> E. p e. ( 0 ... B ) E. q e. ( 0 ... B ) I = ( p E q ) ) )
240 237 239 mpbid 
 |-  ( ph -> E. p e. ( 0 ... B ) E. q e. ( 0 ... B ) I = ( p E q ) )
241 236 240 r19.29vva 
 |-  ( ph -> I e. NN0 )
242 241 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> I e. NN0 )
243 242 ad6antr 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> I e. NN0 )
244 1 2 191 192 193 194 195 196 197 10 198 12 13 199 200 201 17 18 19 202 203 204 23 24 25 205 206 207 208 209 210 211 212 213 243 aks6d1c2lem3 
 |-  ( ( ( ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) /\ p e. ( 0 ... B ) ) /\ q e. ( 0 ... B ) ) /\ I = ( p E q ) ) -> ( J ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( I ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
245 240 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) -> E. p e. ( 0 ... B ) E. q e. ( 0 ... B ) I = ( p E q ) )
246 244 245 r19.29vva 
 |-  ( ( ( ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) -> ( J ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( I ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
247 171 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> E. r e. ( 0 ... B ) E. o e. ( 0 ... B ) J = ( r E o ) )
248 246 247 r19.29vva 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( J ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( I ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) )
249 53 eqcomd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) = ( H ` s ) )
250 249 oveq2d 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( I ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( G ` s ) ) ` M ) ) = ( I ( .g ` ( mulGrp ` K ) ) ( H ` s ) ) )
251 190 248 250 3eqtrd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( J ( .g ` ( mulGrp ` K ) ) ( H ` s ) ) = ( I ( .g ` ( mulGrp ` K ) ) ( H ` s ) ) )
252 40 41 42 43 45 84 186 23 58 242 evl1expd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( I .^ X ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) = ( I ( .g ` ( mulGrp ` K ) ) ( H ` s ) ) ) )
253 252 simprd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) = ( I ( .g ` ( mulGrp ` K ) ) ( H ` s ) ) )
254 253 eqcomd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( I ( .g ` ( mulGrp ` K ) ) ( H ` s ) ) = ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) )
255 189 251 254 3eqtrd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( J .^ X ) ) ` ( H ` s ) ) = ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) )
256 182 255 jca 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( J .^ X ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( J .^ X ) ) ` ( H ` s ) ) = ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) ) )
257 85 23 91 241 179 mulgnn0cld 
 |-  ( ph -> ( I .^ X ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
258 176 eleq2i 
 |-  ( ( I .^ X ) e. ( Base ` ( Poly1 ` K ) ) <-> ( I .^ X ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
259 257 258 sylibr 
 |-  ( ph -> ( I .^ X ) e. ( Base ` ( Poly1 ` K ) ) )
260 259 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( I .^ X ) e. ( Base ` ( Poly1 ` K ) ) )
261 eqidd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) = ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) )
262 260 261 jca 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( I .^ X ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) = ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) ) )
263 eqid 
 |-  ( -g ` ( Poly1 ` K ) ) = ( -g ` ( Poly1 ` K ) )
264 eqid 
 |-  ( -g ` K ) = ( -g ` K )
265 40 41 42 43 45 84 256 262 263 264 evl1subd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) ) ` ( H ` s ) ) = ( ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) ( -g ` K ) ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) ) ) )
266 265 simprd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) ) ` ( H ` s ) ) = ( ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) ( -g ` K ) ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) ) )
267 45 crnggrpd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> K e. Grp )
268 40 41 42 43 45 84 260 fveval1fvcl 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) e. ( Base ` K ) )
269 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
270 42 269 264 grpsubid 
 |-  ( ( K e. Grp /\ ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) e. ( Base ` K ) ) -> ( ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) ( -g ` K ) ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) ) = ( 0g ` K ) )
271 267 268 270 syl2anc 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) ( -g ` K ) ( ( ( eval1 ` K ) ` ( I .^ X ) ) ` ( H ` s ) ) ) = ( 0g ` K ) )
272 266 271 eqtrd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) ) ` ( H ` s ) ) = ( 0g ` K ) )
273 39 272 eqtrd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` S ) ` ( H ` s ) ) = ( 0g ` K ) )
274 fvexd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` S ) ` ( H ` s ) ) e. _V )
275 elsng 
 |-  ( ( ( ( eval1 ` K ) ` S ) ` ( H ` s ) ) e. _V -> ( ( ( ( eval1 ` K ) ` S ) ` ( H ` s ) ) e. { ( 0g ` K ) } <-> ( ( ( eval1 ` K ) ` S ) ` ( H ` s ) ) = ( 0g ` K ) ) )
276 274 275 syl 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( ( eval1 ` K ) ` S ) ` ( H ` s ) ) e. { ( 0g ` K ) } <-> ( ( ( eval1 ` K ) ` S ) ` ( H ` s ) ) = ( 0g ` K ) ) )
277 273 276 mpbird 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` S ) ` ( H ` s ) ) e. { ( 0g ` K ) } )
278 87 crnggrpd 
 |-  ( ph -> ( Poly1 ` K ) e. Grp )
279 43 263 grpsubcl 
 |-  ( ( ( Poly1 ` K ) e. Grp /\ ( J .^ X ) e. ( Base ` ( Poly1 ` K ) ) /\ ( I .^ X ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) e. ( Base ` ( Poly1 ` K ) ) )
280 278 181 259 279 syl3anc 
 |-  ( ph -> ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) e. ( Base ` ( Poly1 ` K ) ) )
281 25 280 eqeltrid 
 |-  ( ph -> S e. ( Base ` ( Poly1 ` K ) ) )
282 eqid 
 |-  ( K ^s ( Base ` K ) ) = ( K ^s ( Base ` K ) )
283 40 41 282 42 evl1rhm 
 |-  ( K e. CRing -> ( eval1 ` K ) e. ( ( Poly1 ` K ) RingHom ( K ^s ( Base ` K ) ) ) )
284 44 283 syl 
 |-  ( ph -> ( eval1 ` K ) e. ( ( Poly1 ` K ) RingHom ( K ^s ( Base ` K ) ) ) )
285 eqid 
 |-  ( Base ` ( K ^s ( Base ` K ) ) ) = ( Base ` ( K ^s ( Base ` K ) ) )
286 43 285 rhmf 
 |-  ( ( eval1 ` K ) e. ( ( Poly1 ` K ) RingHom ( K ^s ( Base ` K ) ) ) -> ( eval1 ` K ) : ( Base ` ( Poly1 ` K ) ) --> ( Base ` ( K ^s ( Base ` K ) ) ) )
287 284 286 syl 
 |-  ( ph -> ( eval1 ` K ) : ( Base ` ( Poly1 ` K ) ) --> ( Base ` ( K ^s ( Base ` K ) ) ) )
288 287 ffvelcdmda 
 |-  ( ( ph /\ S e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( eval1 ` K ) ` S ) e. ( Base ` ( K ^s ( Base ` K ) ) ) )
289 288 ex 
 |-  ( ph -> ( S e. ( Base ` ( Poly1 ` K ) ) -> ( ( eval1 ` K ) ` S ) e. ( Base ` ( K ^s ( Base ` K ) ) ) ) )
290 281 289 mpd 
 |-  ( ph -> ( ( eval1 ` K ) ` S ) e. ( Base ` ( K ^s ( Base ` K ) ) ) )
291 fvexd 
 |-  ( ph -> ( Base ` K ) e. _V )
292 282 42 pwsbas 
 |-  ( ( K e. Field /\ ( Base ` K ) e. _V ) -> ( ( Base ` K ) ^m ( Base ` K ) ) = ( Base ` ( K ^s ( Base ` K ) ) ) )
293 3 291 292 syl2anc 
 |-  ( ph -> ( ( Base ` K ) ^m ( Base ` K ) ) = ( Base ` ( K ^s ( Base ` K ) ) ) )
294 290 293 eleqtrrd 
 |-  ( ph -> ( ( eval1 ` K ) ` S ) e. ( ( Base ` K ) ^m ( Base ` K ) ) )
295 291 291 elmapd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` S ) e. ( ( Base ` K ) ^m ( Base ` K ) ) <-> ( ( eval1 ` K ) ` S ) : ( Base ` K ) --> ( Base ` K ) ) )
296 294 295 mpbid 
 |-  ( ph -> ( ( eval1 ` K ) ` S ) : ( Base ` K ) --> ( Base ` K ) )
297 ffn 
 |-  ( ( ( eval1 ` K ) ` S ) : ( Base ` K ) --> ( Base ` K ) -> ( ( eval1 ` K ) ` S ) Fn ( Base ` K ) )
298 296 297 syl 
 |-  ( ph -> ( ( eval1 ` K ) ` S ) Fn ( Base ` K ) )
299 298 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( eval1 ` K ) ` S ) Fn ( Base ` K ) )
300 fnfun 
 |-  ( ( ( eval1 ` K ) ` S ) Fn ( Base ` K ) -> Fun ( ( eval1 ` K ) ` S ) )
301 299 300 syl 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> Fun ( ( eval1 ` K ) ` S ) )
302 fndm 
 |-  ( ( ( eval1 ` K ) ` S ) Fn ( Base ` K ) -> dom ( ( eval1 ` K ) ` S ) = ( Base ` K ) )
303 298 302 syl 
 |-  ( ph -> dom ( ( eval1 ` K ) ` S ) = ( Base ` K ) )
304 303 adantr 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> dom ( ( eval1 ` K ) ` S ) = ( Base ` K ) )
305 84 304 eleqtrrd 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( H ` s ) e. dom ( ( eval1 ` K ) ` S ) )
306 fvimacnv 
 |-  ( ( Fun ( ( eval1 ` K ) ` S ) /\ ( H ` s ) e. dom ( ( eval1 ` K ) ` S ) ) -> ( ( ( ( eval1 ` K ) ` S ) ` ( H ` s ) ) e. { ( 0g ` K ) } <-> ( H ` s ) e. ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) )
307 301 305 306 syl2anc 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( ( eval1 ` K ) ` S ) ` ( H ` s ) ) e. { ( 0g ` K ) } <-> ( H ` s ) e. ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) )
308 277 307 mpbid 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) ) -> ( H ` s ) e. ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) )
309 32 36 308 funimassd 
 |-  ( ph -> ( H " ( NN0 ^m ( 0 ... A ) ) ) C_ ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) )
310 31 309 ssexd 
 |-  ( ph -> ( H " ( NN0 ^m ( 0 ... A ) ) ) e. _V )
311 25 a1i 
 |-  ( ph -> S = ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) )
312 311 fveq2d 
 |-  ( ph -> ( ( deg1 ` K ) ` S ) = ( ( deg1 ` K ) ` ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) ) )
313 eqid 
 |-  ( deg1 ` K ) = ( deg1 ` K )
314 isfld 
 |-  ( K e. Field <-> ( K e. DivRing /\ K e. CRing ) )
315 314 biimpi 
 |-  ( K e. Field -> ( K e. DivRing /\ K e. CRing ) )
316 315 simpld 
 |-  ( K e. Field -> K e. DivRing )
317 drngnzr 
 |-  ( K e. DivRing -> K e. NzRing )
318 316 317 syl 
 |-  ( K e. Field -> K e. NzRing )
319 3 318 syl 
 |-  ( ph -> K e. NzRing )
320 313 41 24 88 23 deg1pw 
 |-  ( ( K e. NzRing /\ I e. NN0 ) -> ( ( deg1 ` K ) ` ( I .^ X ) ) = I )
321 319 241 320 syl2anc 
 |-  ( ph -> ( ( deg1 ` K ) ` ( I .^ X ) ) = I )
322 321 eqcomd 
 |-  ( ph -> I = ( ( deg1 ` K ) ` ( I .^ X ) ) )
323 313 41 24 88 23 deg1pw 
 |-  ( ( K e. NzRing /\ J e. NN0 ) -> ( ( deg1 ` K ) ` ( J .^ X ) ) = J )
324 319 172 323 syl2anc 
 |-  ( ph -> ( ( deg1 ` K ) ` ( J .^ X ) ) = J )
325 324 eqcomd 
 |-  ( ph -> J = ( ( deg1 ` K ) ` ( J .^ X ) ) )
326 22 322 325 3brtr3d 
 |-  ( ph -> ( ( deg1 ` K ) ` ( I .^ X ) ) < ( ( deg1 ` K ) ` ( J .^ X ) ) )
327 41 313 173 43 263 181 259 326 deg1sub 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) ) = ( ( deg1 ` K ) ` ( J .^ X ) ) )
328 312 327 eqtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` S ) = ( ( deg1 ` K ) ` ( J .^ X ) ) )
329 328 324 eqtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` S ) = J )
330 329 172 eqeltrd 
 |-  ( ph -> ( ( deg1 ` K ) ` S ) e. NN0 )
331 eqid 
 |-  ( 0g ` ( Poly1 ` K ) ) = ( 0g ` ( Poly1 ` K ) )
332 fldidom 
 |-  ( K e. Field -> K e. IDomn )
333 3 332 syl 
 |-  ( ph -> K e. IDomn )
334 313 41 331 43 deg1nn0clb 
 |-  ( ( K e. Ring /\ S e. ( Base ` ( Poly1 ` K ) ) ) -> ( S =/= ( 0g ` ( Poly1 ` K ) ) <-> ( ( deg1 ` K ) ` S ) e. NN0 ) )
335 173 281 334 syl2anc 
 |-  ( ph -> ( S =/= ( 0g ` ( Poly1 ` K ) ) <-> ( ( deg1 ` K ) ` S ) e. NN0 ) )
336 330 335 mpbird 
 |-  ( ph -> S =/= ( 0g ` ( Poly1 ` K ) ) )
337 41 43 313 40 269 331 333 281 336 fta1g 
 |-  ( ph -> ( # ` ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) <_ ( ( deg1 ` K ) ` S ) )
338 hashbnd 
 |-  ( ( ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) e. _V /\ ( ( deg1 ` K ) ` S ) e. NN0 /\ ( # ` ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) <_ ( ( deg1 ` K ) ` S ) ) -> ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) e. Fin )
339 31 330 337 338 syl3anc 
 |-  ( ph -> ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) e. Fin )
340 hashcl 
 |-  ( ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) e. Fin -> ( # ` ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) e. NN0 )
341 339 340 syl 
 |-  ( ph -> ( # ` ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) e. NN0 )
342 hashss 
 |-  ( ( ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) e. _V /\ ( H " ( NN0 ^m ( 0 ... A ) ) ) C_ ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( # ` ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) )
343 31 309 342 syl2anc 
 |-  ( ph -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( # ` ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) )
344 hashbnd 
 |-  ( ( ( H " ( NN0 ^m ( 0 ... A ) ) ) e. _V /\ ( # ` ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) e. NN0 /\ ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( # ` ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) ) -> ( H " ( NN0 ^m ( 0 ... A ) ) ) e. Fin )
345 310 341 343 344 syl3anc 
 |-  ( ph -> ( H " ( NN0 ^m ( 0 ... A ) ) ) e. Fin )
346 hashcl 
 |-  ( ( H " ( NN0 ^m ( 0 ... A ) ) ) e. Fin -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) e. NN0 )
347 345 346 syl 
 |-  ( ph -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) e. NN0 )
348 347 nn0red 
 |-  ( ph -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) e. RR )
349 341 nn0red 
 |-  ( ph -> ( # ` ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) e. RR )
350 115 154 nn0expcld 
 |-  ( ph -> ( N ^ B ) e. NN0 )
351 350 nn0red 
 |-  ( ph -> ( N ^ B ) e. RR )
352 172 nn0red 
 |-  ( ph -> J e. RR )
353 324 352 eqeltrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( J .^ X ) ) e. RR )
354 327 353 eqeltrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) ) e. RR )
355 312 354 eqeltrd 
 |-  ( ph -> ( ( deg1 ` K ) ` S ) e. RR )
356 107 nnred 
 |-  ( P e. Prime -> P e. RR )
357 4 356 syl 
 |-  ( ph -> P e. RR )
358 357 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> P e. RR )
359 358 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> P e. RR )
360 359 102 reexpcld 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( P ^ r ) e. RR )
361 120 357 114 redivcld 
 |-  ( ph -> ( N / P ) e. RR )
362 361 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> ( N / P ) e. RR )
363 362 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( N / P ) e. RR )
364 363 104 reexpcld 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( N / P ) ^ o ) e. RR )
365 360 364 remulcld 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) e. RR )
366 357 154 reexpcld 
 |-  ( ph -> ( P ^ B ) e. RR )
367 366 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> ( P ^ B ) e. RR )
368 361 154 reexpcld 
 |-  ( ph -> ( ( N / P ) ^ B ) e. RR )
369 368 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> ( ( N / P ) ^ B ) e. RR )
370 367 369 remulcld 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> ( ( P ^ B ) x. ( ( N / P ) ^ B ) ) e. RR )
371 370 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( P ^ B ) x. ( ( N / P ) ^ B ) ) e. RR )
372 120 154 reexpcld 
 |-  ( ph -> ( N ^ B ) e. RR )
373 372 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> ( N ^ B ) e. RR )
374 373 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( N ^ B ) e. RR )
375 367 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( P ^ B ) e. RR )
376 369 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( N / P ) ^ B ) e. RR )
377 0red 
 |-  ( ph -> 0 e. RR )
378 1red 
 |-  ( ph -> 1 e. RR )
379 0le1 
 |-  0 <_ 1
380 379 a1i 
 |-  ( ph -> 0 <_ 1 )
381 prmgt1 
 |-  ( P e. Prime -> 1 < P )
382 4 381 syl 
 |-  ( ph -> 1 < P )
383 378 357 382 ltled 
 |-  ( ph -> 1 <_ P )
384 377 378 357 380 383 letrd 
 |-  ( ph -> 0 <_ P )
385 384 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> 0 <_ P )
386 385 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> 0 <_ P )
387 359 102 386 expge0d 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> 0 <_ ( P ^ r ) )
388 123 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> 0 <_ ( N / P ) )
389 388 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> 0 <_ ( N / P ) )
390 363 104 389 expge0d 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> 0 <_ ( ( N / P ) ^ o ) )
391 108 nnge1d 
 |-  ( ph -> 1 <_ P )
392 391 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> 1 <_ P )
393 392 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> 1 <_ P )
394 elfzuz3 
 |-  ( r e. ( 0 ... B ) -> B e. ( ZZ>= ` r ) )
395 394 adantl 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> B e. ( ZZ>= ` r ) )
396 395 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> B e. ( ZZ>= ` r ) )
397 359 393 396 leexp2ad 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( P ^ r ) <_ ( P ^ B ) )
398 357 recnd 
 |-  ( ph -> P e. CC )
399 398 mullidd 
 |-  ( ph -> ( 1 x. P ) = P )
400 108 nnzd 
 |-  ( ph -> P e. ZZ )
401 dvdsle 
 |-  ( ( P e. ZZ /\ N e. NN ) -> ( P || N -> P <_ N ) )
402 400 6 401 syl2anc 
 |-  ( ph -> ( P || N -> P <_ N ) )
403 7 402 mpd 
 |-  ( ph -> P <_ N )
404 399 403 eqbrtrd 
 |-  ( ph -> ( 1 x. P ) <_ N )
405 378 120 121 lemuldivd 
 |-  ( ph -> ( ( 1 x. P ) <_ N <-> 1 <_ ( N / P ) ) )
406 404 405 mpbid 
 |-  ( ph -> 1 <_ ( N / P ) )
407 406 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> 1 <_ ( N / P ) )
408 407 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> 1 <_ ( N / P ) )
409 elfzuz3 
 |-  ( o e. ( 0 ... B ) -> B e. ( ZZ>= ` o ) )
410 409 adantl 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> B e. ( ZZ>= ` o ) )
411 363 408 410 leexp2ad 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( N / P ) ^ o ) <_ ( ( N / P ) ^ B ) )
412 360 375 364 376 387 390 397 411 lemul12ad 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) <_ ( ( P ^ B ) x. ( ( N / P ) ^ B ) ) )
413 120 recnd 
 |-  ( ph -> N e. CC )
414 413 398 114 divcan2d 
 |-  ( ph -> ( P x. ( N / P ) ) = N )
415 414 eqcomd 
 |-  ( ph -> N = ( P x. ( N / P ) ) )
416 415 adantr 
 |-  ( ( ph /\ r e. ( 0 ... B ) ) -> N = ( P x. ( N / P ) ) )
417 416 adantr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> N = ( P x. ( N / P ) ) )
418 417 oveq1d 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( N ^ B ) = ( ( P x. ( N / P ) ) ^ B ) )
419 359 recnd 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> P e. CC )
420 363 recnd 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( N / P ) e. CC )
421 154 ad2antrr 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> B e. NN0 )
422 419 420 421 mulexpd 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( P x. ( N / P ) ) ^ B ) = ( ( P ^ B ) x. ( ( N / P ) ^ B ) ) )
423 418 422 eqtr2d 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( P ^ B ) x. ( ( N / P ) ^ B ) ) = ( N ^ B ) )
424 374 leidd 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( N ^ B ) <_ ( N ^ B ) )
425 423 424 eqbrtrd 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( P ^ B ) x. ( ( N / P ) ^ B ) ) <_ ( N ^ B ) )
426 365 371 374 412 425 letrd 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( ( P ^ r ) x. ( ( N / P ) ^ o ) ) <_ ( N ^ B ) )
427 106 426 eqbrtrd 
 |-  ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) -> ( r E o ) <_ ( N ^ B ) )
428 427 adantr 
 |-  ( ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) -> ( r E o ) <_ ( N ^ B ) )
429 92 428 eqbrtrd 
 |-  ( ( ( ( ph /\ r e. ( 0 ... B ) ) /\ o e. ( 0 ... B ) ) /\ J = ( r E o ) ) -> J <_ ( N ^ B ) )
430 429 171 r19.29vva 
 |-  ( ph -> J <_ ( N ^ B ) )
431 324 430 eqbrtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( J .^ X ) ) <_ ( N ^ B ) )
432 327 431 eqbrtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( J .^ X ) ( -g ` ( Poly1 ` K ) ) ( I .^ X ) ) ) <_ ( N ^ B ) )
433 312 432 eqbrtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` S ) <_ ( N ^ B ) )
434 349 355 351 337 433 letrd 
 |-  ( ph -> ( # ` ( `' ( ( eval1 ` K ) ` S ) " { ( 0g ` K ) } ) ) <_ ( N ^ B ) )
435 348 349 351 343 434 letrd 
 |-  ( ph -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) )