Metamath Proof Explorer

Theorem aks6d1c6lem3

Description: Claim 6 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf TODO, eliminate hypothesis. (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 ) }
aks6d1c6lem3.1 
|- J = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) )
aks6d1c6lem3.2 
|- ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( # ` ( J " ( NN0 X. NN0 ) ) ) )
Assertion aks6d1c6lem3 
|- ( ph -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) )

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 aks6d1c6lem3.1 
 |-  J = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) )
21 aks6d1c6lem3.2 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( # ` ( J " ( NN0 X. NN0 ) ) ) )
22 eqid 
 |-  ( Z/nZ ` R ) = ( Z/nZ ` R )
23 6 4 7 5 8 12 13 22 hashscontpowcl 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )
24 18 23 eqeltrid 
 |-  ( ph -> D e. NN0 )
25 24 nn0zd 
 |-  ( ph -> D e. ZZ )
26 25 zcnd 
 |-  ( ph -> D e. CC )
27 1cnd 
 |-  ( ph -> 1 e. CC )
28 11 nn0cnd 
 |-  ( ph -> A e. CC )
29 26 27 28 nppcan3d 
 |-  ( ph -> ( ( D - 1 ) + ( A + 1 ) ) = ( D + A ) )
30 29 eqcomd 
 |-  ( ph -> ( D + A ) = ( ( D - 1 ) + ( A + 1 ) ) )
31 hashfz0 
 |-  ( A e. NN0 -> ( # ` ( 0 ... A ) ) = ( A + 1 ) )
32 11 31 syl 
 |-  ( ph -> ( # ` ( 0 ... A ) ) = ( A + 1 ) )
33 32 eqcomd 
 |-  ( ph -> ( A + 1 ) = ( # ` ( 0 ... A ) ) )
34 33 oveq2d 
 |-  ( ph -> ( ( D - 1 ) + ( A + 1 ) ) = ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) )
35 30 34 eqtrd 
 |-  ( ph -> ( D + A ) = ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) )
36 1zzd 
 |-  ( ph -> 1 e. ZZ )
37 25 36 zsubcld 
 |-  ( ph -> ( D - 1 ) e. ZZ )
38 0p1e1 
 |-  ( 0 + 1 ) = 1
39 38 a1i 
 |-  ( ph -> ( 0 + 1 ) = 1 )
40 fvexd 
 |-  ( ph -> ( ZRHom ` ( Z/nZ ` R ) ) e. _V )
41 13 40 eqeltrid 
 |-  ( ph -> L e. _V )
42 41 imaexd 
 |-  ( ph -> ( L " ( E " ( NN0 X. NN0 ) ) ) e. _V )
43 11 ne0d 
 |-  ( ph -> NN0 =/= (/) )
44 43 43 jca 
 |-  ( ph -> ( NN0 =/= (/) /\ NN0 =/= (/) ) )
45 xpnz 
 |-  ( ( NN0 =/= (/) /\ NN0 =/= (/) ) <-> ( NN0 X. NN0 ) =/= (/) )
46 44 45 sylib 
 |-  ( ph -> ( NN0 X. NN0 ) =/= (/) )
47 ovexd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. NN0 ) -> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) e. _V )
48 47 ralrimiva 
 |-  ( ( ph /\ k e. NN0 ) -> A. l e. NN0 ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) e. _V )
49 48 ralrimiva 
 |-  ( ph -> A. k e. NN0 A. l e. NN0 ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) e. _V )
50 12 fnmpo 
 |-  ( A. k e. NN0 A. l e. NN0 ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) e. _V -> E Fn ( NN0 X. NN0 ) )
51 49 50 syl 
 |-  ( ph -> E Fn ( NN0 X. NN0 ) )
52 ssidd 
 |-  ( ph -> ( NN0 X. NN0 ) C_ ( NN0 X. NN0 ) )
53 fnimaeq0 
 |-  ( ( E Fn ( NN0 X. NN0 ) /\ ( NN0 X. NN0 ) C_ ( NN0 X. NN0 ) ) -> ( ( E " ( NN0 X. NN0 ) ) = (/) <-> ( NN0 X. NN0 ) = (/) ) )
54 51 52 53 syl2anc 
 |-  ( ph -> ( ( E " ( NN0 X. NN0 ) ) = (/) <-> ( NN0 X. NN0 ) = (/) ) )
55 54 necon3bid 
 |-  ( ph -> ( ( E " ( NN0 X. NN0 ) ) =/= (/) <-> ( NN0 X. NN0 ) =/= (/) ) )
56 46 55 mpbird 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) =/= (/) )
57 5 nnnn0d 
 |-  ( ph -> R e. NN0 )
58 22 zncrng 
 |-  ( R e. NN0 -> ( Z/nZ ` R ) e. CRing )
59 57 58 syl 
 |-  ( ph -> ( Z/nZ ` R ) e. CRing )
60 crngring 
 |-  ( ( Z/nZ ` R ) e. CRing -> ( Z/nZ ` R ) e. Ring )
61 13 zrhrhm 
 |-  ( ( Z/nZ ` R ) e. Ring -> L e. ( ZZring RingHom ( Z/nZ ` R ) ) )
62 zringbas 
 |-  ZZ = ( Base ` ZZring )
63 eqid 
 |-  ( Base ` ( Z/nZ ` R ) ) = ( Base ` ( Z/nZ ` R ) )
64 62 63 rhmf 
 |-  ( L e. ( ZZring RingHom ( Z/nZ ` R ) ) -> L : ZZ --> ( Base ` ( Z/nZ ` R ) ) )
65 59 60 61 64 4syl 
 |-  ( ph -> L : ZZ --> ( Base ` ( Z/nZ ` R ) ) )
66 65 ffnd 
 |-  ( ph -> L Fn ZZ )
67 12 a1i 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) )
68 simprl 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) /\ ( k = x /\ l = y ) ) -> k = x )
69 68 oveq2d 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) /\ ( k = x /\ l = y ) ) -> ( P ^ k ) = ( P ^ x ) )
70 simprr 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) /\ ( k = x /\ l = y ) ) -> l = y )
71 70 oveq2d 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) /\ ( k = x /\ l = y ) ) -> ( ( N / P ) ^ l ) = ( ( N / P ) ^ y ) )
72 69 71 oveq12d 
 |-  ( ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) /\ ( k = x /\ l = y ) ) -> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) = ( ( P ^ x ) x. ( ( N / P ) ^ y ) ) )
73 simplr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> x e. NN0 )
74 simpr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> y e. NN0 )
75 ovexd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> ( ( P ^ x ) x. ( ( N / P ) ^ y ) ) e. _V )
76 67 72 73 74 75 ovmpod 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> ( x E y ) = ( ( P ^ x ) x. ( ( N / P ) ^ y ) ) )
77 4 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> P e. Prime )
78 prmnn 
 |-  ( P e. Prime -> P e. NN )
79 77 78 syl 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> P e. NN )
80 79 nnzd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> P e. ZZ )
81 80 73 zexpcld 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> ( P ^ x ) e. ZZ )
82 7 ad2antrr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> P || N )
83 79 nnne0d 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> P =/= 0 )
84 6 nnzd 
 |-  ( ph -> N e. ZZ )
85 84 adantr 
 |-  ( ( ph /\ x e. NN0 ) -> N e. ZZ )
86 85 adantr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> N e. ZZ )
87 dvdsval2 
 |-  ( ( P e. ZZ /\ P =/= 0 /\ N e. ZZ ) -> ( P || N <-> ( N / P ) e. ZZ ) )
88 80 83 86 87 syl3anc 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> ( P || N <-> ( N / P ) e. ZZ ) )
89 82 88 mpbid 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> ( N / P ) e. ZZ )
90 89 74 zexpcld 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> ( ( N / P ) ^ y ) e. ZZ )
91 81 90 zmulcld 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> ( ( P ^ x ) x. ( ( N / P ) ^ y ) ) e. ZZ )
92 76 91 eqeltrd 
 |-  ( ( ( ph /\ x e. NN0 ) /\ y e. NN0 ) -> ( x E y ) e. ZZ )
93 92 ralrimiva 
 |-  ( ( ph /\ x e. NN0 ) -> A. y e. NN0 ( x E y ) e. ZZ )
94 93 ralrimiva 
 |-  ( ph -> A. x e. NN0 A. y e. NN0 ( x E y ) e. ZZ )
95 51 94 jca 
 |-  ( ph -> ( E Fn ( NN0 X. NN0 ) /\ A. x e. NN0 A. y e. NN0 ( x E y ) e. ZZ ) )
96 ffnov 
 |-  ( E : ( NN0 X. NN0 ) --> ZZ <-> ( E Fn ( NN0 X. NN0 ) /\ A. x e. NN0 A. y e. NN0 ( x E y ) e. ZZ ) )
97 95 96 sylibr 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> ZZ )
98 frn 
 |-  ( E : ( NN0 X. NN0 ) --> ZZ -> ran E C_ ZZ )
99 97 98 syl 
 |-  ( ph -> ran E C_ ZZ )
100 fnima 
 |-  ( E Fn ( NN0 X. NN0 ) -> ( E " ( NN0 X. NN0 ) ) = ran E )
101 51 100 syl 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) = ran E )
102 101 sseq1d 
 |-  ( ph -> ( ( E " ( NN0 X. NN0 ) ) C_ ZZ <-> ran E C_ ZZ ) )
103 99 102 mpbird 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) C_ ZZ )
104 fnimaeq0 
 |-  ( ( L Fn ZZ /\ ( E " ( NN0 X. NN0 ) ) C_ ZZ ) -> ( ( L " ( E " ( NN0 X. NN0 ) ) ) = (/) <-> ( E " ( NN0 X. NN0 ) ) = (/) ) )
105 66 103 104 syl2anc 
 |-  ( ph -> ( ( L " ( E " ( NN0 X. NN0 ) ) ) = (/) <-> ( E " ( NN0 X. NN0 ) ) = (/) ) )
106 105 necon3bid 
 |-  ( ph -> ( ( L " ( E " ( NN0 X. NN0 ) ) ) =/= (/) <-> ( E " ( NN0 X. NN0 ) ) =/= (/) ) )
107 56 106 mpbird 
 |-  ( ph -> ( L " ( E " ( NN0 X. NN0 ) ) ) =/= (/) )
108 hashge1 
 |-  ( ( ( L " ( E " ( NN0 X. NN0 ) ) ) e. _V /\ ( L " ( E " ( NN0 X. NN0 ) ) ) =/= (/) ) -> 1 <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
109 18 eqcomi 
 |-  ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) = D
110 109 a1i 
 |-  ( ( ( L " ( E " ( NN0 X. NN0 ) ) ) e. _V /\ ( L " ( E " ( NN0 X. NN0 ) ) ) =/= (/) ) -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) = D )
111 108 110 breqtrd 
 |-  ( ( ( L " ( E " ( NN0 X. NN0 ) ) ) e. _V /\ ( L " ( E " ( NN0 X. NN0 ) ) ) =/= (/) ) -> 1 <_ D )
112 42 107 111 syl2anc 
 |-  ( ph -> 1 <_ D )
113 39 112 eqbrtrd 
 |-  ( ph -> ( 0 + 1 ) <_ D )
114 0red 
 |-  ( ph -> 0 e. RR )
115 1red 
 |-  ( ph -> 1 e. RR )
116 24 nn0red 
 |-  ( ph -> D e. RR )
117 leaddsub 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ D e. RR ) -> ( ( 0 + 1 ) <_ D <-> 0 <_ ( D - 1 ) ) )
118 114 115 116 117 syl3anc 
 |-  ( ph -> ( ( 0 + 1 ) <_ D <-> 0 <_ ( D - 1 ) ) )
119 113 118 mpbid 
 |-  ( ph -> 0 <_ ( D - 1 ) )
120 37 119 jca 
 |-  ( ph -> ( ( D - 1 ) e. ZZ /\ 0 <_ ( D - 1 ) ) )
121 elnn0z 
 |-  ( ( D - 1 ) e. NN0 <-> ( ( D - 1 ) e. ZZ /\ 0 <_ ( D - 1 ) ) )
122 120 121 sylibr 
 |-  ( ph -> ( D - 1 ) e. NN0 )
123 fzfid 
 |-  ( ph -> ( 0 ... A ) e. Fin )
124 hashcl 
 |-  ( ( 0 ... A ) e. Fin -> ( # ` ( 0 ... A ) ) e. NN0 )
125 123 124 syl 
 |-  ( ph -> ( # ` ( 0 ... A ) ) e. NN0 )
126 122 125 nn0addcld 
 |-  ( ph -> ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) e. NN0 )
127 35 126 eqeltrd 
 |-  ( ph -> ( D + A ) e. NN0 )
128 bccl 
 |-  ( ( ( D + A ) e. NN0 /\ ( D - 1 ) e. ZZ ) -> ( ( D + A ) _C ( D - 1 ) ) e. NN0 )
129 127 37 128 syl2anc 
 |-  ( ph -> ( ( D + A ) _C ( D - 1 ) ) e. NN0 )
130 129 nn0red 
 |-  ( ph -> ( ( D + A ) _C ( D - 1 ) ) e. RR )
131 130 rexrd 
 |-  ( ph -> ( ( D + A ) _C ( D - 1 ) ) e. RR* )
132 ovexd 
 |-  ( ph -> ( NN0 ^m ( 0 ... A ) ) e. _V )
133 132 mptexd 
 |-  ( ph -> ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) ) e. _V )
134 17 133 eqeltrid 
 |-  ( ph -> H e. _V )
135 134 imaexd 
 |-  ( ph -> ( H " ( NN0 ^m ( 0 ... A ) ) ) e. _V )
136 simprl 
 |-  ( ( ph /\ ( w e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( w ` t ) <_ ( D - 1 ) ) ) -> w e. ( NN0 ^m ( 0 ... A ) ) )
137 136 ex 
 |-  ( ph -> ( ( w e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( w ` t ) <_ ( D - 1 ) ) -> w e. ( NN0 ^m ( 0 ... A ) ) ) )
138 simpl 
 |-  ( ( s = w /\ t e. ( 0 ... A ) ) -> s = w )
139 138 fveq1d 
 |-  ( ( s = w /\ t e. ( 0 ... A ) ) -> ( s ` t ) = ( w ` t ) )
140 139 sumeq2dv 
 |-  ( s = w -> sum_ t e. ( 0 ... A ) ( s ` t ) = sum_ t e. ( 0 ... A ) ( w ` t ) )
141 140 breq1d 
 |-  ( s = w -> ( sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) <-> sum_ t e. ( 0 ... A ) ( w ` t ) <_ ( D - 1 ) ) )
142 141 elrab 
 |-  ( w e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } <-> ( w e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( w ` t ) <_ ( D - 1 ) ) )
143 142 a1i 
 |-  ( ph -> ( w e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } <-> ( w e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( w ` t ) <_ ( D - 1 ) ) ) )
144 143 biimpd 
 |-  ( ph -> ( w e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } -> ( w e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( w ` t ) <_ ( D - 1 ) ) ) )
145 144 imim1d 
 |-  ( ph -> ( ( ( w e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( w ` t ) <_ ( D - 1 ) ) -> w e. ( NN0 ^m ( 0 ... A ) ) ) -> ( w e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } -> w e. ( NN0 ^m ( 0 ... A ) ) ) ) )
146 137 145 mpd 
 |-  ( ph -> ( w e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } -> w e. ( NN0 ^m ( 0 ... A ) ) ) )
147 146 ssrdv 
 |-  ( ph -> { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } C_ ( NN0 ^m ( 0 ... A ) ) )
148 19 a1i 
 |-  ( ph -> S = { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } )
149 148 sseq1d 
 |-  ( ph -> ( S C_ ( NN0 ^m ( 0 ... A ) ) <-> { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } C_ ( NN0 ^m ( 0 ... A ) ) ) )
150 147 149 mpbird 
 |-  ( ph -> S C_ ( NN0 ^m ( 0 ... A ) ) )
151 imass2 
 |-  ( S C_ ( NN0 ^m ( 0 ... A ) ) -> ( H " S ) C_ ( H " ( NN0 ^m ( 0 ... A ) ) ) )
152 150 151 syl 
 |-  ( ph -> ( H " S ) C_ ( H " ( NN0 ^m ( 0 ... A ) ) ) )
153 135 152 ssexd 
 |-  ( ph -> ( H " S ) e. _V )
154 hashxnn0 
 |-  ( ( H " S ) e. _V -> ( # ` ( H " S ) ) e. NN0* )
155 153 154 syl 
 |-  ( ph -> ( # ` ( H " S ) ) e. NN0* )
156 xnn0xr 
 |-  ( ( # ` ( H " S ) ) e. NN0* -> ( # ` ( H " S ) ) e. RR* )
157 155 156 syl 
 |-  ( ph -> ( # ` ( H " S ) ) e. RR* )
158 hashxnn0 
 |-  ( ( H " ( NN0 ^m ( 0 ... A ) ) ) e. _V -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) e. NN0* )
159 135 158 syl 
 |-  ( ph -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) e. NN0* )
160 xnn0xr 
 |-  ( ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) e. NN0* -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) e. RR* )
161 159 160 syl 
 |-  ( ph -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) e. RR* )
162 122 nn0cnd 
 |-  ( ph -> ( D - 1 ) e. CC )
163 125 nn0cnd 
 |-  ( ph -> ( # ` ( 0 ... A ) ) e. CC )
164 162 163 pncand 
 |-  ( ph -> ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) - ( # ` ( 0 ... A ) ) ) = ( D - 1 ) )
165 164 eqcomd 
 |-  ( ph -> ( D - 1 ) = ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) - ( # ` ( 0 ... A ) ) ) )
166 35 165 oveq12d 
 |-  ( ph -> ( ( D + A ) _C ( D - 1 ) ) = ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) _C ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) - ( # ` ( 0 ... A ) ) ) ) )
167 11 nn0ge0d 
 |-  ( ph -> 0 <_ A )
168 0zd 
 |-  ( ph -> 0 e. ZZ )
169 11 nn0zd 
 |-  ( ph -> A e. ZZ )
170 eluz 
 |-  ( ( 0 e. ZZ /\ A e. ZZ ) -> ( A e. ( ZZ>= ` 0 ) <-> 0 <_ A ) )
171 168 169 170 syl2anc 
 |-  ( ph -> ( A e. ( ZZ>= ` 0 ) <-> 0 <_ A ) )
172 167 171 mpbird 
 |-  ( ph -> A e. ( ZZ>= ` 0 ) )
173 fzn0 
 |-  ( ( 0 ... A ) =/= (/) <-> A e. ( ZZ>= ` 0 ) )
174 172 173 sylibr 
 |-  ( ph -> ( 0 ... A ) =/= (/) )
175 122 123 174 19 sticksstones23 
 |-  ( ph -> ( # ` S ) = ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) _C ( # ` ( 0 ... A ) ) ) )
176 125 nn0zd 
 |-  ( ph -> ( # ` ( 0 ... A ) ) e. ZZ )
177 bccmpl 
 |-  ( ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) e. NN0 /\ ( # ` ( 0 ... A ) ) e. ZZ ) -> ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) _C ( # ` ( 0 ... A ) ) ) = ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) _C ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) - ( # ` ( 0 ... A ) ) ) ) )
178 126 176 177 syl2anc 
 |-  ( ph -> ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) _C ( # ` ( 0 ... A ) ) ) = ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) _C ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) - ( # ` ( 0 ... A ) ) ) ) )
179 175 178 eqtrd 
 |-  ( ph -> ( # ` S ) = ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) _C ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) - ( # ` ( 0 ... A ) ) ) ) )
180 179 eqcomd 
 |-  ( ph -> ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) _C ( ( ( D - 1 ) + ( # ` ( 0 ... A ) ) ) - ( # ` ( 0 ... A ) ) ) ) = ( # ` S ) )
181 166 180 eqtrd 
 |-  ( ph -> ( ( D + A ) _C ( D - 1 ) ) = ( # ` S ) )
182 181 adantr 
 |-  ( ( ph /\ ( H |` S ) : S -1-1-> ( H " S ) ) -> ( ( D + A ) _C ( D - 1 ) ) = ( # ` S ) )
183 17 a1i 
 |-  ( ( ph /\ ( H |` S ) : S -1-1-> ( H " S ) ) -> H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) ) )
184 ovexd 
 |-  ( ( ph /\ ( H |` S ) : S -1-1-> ( H " S ) ) -> ( NN0 ^m ( 0 ... A ) ) e. _V )
185 184 mptexd 
 |-  ( ( ph /\ ( H |` S ) : S -1-1-> ( H " S ) ) -> ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) ) e. _V )
186 183 185 eqeltrd 
 |-  ( ( ph /\ ( H |` S ) : S -1-1-> ( H " S ) ) -> H e. _V )
187 186 resexd 
 |-  ( ( ph /\ ( H |` S ) : S -1-1-> ( H " S ) ) -> ( H |` S ) e. _V )
188 186 imaexd 
 |-  ( ( ph /\ ( H |` S ) : S -1-1-> ( H " S ) ) -> ( H " S ) e. _V )
189 simpr 
 |-  ( ( ph /\ ( H |` S ) : S -1-1-> ( H " S ) ) -> ( H |` S ) : S -1-1-> ( H " S ) )
190 hashf1dmcdm 
 |-  ( ( ( H |` S ) e. _V /\ ( H " S ) e. _V /\ ( H |` S ) : S -1-1-> ( H " S ) ) -> ( # ` S ) <_ ( # ` ( H " S ) ) )
191 187 188 189 190 syl3anc 
 |-  ( ( ph /\ ( H |` S ) : S -1-1-> ( H " S ) ) -> ( # ` S ) <_ ( # ` ( H " S ) ) )
192 182 191 eqbrtrd 
 |-  ( ( ph /\ ( H |` S ) : S -1-1-> ( H " S ) ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) )
193 17 a1i 
 |-  ( ( ph /\ j e. S ) -> H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) ) )
194 simpr 
 |-  ( ( ( ph /\ j e. S ) /\ h = j ) -> h = j )
195 194 fveq2d 
 |-  ( ( ( ph /\ j e. S ) /\ h = j ) -> ( G ` h ) = ( G ` j ) )
196 195 fveq2d 
 |-  ( ( ( ph /\ j e. S ) /\ h = j ) -> ( ( eval1 ` K ) ` ( G ` h ) ) = ( ( eval1 ` K ) ` ( G ` j ) ) )
197 196 fveq1d 
 |-  ( ( ( ph /\ j e. S ) /\ h = j ) -> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) = ( ( ( eval1 ` K ) ` ( G ` j ) ) ` M ) )
198 simp2 
 |-  ( ( ph /\ s e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) ) -> s e. ( NN0 ^m ( 0 ... A ) ) )
199 198 rabssdv 
 |-  ( ph -> { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } C_ ( NN0 ^m ( 0 ... A ) ) )
200 19 199 eqsstrid 
 |-  ( ph -> S C_ ( NN0 ^m ( 0 ... A ) ) )
201 200 sselda 
 |-  ( ( ph /\ j e. S ) -> j e. ( NN0 ^m ( 0 ... A ) ) )
202 fvexd 
 |-  ( ( ph /\ j e. S ) -> ( ( ( eval1 ` K ) ` ( G ` j ) ) ` M ) e. _V )
203 193 197 201 202 fvmptd 
 |-  ( ( ph /\ j e. S ) -> ( H ` j ) = ( ( ( eval1 ` K ) ` ( G ` j ) ) ` M ) )
204 eqid 
 |-  ( eval1 ` K ) = ( eval1 ` K )
205 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
206 eqid 
 |-  ( Base ` K ) = ( Base ` K )
207 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
208 3 fldcrngd 
 |-  ( ph -> K e. CRing )
209 208 adantr 
 |-  ( ( ph /\ j e. S ) -> K e. CRing )
210 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
211 210 crngmgp 
 |-  ( K e. CRing -> ( mulGrp ` K ) e. CMnd )
212 208 211 syl 
 |-  ( ph -> ( mulGrp ` K ) e. CMnd )
213 eqid 
 |-  ( .g ` ( mulGrp ` K ) ) = ( .g ` ( mulGrp ` K ) )
214 212 57 213 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 ) ) ) )
215 214 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 ) ) ) )
216 16 215 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 ) ) )
217 216 simp1d 
 |-  ( ph -> M e. ( Base ` ( mulGrp ` K ) ) )
218 210 206 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
219 218 eqcomi 
 |-  ( Base ` ( mulGrp ` K ) ) = ( Base ` K )
220 217 219 eleqtrdi 
 |-  ( ph -> M e. ( Base ` K ) )
221 220 adantr 
 |-  ( ( ph /\ j e. S ) -> M e. ( Base ` K ) )
222 eqid 
 |-  ( var1 ` K ) = ( var1 ` K )
223 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
224 3 4 2 11 9 222 223 10 aks6d1c5lem0 
 |-  ( ph -> G : ( NN0 ^m ( 0 ... A ) ) --> ( Base ` ( Poly1 ` K ) ) )
225 224 adantr 
 |-  ( ( ph /\ j e. S ) -> G : ( NN0 ^m ( 0 ... A ) ) --> ( Base ` ( Poly1 ` K ) ) )
226 225 201 ffvelcdmd 
 |-  ( ( ph /\ j e. S ) -> ( G ` j ) e. ( Base ` ( Poly1 ` K ) ) )
227 204 205 206 207 209 221 226 fveval1fvcl 
 |-  ( ( ph /\ j e. S ) -> ( ( ( eval1 ` K ) ` ( G ` j ) ) ` M ) e. ( Base ` K ) )
228 203 227 eqeltrd 
 |-  ( ( ph /\ j e. S ) -> ( H ` j ) e. ( Base ` K ) )
229 eqid 
 |-  ( j e. S |-> ( H ` j ) ) = ( j e. S |-> ( H ` j ) )
230 228 229 fmptd 
 |-  ( ph -> ( j e. S |-> ( H ` j ) ) : S --> ( Base ` K ) )
231 fvexd 
 |-  ( ( ph /\ h e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) e. _V )
232 231 17 fmptd 
 |-  ( ph -> H : ( NN0 ^m ( 0 ... A ) ) --> _V )
233 232 200 feqresmpt 
 |-  ( ph -> ( H |` S ) = ( j e. S |-> ( H ` j ) ) )
234 233 feq1d 
 |-  ( ph -> ( ( H |` S ) : S --> ( Base ` K ) <-> ( j e. S |-> ( H ` j ) ) : S --> ( Base ` K ) ) )
235 230 234 mpbird 
 |-  ( ph -> ( H |` S ) : S --> ( Base ` K ) )
236 ffrn 
 |-  ( ( H |` S ) : S --> ( Base ` K ) -> ( H |` S ) : S --> ran ( H |` S ) )
237 235 236 syl 
 |-  ( ph -> ( H |` S ) : S --> ran ( H |` S ) )
238 df-ima 
 |-  ( H " S ) = ran ( H |` S )
239 238 a1i 
 |-  ( ph -> ( H " S ) = ran ( H |` S ) )
240 239 feq3d 
 |-  ( ph -> ( ( H |` S ) : S --> ( H " S ) <-> ( H |` S ) : S --> ran ( H |` S ) ) )
241 237 240 mpbird 
 |-  ( ph -> ( H |` S ) : S --> ( H " S ) )
242 241 notnotd 
 |-  ( ph -> -. -. ( H |` S ) : S --> ( H " S ) )
243 242 a1d 
 |-  ( ph -> ( -. ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) -> -. -. ( H |` S ) : S --> ( H " S ) ) )
244 243 con4d 
 |-  ( ph -> ( -. ( H |` S ) : S --> ( H " S ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) )
245 df-an 
 |-  ( ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) <-> -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> -. -. u = v ) )
246 245 a1i 
 |-  ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) -> ( ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) <-> -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> -. -. u = v ) ) )
247 eqid 
 |-  ( deg1 ` K ) = ( deg1 ` K )
248 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
249 eqid 
 |-  ( 0g ` ( Poly1 ` K ) ) = ( 0g ` ( Poly1 ` K ) )
250 fldidom 
 |-  ( K e. Field -> K e. IDomn )
251 3 250 syl 
 |-  ( ph -> K e. IDomn )
252 251 ad4antr 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> K e. IDomn )
253 205 ply1crng 
 |-  ( K e. CRing -> ( Poly1 ` K ) e. CRing )
254 crngring 
 |-  ( ( Poly1 ` K ) e. CRing -> ( Poly1 ` K ) e. Ring )
255 ringgrp 
 |-  ( ( Poly1 ` K ) e. Ring -> ( Poly1 ` K ) e. Grp )
256 208 253 254 255 4syl 
 |-  ( ph -> ( Poly1 ` K ) e. Grp )
257 256 ad4antr 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( Poly1 ` K ) e. Grp )
258 3 4 2 11 9 222 223 10 aks6d1c5 
 |-  ( ph -> G : ( NN0 ^m ( 0 ... A ) ) -1-1-> ( Base ` ( Poly1 ` K ) ) )
259 258 ad4antr 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> G : ( NN0 ^m ( 0 ... A ) ) -1-1-> ( Base ` ( Poly1 ` K ) ) )
260 f1f 
 |-  ( G : ( NN0 ^m ( 0 ... A ) ) -1-1-> ( Base ` ( Poly1 ` K ) ) -> G : ( NN0 ^m ( 0 ... A ) ) --> ( Base ` ( Poly1 ` K ) ) )
261 259 260 syl 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> G : ( NN0 ^m ( 0 ... A ) ) --> ( Base ` ( Poly1 ` K ) ) )
262 19 eleq2i 
 |-  ( u e. S <-> u e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } )
263 simpl 
 |-  ( ( s = u /\ t e. ( 0 ... A ) ) -> s = u )
264 263 fveq1d 
 |-  ( ( s = u /\ t e. ( 0 ... A ) ) -> ( s ` t ) = ( u ` t ) )
265 264 sumeq2dv 
 |-  ( s = u -> sum_ t e. ( 0 ... A ) ( s ` t ) = sum_ t e. ( 0 ... A ) ( u ` t ) )
266 265 breq1d 
 |-  ( s = u -> ( sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) <-> sum_ t e. ( 0 ... A ) ( u ` t ) <_ ( D - 1 ) ) )
267 266 elrab 
 |-  ( u e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } <-> ( u e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( u ` t ) <_ ( D - 1 ) ) )
268 267 simplbi 
 |-  ( u e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } -> u e. ( NN0 ^m ( 0 ... A ) ) )
269 262 268 sylbi 
 |-  ( u e. S -> u e. ( NN0 ^m ( 0 ... A ) ) )
270 269 adantl 
 |-  ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) -> u e. ( NN0 ^m ( 0 ... A ) ) )
271 270 adantr 
 |-  ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) -> u e. ( NN0 ^m ( 0 ... A ) ) )
272 271 adantr 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> u e. ( NN0 ^m ( 0 ... A ) ) )
273 261 272 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( G ` u ) e. ( Base ` ( Poly1 ` K ) ) )
274 19 eleq2i 
 |-  ( v e. S <-> v e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } )
275 elrabi 
 |-  ( v e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } -> v e. ( NN0 ^m ( 0 ... A ) ) )
276 274 275 sylbi 
 |-  ( v e. S -> v e. ( NN0 ^m ( 0 ... A ) ) )
277 276 adantl 
 |-  ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) -> v e. ( NN0 ^m ( 0 ... A ) ) )
278 277 adantr 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> v e. ( NN0 ^m ( 0 ... A ) ) )
279 261 278 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( G ` v ) e. ( Base ` ( Poly1 ` K ) ) )
280 eqid 
 |-  ( -g ` ( Poly1 ` K ) ) = ( -g ` ( Poly1 ` K ) )
281 207 280 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 ) ) )
282 257 273 279 281 syl3anc 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) e. ( Base ` ( Poly1 ` K ) ) )
283 neqne 
 |-  ( -. u = v -> u =/= v )
284 283 adantl 
 |-  ( ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) -> u =/= v )
285 284 adantl 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> u =/= v )
286 272 278 jca 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( u e. ( NN0 ^m ( 0 ... A ) ) /\ v e. ( NN0 ^m ( 0 ... A ) ) ) )
287 f1fveq 
 |-  ( ( G : ( NN0 ^m ( 0 ... A ) ) -1-1-> ( Base ` ( Poly1 ` K ) ) /\ ( u e. ( NN0 ^m ( 0 ... A ) ) /\ v e. ( NN0 ^m ( 0 ... A ) ) ) ) -> ( ( G ` u ) = ( G ` v ) <-> u = v ) )
288 259 286 287 syl2anc 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( G ` u ) = ( G ` v ) <-> u = v ) )
289 288 bicomd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( u = v <-> ( G ` u ) = ( G ` v ) ) )
290 289 necon3bid 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( u =/= v <-> ( G ` u ) =/= ( G ` v ) ) )
291 290 biimpd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( u =/= v -> ( G ` u ) =/= ( G ` v ) ) )
292 285 291 mpd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( G ` u ) =/= ( G ` v ) )
293 207 249 280 grpsubeq0 
 |-  ( ( ( Poly1 ` K ) e. Grp /\ ( G ` u ) e. ( Base ` ( Poly1 ` K ) ) /\ ( G ` v ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) = ( 0g ` ( Poly1 ` K ) ) <-> ( G ` u ) = ( G ` v ) ) )
294 293 necon3bid 
 |-  ( ( ( Poly1 ` K ) e. Grp /\ ( G ` u ) e. ( Base ` ( Poly1 ` K ) ) /\ ( G ` v ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) =/= ( 0g ` ( Poly1 ` K ) ) <-> ( G ` u ) =/= ( G ` v ) ) )
295 257 273 279 294 syl3anc 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) =/= ( 0g ` ( Poly1 ` K ) ) <-> ( G ` u ) =/= ( G ` v ) ) )
296 292 295 mpbird 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) =/= ( 0g ` ( Poly1 ` K ) ) )
297 205 207 247 204 248 249 252 282 296 fta1g 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) <_ ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) )
298 247 205 207 deg1xrcl 
 |-  ( ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) e. ( Base ` ( Poly1 ` K ) ) -> ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. RR* )
299 282 298 syl 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. RR* )
300 116 ad4antr 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> D e. RR )
301 1red 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> 1 e. RR )
302 300 301 resubcld 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( D - 1 ) e. RR )
303 302 rexrd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( D - 1 ) e. RR* )
304 simp-4l 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ph )
305 fvexd 
 |-  ( ph -> ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. _V )
306 cnvexg 
 |-  ( ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. _V -> `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. _V )
307 305 306 syl 
 |-  ( ph -> `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. _V )
308 307 imaexd 
 |-  ( ph -> ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) e. _V )
309 hashxnn0 
 |-  ( ( `' ( ( 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. NN0* )
310 xnn0xr 
 |-  ( ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) e. NN0* -> ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) e. RR* )
311 304 308 309 310 4syl 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) e. RR* )
312 247 205 207 deg1xrcl 
 |-  ( ( G ` v ) e. ( Base ` ( Poly1 ` K ) ) -> ( ( deg1 ` K ) ` ( G ` v ) ) e. RR* )
313 279 312 syl 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( deg1 ` K ) ` ( G ` v ) ) e. RR* )
314 247 205 207 deg1xrcl 
 |-  ( ( G ` u ) e. ( Base ` ( Poly1 ` K ) ) -> ( ( deg1 ` K ) ` ( G ` u ) ) e. RR* )
315 273 314 syl 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( deg1 ` K ) ` ( G ` u ) ) e. RR* )
316 313 315 ifcld 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> if ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` u ) ) ) e. RR* )
317 252 idomringd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> K e. Ring )
318 205 247 317 207 280 273 279 deg1suble 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) <_ if ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` u ) ) ) )
319 id 
 |-  ( ( ( deg1 ` K ) ` ( G ` v ) ) = if ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` u ) ) ) -> ( ( deg1 ` K ) ` ( G ` v ) ) = if ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` u ) ) ) )
320 319 breq1d 
 |-  ( ( ( deg1 ` K ) ` ( G ` v ) ) = if ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` u ) ) ) -> ( ( ( deg1 ` K ) ` ( G ` v ) ) <_ ( D - 1 ) <-> if ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` u ) ) ) <_ ( D - 1 ) ) )
321 id 
 |-  ( ( ( deg1 ` K ) ` ( G ` u ) ) = if ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` u ) ) ) -> ( ( deg1 ` K ) ` ( G ` u ) ) = if ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` u ) ) ) )
322 321 breq1d 
 |-  ( ( ( deg1 ` K ) ` ( G ` u ) ) = if ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` u ) ) ) -> ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( D - 1 ) <-> if ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` u ) ) ) <_ ( D - 1 ) ) )
323 3 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> K e. Field )
324 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> P e. Prime )
325 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> R e. NN )
326 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> N e. NN )
327 7 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> P || N )
328 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> ( N gcd R ) = 1 )
329 9 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> A < P )
330 11 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> A e. NN0 )
331 14 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
332 15 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
333 16 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
334 simpllr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> v e. S )
335 334 276 syl 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> v e. ( NN0 ^m ( 0 ... A ) ) )
336 1 2 323 324 325 326 327 328 329 10 330 12 13 331 332 333 17 18 19 335 aks6d1c6lem1 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> ( ( deg1 ` K ) ` ( G ` v ) ) = sum_ t e. ( 0 ... A ) ( v ` t ) )
337 simpl 
 |-  ( ( s = v /\ t e. ( 0 ... A ) ) -> s = v )
338 337 fveq1d 
 |-  ( ( s = v /\ t e. ( 0 ... A ) ) -> ( s ` t ) = ( v ` t ) )
339 338 sumeq2dv 
 |-  ( s = v -> sum_ t e. ( 0 ... A ) ( s ` t ) = sum_ t e. ( 0 ... A ) ( v ` t ) )
340 339 breq1d 
 |-  ( s = v -> ( sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) <-> sum_ t e. ( 0 ... A ) ( v ` t ) <_ ( D - 1 ) ) )
341 340 elrab 
 |-  ( v e. { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) } <-> ( v e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( v ` t ) <_ ( D - 1 ) ) )
342 274 341 bitri 
 |-  ( v e. S <-> ( v e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( v ` t ) <_ ( D - 1 ) ) )
343 334 342 sylib 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> ( v e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( v ` t ) <_ ( D - 1 ) ) )
344 343 simprd 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> sum_ t e. ( 0 ... A ) ( v ` t ) <_ ( D - 1 ) )
345 336 344 eqbrtrd 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> ( ( deg1 ` K ) ` ( G ` v ) ) <_ ( D - 1 ) )
346 3 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> K e. Field )
347 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> P e. Prime )
348 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> R e. NN )
349 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> N e. NN )
350 7 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> P || N )
351 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> ( N gcd R ) = 1 )
352 9 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> A < P )
353 11 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> A e. NN0 )
354 14 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
355 15 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
356 16 ad5antr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
357 272 adantr 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> u e. ( NN0 ^m ( 0 ... A ) ) )
358 1 2 346 347 348 349 350 351 352 10 353 12 13 354 355 356 17 18 19 357 aks6d1c6lem1 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> ( ( deg1 ` K ) ` ( G ` u ) ) = sum_ t e. ( 0 ... A ) ( u ` t ) )
359 simp-4r 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> u e. S )
360 262 267 bitri 
 |-  ( u e. S <-> ( u e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( u ` t ) <_ ( D - 1 ) ) )
361 359 360 sylib 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> ( u e. ( NN0 ^m ( 0 ... A ) ) /\ sum_ t e. ( 0 ... A ) ( u ` t ) <_ ( D - 1 ) ) )
362 361 simprd 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> sum_ t e. ( 0 ... A ) ( u ` t ) <_ ( D - 1 ) )
363 358 362 eqbrtrd 
 |-  ( ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) /\ -. ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) ) -> ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( D - 1 ) )
364 320 322 345 363 ifbothda 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> if ( ( ( deg1 ` K ) ` ( G ` u ) ) <_ ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` v ) ) , ( ( deg1 ` K ) ` ( G ` u ) ) ) <_ ( D - 1 ) )
365 299 316 303 318 364 xrletrd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) <_ ( D - 1 ) )
366 300 rexrd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> D e. RR* )
367 300 ltm1d 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( D - 1 ) < D )
368 simpllr 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> u e. S )
369 simplr 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> v e. S )
370 304 368 369 jca31 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( ph /\ u e. S ) /\ v e. S ) )
371 simpr 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) )
372 370 371 jca 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) )
373 3 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> K e. Field )
374 4 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> P e. Prime )
375 5 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> R e. NN )
376 6 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> N e. NN )
377 7 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> P || N )
378 8 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( N gcd R ) = 1 )
379 9 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> A < P )
380 11 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> A e. NN0 )
381 14 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
382 15 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
383 16 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
384 simpllr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> u e. S )
385 simplr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> v e. S )
386 simprl 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) )
387 284 adantl 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> u =/= v )
388 21 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( # ` ( J " ( NN0 X. NN0 ) ) ) )
389 1 2 373 374 375 376 377 378 379 10 380 12 13 381 382 383 17 18 19 384 385 386 387 20 388 aks6d1c6lem2 
 |-  ( ( ( ( ph /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> D <_ ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) )
390 372 389 syl 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> D <_ ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) )
391 303 366 311 367 390 xrltletrd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( D - 1 ) < ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) )
392 299 303 311 365 391 xrlelttrd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) < ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) )
393 247 205 249 207 deg1nn0clb 
 |-  ( ( K e. Ring /\ ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) =/= ( 0g ` ( Poly1 ` K ) ) <-> ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. NN0 ) )
394 317 282 393 syl2anc 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) =/= ( 0g ` ( Poly1 ` K ) ) <-> ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. NN0 ) )
395 296 394 mpbid 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. NN0 )
396 395 nn0red 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. RR )
397 396 rexrd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. RR* )
398 fvexd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. _V )
399 398 306 syl 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. _V )
400 399 imaexd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) e. _V )
401 400 309 syl 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) e. NN0* )
402 401 310 syl 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) e. RR* )
403 xrltnle 
 |-  ( ( ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) e. RR* /\ ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) e. RR* ) -> ( ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) < ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) <-> -. ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) <_ ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) ) )
404 397 402 403 syl2anc 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) < ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) <-> -. ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) <_ ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) ) )
405 392 404 mpbid 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> -. ( # ` ( `' ( ( eval1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) " { ( 0g ` K ) } ) ) <_ ( ( deg1 ` K ) ` ( ( G ` u ) ( -g ` ( Poly1 ` K ) ) ( G ` v ) ) ) )
406 297 405 pm2.21dd 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) )
407 406 ex 
 |-  ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) -> ( ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) /\ -. u = v ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) )
408 246 407 sylbird 
 |-  ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) -> ( -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> -. -. u = v ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) )
409 biidd 
 |-  ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> ( u = v <-> u = v ) )
410 409 necon3abid 
 |-  ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> ( u =/= v <-> -. u = v ) )
411 410 necon1bbid 
 |-  ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> ( -. -. u = v <-> u = v ) )
412 411 pm5.74i 
 |-  ( ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> -. -. u = v ) <-> ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> u = v ) )
413 412 notbii 
 |-  ( -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> -. -. u = v ) <-> -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> u = v ) )
414 413 a1i 
 |-  ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) -> ( -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> -. -. u = v ) <-> -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> u = v ) ) )
415 414 imbi1d 
 |-  ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) -> ( ( -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> -. -. u = v ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) <-> ( -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> u = v ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) ) )
416 408 415 mpbid 
 |-  ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) -> ( -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> u = v ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) )
417 416 imp 
 |-  ( ( ( ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) /\ u e. S ) /\ v e. S ) /\ -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> u = v ) ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) )
418 fveqeq2 
 |-  ( x = u -> ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) <-> ( ( H |` S ) ` u ) = ( ( H |` S ) ` y ) ) )
419 equequ1 
 |-  ( x = u -> ( x = y <-> u = y ) )
420 418 419 imbi12d 
 |-  ( x = u -> ( ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) <-> ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` y ) -> u = y ) ) )
421 420 notbid 
 |-  ( x = u -> ( -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) <-> -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` y ) -> u = y ) ) )
422 fveq2 
 |-  ( y = v -> ( ( H |` S ) ` y ) = ( ( H |` S ) ` v ) )
423 422 eqeq2d 
 |-  ( y = v -> ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` y ) <-> ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) ) )
424 equequ2 
 |-  ( y = v -> ( u = y <-> u = v ) )
425 423 424 imbi12d 
 |-  ( y = v -> ( ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` y ) -> u = y ) <-> ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> u = v ) ) )
426 425 notbid 
 |-  ( y = v -> ( -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` y ) -> u = y ) <-> -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> u = v ) ) )
427 421 426 cbvrex2vw 
 |-  ( E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) <-> E. u e. S E. v e. S -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> u = v ) )
428 427 biimpi 
 |-  ( E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) -> E. u e. S E. v e. S -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> u = v ) )
429 428 adantl 
 |-  ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) -> E. u e. S E. v e. S -. ( ( ( H |` S ) ` u ) = ( ( H |` S ) ` v ) -> u = v ) )
430 417 429 r19.29vva 
 |-  ( ( ph /\ E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) )
431 430 ex 
 |-  ( ph -> ( E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) )
432 rexnal2 
 |-  ( E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) <-> -. A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) )
433 432 a1i 
 |-  ( ph -> ( E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) <-> -. A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) )
434 433 imbi1d 
 |-  ( ph -> ( ( E. x e. S E. y e. S -. ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) <-> ( -. A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) ) )
435 431 434 mpbid 
 |-  ( ph -> ( -. A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) )
436 244 435 jaod 
 |-  ( ph -> ( ( -. ( H |` S ) : S --> ( H " S ) \/ -. A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) )
437 ianor 
 |-  ( -. ( ( H |` S ) : S --> ( H " S ) /\ A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) <-> ( -. ( H |` S ) : S --> ( H " S ) \/ -. A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) )
438 437 a1i 
 |-  ( ph -> ( -. ( ( H |` S ) : S --> ( H " S ) /\ A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) <-> ( -. ( H |` S ) : S --> ( H " S ) \/ -. A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) ) )
439 438 biimpd 
 |-  ( ph -> ( -. ( ( H |` S ) : S --> ( H " S ) /\ A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) -> ( -. ( H |` S ) : S --> ( H " S ) \/ -. A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) ) )
440 439 imim1d 
 |-  ( ph -> ( ( ( -. ( H |` S ) : S --> ( H " S ) \/ -. A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) -> ( -. ( ( H |` S ) : S --> ( H " S ) /\ A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) ) )
441 436 440 mpd 
 |-  ( ph -> ( -. ( ( H |` S ) : S --> ( H " S ) /\ A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) )
442 dff13 
 |-  ( ( H |` S ) : S -1-1-> ( H " S ) <-> ( ( H |` S ) : S --> ( H " S ) /\ A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) )
443 442 a1i 
 |-  ( ph -> ( ( H |` S ) : S -1-1-> ( H " S ) <-> ( ( H |` S ) : S --> ( H " S ) /\ A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) ) )
444 443 notbid 
 |-  ( ph -> ( -. ( H |` S ) : S -1-1-> ( H " S ) <-> -. ( ( H |` S ) : S --> ( H " S ) /\ A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) ) )
445 444 biimpd 
 |-  ( ph -> ( -. ( H |` S ) : S -1-1-> ( H " S ) -> -. ( ( H |` S ) : S --> ( H " S ) /\ A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) ) )
446 445 imim1d 
 |-  ( ph -> ( ( -. ( ( H |` S ) : S --> ( H " S ) /\ A. x e. S A. y e. S ( ( ( H |` S ) ` x ) = ( ( H |` S ) ` y ) -> x = y ) ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) -> ( -. ( H |` S ) : S -1-1-> ( H " S ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) ) )
447 441 446 mpd 
 |-  ( ph -> ( -. ( H |` S ) : S -1-1-> ( H " S ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) ) )
448 447 imp 
 |-  ( ( ph /\ -. ( H |` S ) : S -1-1-> ( H " S ) ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) )
449 192 448 pm2.61dan 
 |-  ( ph -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " S ) ) )
450 hashss 
 |-  ( ( ( H " ( NN0 ^m ( 0 ... A ) ) ) e. _V /\ ( H " S ) C_ ( H " ( NN0 ^m ( 0 ... A ) ) ) ) -> ( # ` ( H " S ) ) <_ ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) )
451 135 152 450 syl2anc 
 |-  ( ph -> ( # ` ( H " S ) ) <_ ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) )
452 131 157 161 449 451 xrletrd 
 |-  ( ph -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) )