Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aks6d1c6lem3 Structured version   Visualization version   GIF version

Theorem aks6d1c6lem3 42174
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.)
Hypotheses
Ref Expression
aks6d1c6.1 = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1𝐾)‘𝑓)‘𝑦)) = (((eval1𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))}
aks6d1c6.2 𝑃 = (chr‘𝐾)
aks6d1c6.3 (𝜑𝐾 ∈ Field)
aks6d1c6.4 (𝜑𝑃 ∈ ℙ)
aks6d1c6.5 (𝜑𝑅 ∈ ℕ)
aks6d1c6.6 (𝜑𝑁 ∈ ℕ)
aks6d1c6.7 (𝜑𝑃𝑁)
aks6d1c6.8 (𝜑 → (𝑁 gcd 𝑅) = 1)
aks6d1c6.9 (𝜑𝐴 < 𝑃)
aks6d1c6.10 𝐺 = (𝑔 ∈ (ℕ0m (0...𝐴)) ↦ ((mulGrp‘(Poly1𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔𝑖)(.g‘(mulGrp‘(Poly1𝐾)))((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
aks6d1c6.11 (𝜑𝐴 ∈ ℕ0)
aks6d1c6.12 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))
aks6d1c6.13 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))
aks6d1c6.14 (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
aks6d1c6.15 (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
aks6d1c6.16 (𝜑𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
aks6d1c6.17 𝐻 = ( ∈ (ℕ0m (0...𝐴)) ↦ (((eval1𝐾)‘(𝐺))‘𝑀))
aks6d1c6.18 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))
aks6d1c6.19 𝑆 = {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)}
aks6d1c6lem3.1 𝐽 = (𝑗 ∈ (ℕ0 × ℕ0) ↦ ((𝐸𝑗)(.g‘(mulGrp‘𝐾))𝑀))
aks6d1c6lem3.2 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ≤ (♯‘(𝐽 “ (ℕ0 × ℕ0))))
Assertion
Ref Expression
aks6d1c6lem3 (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ0m (0...𝐴)))))
Distinct variable groups:   ,𝑎   𝑔,𝑖,𝜑   𝑆,𝑠,𝑡   ,𝐺   𝑆,,𝑗   𝑦,𝑀   𝑒,𝑁,𝑓   𝜑,,𝑗   𝑁,𝑠   𝑡,𝐾,𝑥   𝑅,𝑒,𝑓   𝑥,𝑃   𝑥,𝑅,𝑦   ,𝐾,𝑗   𝑒,𝐾,𝑓   ,𝑀,𝑗   𝑃,𝑘,𝑙,𝑠   𝑘,𝑁,𝑙,𝑥   𝑃,𝑒,𝑓   𝜑,𝑎   𝜑,𝑘,𝑦,𝑙,𝑥   𝑆,𝑔,𝑖,𝑥,𝑦   𝑆,𝑎   𝜑,𝑠,𝑡   𝐾,𝑎   𝑔,𝐾,𝑖,𝑦   𝑥,𝐸   𝑗,𝐸   𝑒,𝐸,𝑓,𝑦   𝐴,𝑠,𝑡   𝐴,𝑎   𝑖,𝐺,𝑡,𝑦   𝑔,𝐺   𝐷,𝑠   ,𝐻,𝑗   𝐻,𝑎   𝑔,𝐻,𝑖,𝑥,𝑦   𝐴,,𝑗   𝑒,𝐺,𝑓   𝑁,𝑎   𝐴,𝑔,𝑖,𝑥   𝐻,𝑠,𝑡
Allowed substitution hints:   𝜑(𝑒,𝑓)   𝐴(𝑦,𝑒,𝑓,𝑘,𝑙)   𝐷(𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,,𝑖,𝑗,𝑘,𝑎,𝑙)   𝑃(𝑦,𝑡,𝑔,,𝑖,𝑗,𝑎)   (𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,,𝑖,𝑗,𝑘,𝑠,𝑙)   𝑅(𝑡,𝑔,,𝑖,𝑗,𝑘,𝑠,𝑎,𝑙)   𝑆(𝑒,𝑓,𝑘,𝑙)   𝐸(𝑡,𝑔,,𝑖,𝑘,𝑠,𝑎,𝑙)   𝐺(𝑥,𝑗,𝑘,𝑠,𝑎,𝑙)   𝐻(𝑒,𝑓,𝑘,𝑙)   𝐽(𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,,𝑖,𝑗,𝑘,𝑠,𝑎,𝑙)   𝐾(𝑘,𝑠,𝑙)   𝐿(𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,,𝑖,𝑗,𝑘,𝑠,𝑎,𝑙)   𝑀(𝑥,𝑡,𝑒,𝑓,𝑔,𝑖,𝑘,𝑠,𝑎,𝑙)   𝑁(𝑦,𝑡,𝑔,,𝑖,𝑗)

Proof of Theorem aks6d1c6lem3
Dummy variables 𝑣 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 aks6d1c6.18 . . . . . . . . . . . 12 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))
2 aks6d1c6.6 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
3 aks6d1c6.4 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℙ)
4 aks6d1c6.7 . . . . . . . . . . . . 13 (𝜑𝑃𝑁)
5 aks6d1c6.5 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ℕ)
6 aks6d1c6.8 . . . . . . . . . . . . 13 (𝜑 → (𝑁 gcd 𝑅) = 1)
7 aks6d1c6.12 . . . . . . . . . . . . 13 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))
8 aks6d1c6.13 . . . . . . . . . . . . 13 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))
9 eqid 2736 . . . . . . . . . . . . 13 (ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅)
102, 3, 4, 5, 6, 7, 8, 9hashscontpowcl 42122 . . . . . . . . . . . 12 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℕ0)
111, 10eqeltrid 2844 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℕ0)
1211nn0zd 12641 . . . . . . . . . 10 (𝜑𝐷 ∈ ℤ)
1312zcnd 12725 . . . . . . . . 9 (𝜑𝐷 ∈ ℂ)
14 1cnd 11257 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
15 aks6d1c6.11 . . . . . . . . . 10 (𝜑𝐴 ∈ ℕ0)
1615nn0cnd 12591 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
1713, 14, 16nppcan3d 11648 . . . . . . . 8 (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = (𝐷 + 𝐴))
1817eqcomd 2742 . . . . . . 7 (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (𝐴 + 1)))
19 hashfz0 14472 . . . . . . . . . 10 (𝐴 ∈ ℕ0 → (♯‘(0...𝐴)) = (𝐴 + 1))
2015, 19syl 17 . . . . . . . . 9 (𝜑 → (♯‘(0...𝐴)) = (𝐴 + 1))
2120eqcomd 2742 . . . . . . . 8 (𝜑 → (𝐴 + 1) = (♯‘(0...𝐴)))
2221oveq2d 7448 . . . . . . 7 (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = ((𝐷 − 1) + (♯‘(0...𝐴))))
2318, 22eqtrd 2776 . . . . . 6 (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (♯‘(0...𝐴))))
24 1zzd 12650 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
2512, 24zsubcld 12729 . . . . . . . . 9 (𝜑 → (𝐷 − 1) ∈ ℤ)
26 0p1e1 12389 . . . . . . . . . . . 12 (0 + 1) = 1
2726a1i 11 . . . . . . . . . . 11 (𝜑 → (0 + 1) = 1)
28 fvexd 6920 . . . . . . . . . . . . . 14 (𝜑 → (ℤRHom‘(ℤ/nℤ‘𝑅)) ∈ V)
298, 28eqeltrid 2844 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ V)
3029imaexd 7939 . . . . . . . . . . . 12 (𝜑 → (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ V)
3115ne0d 4341 . . . . . . . . . . . . . . . 16 (𝜑 → ℕ0 ≠ ∅)
3231, 31jca 511 . . . . . . . . . . . . . . 15 (𝜑 → (ℕ0 ≠ ∅ ∧ ℕ0 ≠ ∅))
33 xpnz 6178 . . . . . . . . . . . . . . 15 ((ℕ0 ≠ ∅ ∧ ℕ0 ≠ ∅) ↔ (ℕ0 × ℕ0) ≠ ∅)
3432, 33sylib 218 . . . . . . . . . . . . . 14 (𝜑 → (ℕ0 × ℕ0) ≠ ∅)
35 ovexd 7467 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑙 ∈ ℕ0) → ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
3635ralrimiva 3145 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ0) → ∀𝑙 ∈ ℕ0 ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
3736ralrimiva 3145 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑘 ∈ ℕ0𝑙 ∈ ℕ0 ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
387fnmpo 8095 . . . . . . . . . . . . . . . . 17 (∀𝑘 ∈ ℕ0𝑙 ∈ ℕ0 ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V → 𝐸 Fn (ℕ0 × ℕ0))
3937, 38syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐸 Fn (ℕ0 × ℕ0))
40 ssidd 4006 . . . . . . . . . . . . . . . 16 (𝜑 → (ℕ0 × ℕ0) ⊆ (ℕ0 × ℕ0))
41 fnimaeq0 6700 . . . . . . . . . . . . . . . 16 ((𝐸 Fn (ℕ0 × ℕ0) ∧ (ℕ0 × ℕ0) ⊆ (ℕ0 × ℕ0)) → ((𝐸 “ (ℕ0 × ℕ0)) = ∅ ↔ (ℕ0 × ℕ0) = ∅))
4239, 40, 41syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐸 “ (ℕ0 × ℕ0)) = ∅ ↔ (ℕ0 × ℕ0) = ∅))
4342necon3bid 2984 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸 “ (ℕ0 × ℕ0)) ≠ ∅ ↔ (ℕ0 × ℕ0) ≠ ∅))
4434, 43mpbird 257 . . . . . . . . . . . . 13 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) ≠ ∅)
455nnnn0d 12589 . . . . . . . . . . . . . . . . . 18 (𝜑𝑅 ∈ ℕ0)
469zncrng 21564 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℕ0 → (ℤ/nℤ‘𝑅) ∈ CRing)
4745, 46syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℤ/nℤ‘𝑅) ∈ CRing)
48 crngring 20243 . . . . . . . . . . . . . . . . 17 ((ℤ/nℤ‘𝑅) ∈ CRing → (ℤ/nℤ‘𝑅) ∈ Ring)
498zrhrhm 21523 . . . . . . . . . . . . . . . . 17 ((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤring RingHom (ℤ/nℤ‘𝑅)))
50 zringbas 21465 . . . . . . . . . . . . . . . . . 18 ℤ = (Base‘ℤring)
51 eqid 2736 . . . . . . . . . . . . . . . . . 18 (Base‘(ℤ/nℤ‘𝑅)) = (Base‘(ℤ/nℤ‘𝑅))
5250, 51rhmf 20486 . . . . . . . . . . . . . . . . 17 (𝐿 ∈ (ℤring RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
5347, 48, 49, 524syl 19 . . . . . . . . . . . . . . . 16 (𝜑𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
5453ffnd 6736 . . . . . . . . . . . . . . 15 (𝜑𝐿 Fn ℤ)
557a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙))))
56 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) ∧ (𝑘 = 𝑥𝑙 = 𝑦)) → 𝑘 = 𝑥)
5756oveq2d 7448 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) ∧ (𝑘 = 𝑥𝑙 = 𝑦)) → (𝑃𝑘) = (𝑃𝑥))
58 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) ∧ (𝑘 = 𝑥𝑙 = 𝑦)) → 𝑙 = 𝑦)
5958oveq2d 7448 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) ∧ (𝑘 = 𝑥𝑙 = 𝑦)) → ((𝑁 / 𝑃)↑𝑙) = ((𝑁 / 𝑃)↑𝑦))
6057, 59oveq12d 7450 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) ∧ (𝑘 = 𝑥𝑙 = 𝑦)) → ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)) = ((𝑃𝑥) · ((𝑁 / 𝑃)↑𝑦)))
61 simplr 768 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → 𝑥 ∈ ℕ0)
62 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℕ0)
63 ovexd 7467 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → ((𝑃𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ V)
6455, 60, 61, 62, 63ovmpod 7586 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → (𝑥𝐸𝑦) = ((𝑃𝑥) · ((𝑁 / 𝑃)↑𝑦)))
653ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → 𝑃 ∈ ℙ)
66 prmnn 16712 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
6765, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → 𝑃 ∈ ℕ)
6867nnzd 12642 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → 𝑃 ∈ ℤ)
6968, 61zexpcld 14129 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → (𝑃𝑥) ∈ ℤ)
704ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → 𝑃𝑁)
7167nnne0d 12317 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → 𝑃 ≠ 0)
722nnzd 12642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ∈ ℤ)
7372adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℕ0) → 𝑁 ∈ ℤ)
7473adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → 𝑁 ∈ ℤ)
75 dvdsval2 16294 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
7668, 71, 74, 75syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → (𝑃𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
7770, 76mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → (𝑁 / 𝑃) ∈ ℤ)
7877, 62zexpcld 14129 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → ((𝑁 / 𝑃)↑𝑦) ∈ ℤ)
7969, 78zmulcld 12730 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → ((𝑃𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ ℤ)
8064, 79eqeltrd 2840 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℕ0) ∧ 𝑦 ∈ ℕ0) → (𝑥𝐸𝑦) ∈ ℤ)
8180ralrimiva 3145 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℕ0) → ∀𝑦 ∈ ℕ0 (𝑥𝐸𝑦) ∈ ℤ)
8281ralrimiva 3145 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥 ∈ ℕ0𝑦 ∈ ℕ0 (𝑥𝐸𝑦) ∈ ℤ)
8339, 82jca 511 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐸 Fn (ℕ0 × ℕ0) ∧ ∀𝑥 ∈ ℕ0𝑦 ∈ ℕ0 (𝑥𝐸𝑦) ∈ ℤ))
84 ffnov 7560 . . . . . . . . . . . . . . . . . 18 (𝐸:(ℕ0 × ℕ0)⟶ℤ ↔ (𝐸 Fn (ℕ0 × ℕ0) ∧ ∀𝑥 ∈ ℕ0𝑦 ∈ ℕ0 (𝑥𝐸𝑦) ∈ ℤ))
8583, 84sylibr 234 . . . . . . . . . . . . . . . . 17 (𝜑𝐸:(ℕ0 × ℕ0)⟶ℤ)
86 frn 6742 . . . . . . . . . . . . . . . . 17 (𝐸:(ℕ0 × ℕ0)⟶ℤ → ran 𝐸 ⊆ ℤ)
8785, 86syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝐸 ⊆ ℤ)
88 fnima 6697 . . . . . . . . . . . . . . . . . 18 (𝐸 Fn (ℕ0 × ℕ0) → (𝐸 “ (ℕ0 × ℕ0)) = ran 𝐸)
8939, 88syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) = ran 𝐸)
9089sseq1d 4014 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸 “ (ℕ0 × ℕ0)) ⊆ ℤ ↔ ran 𝐸 ⊆ ℤ))
9187, 90mpbird 257 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℤ)
92 fnimaeq0 6700 . . . . . . . . . . . . . . 15 ((𝐿 Fn ℤ ∧ (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℤ) → ((𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) = ∅ ↔ (𝐸 “ (ℕ0 × ℕ0)) = ∅))
9354, 91, 92syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) = ∅ ↔ (𝐸 “ (ℕ0 × ℕ0)) = ∅))
9493necon3bid 2984 . . . . . . . . . . . . 13 (𝜑 → ((𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ≠ ∅ ↔ (𝐸 “ (ℕ0 × ℕ0)) ≠ ∅))
9544, 94mpbird 257 . . . . . . . . . . . 12 (𝜑 → (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ≠ ∅)
96 hashge1 14429 . . . . . . . . . . . . 13 (((𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ≠ ∅) → 1 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))
971eqcomi 2745 . . . . . . . . . . . . . 14 (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) = 𝐷
9897a1i 11 . . . . . . . . . . . . 13 (((𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ≠ ∅) → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) = 𝐷)
9996, 98breqtrd 5168 . . . . . . . . . . . 12 (((𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ≠ ∅) → 1 ≤ 𝐷)
10030, 95, 99syl2anc 584 . . . . . . . . . . 11 (𝜑 → 1 ≤ 𝐷)
10127, 100eqbrtrd 5164 . . . . . . . . . 10 (𝜑 → (0 + 1) ≤ 𝐷)
102 0red 11265 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℝ)
103 1red 11263 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℝ)
10411nn0red 12590 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℝ)
105 leaddsub 11740 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
106102, 103, 104, 105syl3anc 1372 . . . . . . . . . 10 (𝜑 → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
107101, 106mpbid 232 . . . . . . . . 9 (𝜑 → 0 ≤ (𝐷 − 1))
10825, 107jca 511 . . . . . . . 8 (𝜑 → ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
109 elnn0z 12628 . . . . . . . 8 ((𝐷 − 1) ∈ ℕ0 ↔ ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
110108, 109sylibr 234 . . . . . . 7 (𝜑 → (𝐷 − 1) ∈ ℕ0)
111 fzfid 14015 . . . . . . . 8 (𝜑 → (0...𝐴) ∈ Fin)
112 hashcl 14396 . . . . . . . 8 ((0...𝐴) ∈ Fin → (♯‘(0...𝐴)) ∈ ℕ0)
113111, 112syl 17 . . . . . . 7 (𝜑 → (♯‘(0...𝐴)) ∈ ℕ0)
114110, 113nn0addcld 12593 . . . . . 6 (𝜑 → ((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ0)
11523, 114eqeltrd 2840 . . . . 5 (𝜑 → (𝐷 + 𝐴) ∈ ℕ0)
116 bccl 14362 . . . . 5 (((𝐷 + 𝐴) ∈ ℕ0 ∧ (𝐷 − 1) ∈ ℤ) → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ0)
117115, 25, 116syl2anc 584 . . . 4 (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ0)
118117nn0red 12590 . . 3 (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ)
119118rexrd 11312 . 2 (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ*)
120 aks6d1c6.17 . . . . . . 7 𝐻 = ( ∈ (ℕ0m (0...𝐴)) ↦ (((eval1𝐾)‘(𝐺))‘𝑀))
121 ovexd 7467 . . . . . . . 8 (𝜑 → (ℕ0m (0...𝐴)) ∈ V)
122121mptexd 7245 . . . . . . 7 (𝜑 → ( ∈ (ℕ0m (0...𝐴)) ↦ (((eval1𝐾)‘(𝐺))‘𝑀)) ∈ V)
123120, 122eqeltrid 2844 . . . . . 6 (𝜑𝐻 ∈ V)
124123imaexd 7939 . . . . 5 (𝜑 → (𝐻 “ (ℕ0m (0...𝐴))) ∈ V)
125 simprl 770 . . . . . . . . . 10 ((𝜑 ∧ (𝑤 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤𝑡) ≤ (𝐷 − 1))) → 𝑤 ∈ (ℕ0m (0...𝐴)))
126125ex 412 . . . . . . . . 9 (𝜑 → ((𝑤 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤𝑡) ≤ (𝐷 − 1)) → 𝑤 ∈ (ℕ0m (0...𝐴))))
127 simpl 482 . . . . . . . . . . . . . . . 16 ((𝑠 = 𝑤𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑤)
128127fveq1d 6907 . . . . . . . . . . . . . . 15 ((𝑠 = 𝑤𝑡 ∈ (0...𝐴)) → (𝑠𝑡) = (𝑤𝑡))
129128sumeq2dv 15739 . . . . . . . . . . . . . 14 (𝑠 = 𝑤 → Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑤𝑡))
130129breq1d 5152 . . . . . . . . . . . . 13 (𝑠 = 𝑤 → (Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑤𝑡) ≤ (𝐷 − 1)))
131130elrab 3691 . . . . . . . . . . . 12 (𝑤 ∈ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} ↔ (𝑤 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤𝑡) ≤ (𝐷 − 1)))
132131a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} ↔ (𝑤 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤𝑡) ≤ (𝐷 − 1))))
133132biimpd 229 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} → (𝑤 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤𝑡) ≤ (𝐷 − 1))))
134133imim1d 82 . . . . . . . . 9 (𝜑 → (((𝑤 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤𝑡) ≤ (𝐷 − 1)) → 𝑤 ∈ (ℕ0m (0...𝐴))) → (𝑤 ∈ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} → 𝑤 ∈ (ℕ0m (0...𝐴)))))
135126, 134mpd 15 . . . . . . . 8 (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} → 𝑤 ∈ (ℕ0m (0...𝐴))))
136135ssrdv 3988 . . . . . . 7 (𝜑 → {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ0m (0...𝐴)))
137 aks6d1c6.19 . . . . . . . . 9 𝑆 = {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)}
138137a1i 11 . . . . . . . 8 (𝜑𝑆 = {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)})
139138sseq1d 4014 . . . . . . 7 (𝜑 → (𝑆 ⊆ (ℕ0m (0...𝐴)) ↔ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ0m (0...𝐴))))
140136, 139mpbird 257 . . . . . 6 (𝜑𝑆 ⊆ (ℕ0m (0...𝐴)))
141 imass2 6119 . . . . . 6 (𝑆 ⊆ (ℕ0m (0...𝐴)) → (𝐻𝑆) ⊆ (𝐻 “ (ℕ0m (0...𝐴))))
142140, 141syl 17 . . . . 5 (𝜑 → (𝐻𝑆) ⊆ (𝐻 “ (ℕ0m (0...𝐴))))
143124, 142ssexd 5323 . . . 4 (𝜑 → (𝐻𝑆) ∈ V)
144 hashxnn0 14379 . . . 4 ((𝐻𝑆) ∈ V → (♯‘(𝐻𝑆)) ∈ ℕ0*)
145143, 144syl 17 . . 3 (𝜑 → (♯‘(𝐻𝑆)) ∈ ℕ0*)
146 xnn0xr 12606 . . 3 ((♯‘(𝐻𝑆)) ∈ ℕ0* → (♯‘(𝐻𝑆)) ∈ ℝ*)
147145, 146syl 17 . 2 (𝜑 → (♯‘(𝐻𝑆)) ∈ ℝ*)
148 hashxnn0 14379 . . . 4 ((𝐻 “ (ℕ0m (0...𝐴))) ∈ V → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ∈ ℕ0*)
149124, 148syl 17 . . 3 (𝜑 → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ∈ ℕ0*)
150 xnn0xr 12606 . . 3 ((♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ∈ ℕ0* → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ∈ ℝ*)
151149, 150syl 17 . 2 (𝜑 → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ∈ ℝ*)
152110nn0cnd 12591 . . . . . . . . 9 (𝜑 → (𝐷 − 1) ∈ ℂ)
153113nn0cnd 12591 . . . . . . . . 9 (𝜑 → (♯‘(0...𝐴)) ∈ ℂ)
154152, 153pncand 11622 . . . . . . . 8 (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))) = (𝐷 − 1))
155154eqcomd 2742 . . . . . . 7 (𝜑 → (𝐷 − 1) = (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))))
15623, 155oveq12d 7450 . . . . . 6 (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
15715nn0ge0d 12592 . . . . . . . . . . 11 (𝜑 → 0 ≤ 𝐴)
158 0zd 12627 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ℤ)
15915nn0zd 12641 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℤ)
160 eluz 12893 . . . . . . . . . . . 12 ((0 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ (ℤ‘0) ↔ 0 ≤ 𝐴))
161158, 159, 160syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝐴 ∈ (ℤ‘0) ↔ 0 ≤ 𝐴))
162157, 161mpbird 257 . . . . . . . . . 10 (𝜑𝐴 ∈ (ℤ‘0))
163 fzn0 13579 . . . . . . . . . 10 ((0...𝐴) ≠ ∅ ↔ 𝐴 ∈ (ℤ‘0))
164162, 163sylibr 234 . . . . . . . . 9 (𝜑 → (0...𝐴) ≠ ∅)
165110, 111, 164, 137sticksstones23 42171 . . . . . . . 8 (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))))
166113nn0zd 12641 . . . . . . . . 9 (𝜑 → (♯‘(0...𝐴)) ∈ ℤ)
167 bccmpl 14349 . . . . . . . . 9 ((((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ0 ∧ (♯‘(0...𝐴)) ∈ ℤ) → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
168114, 166, 167syl2anc 584 . . . . . . . 8 (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
169165, 168eqtrd 2776 . . . . . . 7 (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
170169eqcomd 2742 . . . . . 6 (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))) = (♯‘𝑆))
171156, 170eqtrd 2776 . . . . 5 (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
172171adantr 480 . . . 4 ((𝜑 ∧ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
173120a1i 11 . . . . . . 7 ((𝜑 ∧ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → 𝐻 = ( ∈ (ℕ0m (0...𝐴)) ↦ (((eval1𝐾)‘(𝐺))‘𝑀)))
174 ovexd 7467 . . . . . . . 8 ((𝜑 ∧ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → (ℕ0m (0...𝐴)) ∈ V)
175174mptexd 7245 . . . . . . 7 ((𝜑 ∧ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → ( ∈ (ℕ0m (0...𝐴)) ↦ (((eval1𝐾)‘(𝐺))‘𝑀)) ∈ V)
176173, 175eqeltrd 2840 . . . . . 6 ((𝜑 ∧ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → 𝐻 ∈ V)
177176resexd 6045 . . . . 5 ((𝜑 ∧ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → (𝐻𝑆) ∈ V)
178176imaexd 7939 . . . . 5 ((𝜑 ∧ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → (𝐻𝑆) ∈ V)
179 simpr 484 . . . . 5 ((𝜑 ∧ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → (𝐻𝑆):𝑆1-1→(𝐻𝑆))
180 hashf1dmcdm 14484 . . . . 5 (((𝐻𝑆) ∈ V ∧ (𝐻𝑆) ∈ V ∧ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻𝑆)))
181177, 178, 179, 180syl3anc 1372 . . . 4 ((𝜑 ∧ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻𝑆)))
182172, 181eqbrtrd 5164 . . 3 ((𝜑 ∧ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆)))
183120a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑆) → 𝐻 = ( ∈ (ℕ0m (0...𝐴)) ↦ (((eval1𝐾)‘(𝐺))‘𝑀)))
184 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗𝑆) ∧ = 𝑗) → = 𝑗)
185184fveq2d 6909 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗𝑆) ∧ = 𝑗) → (𝐺) = (𝐺𝑗))
186185fveq2d 6909 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑆) ∧ = 𝑗) → ((eval1𝐾)‘(𝐺)) = ((eval1𝐾)‘(𝐺𝑗)))
187186fveq1d 6907 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑆) ∧ = 𝑗) → (((eval1𝐾)‘(𝐺))‘𝑀) = (((eval1𝐾)‘(𝐺𝑗))‘𝑀))
188 simp2 1137 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑠 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)) → 𝑠 ∈ (ℕ0m (0...𝐴)))
189188rabssdv 4074 . . . . . . . . . . . . . . . . . 18 (𝜑 → {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ0m (0...𝐴)))
190137, 189eqsstrid 4021 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 ⊆ (ℕ0m (0...𝐴)))
191190sselda 3982 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑆) → 𝑗 ∈ (ℕ0m (0...𝐴)))
192 fvexd 6920 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑆) → (((eval1𝐾)‘(𝐺𝑗))‘𝑀) ∈ V)
193183, 187, 191, 192fvmptd 7022 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑆) → (𝐻𝑗) = (((eval1𝐾)‘(𝐺𝑗))‘𝑀))
194 eqid 2736 . . . . . . . . . . . . . . . 16 (eval1𝐾) = (eval1𝐾)
195 eqid 2736 . . . . . . . . . . . . . . . 16 (Poly1𝐾) = (Poly1𝐾)
196 eqid 2736 . . . . . . . . . . . . . . . 16 (Base‘𝐾) = (Base‘𝐾)
197 eqid 2736 . . . . . . . . . . . . . . . 16 (Base‘(Poly1𝐾)) = (Base‘(Poly1𝐾))
198 aks6d1c6.3 . . . . . . . . . . . . . . . . . 18 (𝜑𝐾 ∈ Field)
199198fldcrngd 20743 . . . . . . . . . . . . . . . . 17 (𝜑𝐾 ∈ CRing)
200199adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑆) → 𝐾 ∈ CRing)
201 aks6d1c6.16 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
202 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . 24 (mulGrp‘𝐾) = (mulGrp‘𝐾)
203202crngmgp 20239 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
204199, 203syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
205 eqid 2736 . . . . . . . . . . . . . . . . . . . . . 22 (.g‘(mulGrp‘𝐾)) = (.g‘(mulGrp‘𝐾))
206204, 45, 205isprimroot 42095 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) ↔ (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ0 ((𝑣(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) → 𝑅𝑣))))
207206biimpd 229 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ0 ((𝑣(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) → 𝑅𝑣))))
208201, 207mpd 15 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ0 ((𝑣(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) → 𝑅𝑣)))
209208simp1d 1142 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ (Base‘(mulGrp‘𝐾)))
210202, 196mgpbas 20143 . . . . . . . . . . . . . . . . . . 19 (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
211210eqcomi 2745 . . . . . . . . . . . . . . . . . 18 (Base‘(mulGrp‘𝐾)) = (Base‘𝐾)
212209, 211eleqtrdi 2850 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ (Base‘𝐾))
213212adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑆) → 𝑀 ∈ (Base‘𝐾))
214 aks6d1c6.2 . . . . . . . . . . . . . . . . . . 19 𝑃 = (chr‘𝐾)
215 aks6d1c6.9 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 < 𝑃)
216 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (var1𝐾) = (var1𝐾)
217 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (.g‘(mulGrp‘(Poly1𝐾))) = (.g‘(mulGrp‘(Poly1𝐾)))
218 aks6d1c6.10 . . . . . . . . . . . . . . . . . . 19 𝐺 = (𝑔 ∈ (ℕ0m (0...𝐴)) ↦ ((mulGrp‘(Poly1𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔𝑖)(.g‘(mulGrp‘(Poly1𝐾)))((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
219198, 3, 214, 15, 215, 216, 217, 218aks6d1c5lem0 42137 . . . . . . . . . . . . . . . . . 18 (𝜑𝐺:(ℕ0m (0...𝐴))⟶(Base‘(Poly1𝐾)))
220219adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑆) → 𝐺:(ℕ0m (0...𝐴))⟶(Base‘(Poly1𝐾)))
221220, 191ffvelcdmd 7104 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑆) → (𝐺𝑗) ∈ (Base‘(Poly1𝐾)))
222194, 195, 196, 197, 200, 213, 221fveval1fvcl 22338 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑆) → (((eval1𝐾)‘(𝐺𝑗))‘𝑀) ∈ (Base‘𝐾))
223193, 222eqeltrd 2840 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑆) → (𝐻𝑗) ∈ (Base‘𝐾))
224 eqid 2736 . . . . . . . . . . . . . 14 (𝑗𝑆 ↦ (𝐻𝑗)) = (𝑗𝑆 ↦ (𝐻𝑗))
225223, 224fmptd 7133 . . . . . . . . . . . . 13 (𝜑 → (𝑗𝑆 ↦ (𝐻𝑗)):𝑆⟶(Base‘𝐾))
226 fvexd 6920 . . . . . . . . . . . . . . . 16 ((𝜑 ∈ (ℕ0m (0...𝐴))) → (((eval1𝐾)‘(𝐺))‘𝑀) ∈ V)
227226, 120fmptd 7133 . . . . . . . . . . . . . . 15 (𝜑𝐻:(ℕ0m (0...𝐴))⟶V)
228227, 190feqresmpt 6977 . . . . . . . . . . . . . 14 (𝜑 → (𝐻𝑆) = (𝑗𝑆 ↦ (𝐻𝑗)))
229228feq1d 6719 . . . . . . . . . . . . 13 (𝜑 → ((𝐻𝑆):𝑆⟶(Base‘𝐾) ↔ (𝑗𝑆 ↦ (𝐻𝑗)):𝑆⟶(Base‘𝐾)))
230225, 229mpbird 257 . . . . . . . . . . . 12 (𝜑 → (𝐻𝑆):𝑆⟶(Base‘𝐾))
231 ffrn 6748 . . . . . . . . . . . 12 ((𝐻𝑆):𝑆⟶(Base‘𝐾) → (𝐻𝑆):𝑆⟶ran (𝐻𝑆))
232230, 231syl 17 . . . . . . . . . . 11 (𝜑 → (𝐻𝑆):𝑆⟶ran (𝐻𝑆))
233 df-ima 5697 . . . . . . . . . . . . 13 (𝐻𝑆) = ran (𝐻𝑆)
234233a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐻𝑆) = ran (𝐻𝑆))
235234feq3d 6722 . . . . . . . . . . 11 (𝜑 → ((𝐻𝑆):𝑆⟶(𝐻𝑆) ↔ (𝐻𝑆):𝑆⟶ran (𝐻𝑆)))
236232, 235mpbird 257 . . . . . . . . . 10 (𝜑 → (𝐻𝑆):𝑆⟶(𝐻𝑆))
237236notnotd 144 . . . . . . . . 9 (𝜑 → ¬ ¬ (𝐻𝑆):𝑆⟶(𝐻𝑆))
238237a1d 25 . . . . . . . 8 (𝜑 → (¬ ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆)) → ¬ ¬ (𝐻𝑆):𝑆⟶(𝐻𝑆)))
239238con4d 115 . . . . . . 7 (𝜑 → (¬ (𝐻𝑆):𝑆⟶(𝐻𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))))
240 df-an 396 . . . . . . . . . . . . . 14 ((((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣))
241240a1i 11 . . . . . . . . . . . . 13 ((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) → ((((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣)))
242 eqid 2736 . . . . . . . . . . . . . . . 16 (deg1𝐾) = (deg1𝐾)
243 eqid 2736 . . . . . . . . . . . . . . . 16 (0g𝐾) = (0g𝐾)
244 eqid 2736 . . . . . . . . . . . . . . . 16 (0g‘(Poly1𝐾)) = (0g‘(Poly1𝐾))
245 fldidom 20772 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ Field → 𝐾 ∈ IDomn)
246198, 245syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐾 ∈ IDomn)
247246ad4antr 732 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ IDomn)
248195ply1crng 22201 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ CRing → (Poly1𝐾) ∈ CRing)
249 crngring 20243 . . . . . . . . . . . . . . . . . . 19 ((Poly1𝐾) ∈ CRing → (Poly1𝐾) ∈ Ring)
250 ringgrp 20236 . . . . . . . . . . . . . . . . . . 19 ((Poly1𝐾) ∈ Ring → (Poly1𝐾) ∈ Grp)
251199, 248, 249, 2504syl 19 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Poly1𝐾) ∈ Grp)
252251ad4antr 732 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (Poly1𝐾) ∈ Grp)
253198, 3, 214, 15, 215, 216, 217, 218aks6d1c5 42141 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:(ℕ0m (0...𝐴))–1-1→(Base‘(Poly1𝐾)))
254253ad4antr 732 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ0m (0...𝐴))–1-1→(Base‘(Poly1𝐾)))
255 f1f 6803 . . . . . . . . . . . . . . . . . . 19 (𝐺:(ℕ0m (0...𝐴))–1-1→(Base‘(Poly1𝐾)) → 𝐺:(ℕ0m (0...𝐴))⟶(Base‘(Poly1𝐾)))
256254, 255syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ0m (0...𝐴))⟶(Base‘(Poly1𝐾)))
257137eleq2i 2832 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢𝑆𝑢 ∈ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)})
258 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 = 𝑢𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑢)
259258fveq1d 6907 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 = 𝑢𝑡 ∈ (0...𝐴)) → (𝑠𝑡) = (𝑢𝑡))
260259sumeq2dv 15739 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = 𝑢 → Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑢𝑡))
261260breq1d 5152 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = 𝑢 → (Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑢𝑡) ≤ (𝐷 − 1)))
262261elrab 3691 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} ↔ (𝑢 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢𝑡) ≤ (𝐷 − 1)))
263262simplbi 497 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 ∈ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} → 𝑢 ∈ (ℕ0m (0...𝐴)))
264257, 263sylbi 217 . . . . . . . . . . . . . . . . . . . . 21 (𝑢𝑆𝑢 ∈ (ℕ0m (0...𝐴)))
265264adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) → 𝑢 ∈ (ℕ0m (0...𝐴)))
266265adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) → 𝑢 ∈ (ℕ0m (0...𝐴)))
267266adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ (ℕ0m (0...𝐴)))
268256, 267ffvelcdmd 7104 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺𝑢) ∈ (Base‘(Poly1𝐾)))
269137eleq2i 2832 . . . . . . . . . . . . . . . . . . . . 21 (𝑣𝑆𝑣 ∈ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)})
270 elrabi 3686 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 ∈ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} → 𝑣 ∈ (ℕ0m (0...𝐴)))
271269, 270sylbi 217 . . . . . . . . . . . . . . . . . . . 20 (𝑣𝑆𝑣 ∈ (ℕ0m (0...𝐴)))
272271adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) → 𝑣 ∈ (ℕ0m (0...𝐴)))
273272adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ (ℕ0m (0...𝐴)))
274256, 273ffvelcdmd 7104 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺𝑣) ∈ (Base‘(Poly1𝐾)))
275 eqid 2736 . . . . . . . . . . . . . . . . . 18 (-g‘(Poly1𝐾)) = (-g‘(Poly1𝐾))
276197, 275grpsubcl 19039 . . . . . . . . . . . . . . . . 17 (((Poly1𝐾) ∈ Grp ∧ (𝐺𝑢) ∈ (Base‘(Poly1𝐾)) ∧ (𝐺𝑣) ∈ (Base‘(Poly1𝐾))) → ((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)) ∈ (Base‘(Poly1𝐾)))
277252, 268, 274, 276syl3anc 1372 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)) ∈ (Base‘(Poly1𝐾)))
278 neqne 2947 . . . . . . . . . . . . . . . . . . . 20 𝑢 = 𝑣𝑢𝑣)
279278adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → 𝑢𝑣)
280279adantl 481 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢𝑣)
281267, 273jca 511 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ∈ (ℕ0m (0...𝐴)) ∧ 𝑣 ∈ (ℕ0m (0...𝐴))))
282 f1fveq 7283 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺:(ℕ0m (0...𝐴))–1-1→(Base‘(Poly1𝐾)) ∧ (𝑢 ∈ (ℕ0m (0...𝐴)) ∧ 𝑣 ∈ (ℕ0m (0...𝐴)))) → ((𝐺𝑢) = (𝐺𝑣) ↔ 𝑢 = 𝑣))
283254, 281, 282syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺𝑢) = (𝐺𝑣) ↔ 𝑢 = 𝑣))
284283bicomd 223 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 = 𝑣 ↔ (𝐺𝑢) = (𝐺𝑣)))
285284necon3bid 2984 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢𝑣 ↔ (𝐺𝑢) ≠ (𝐺𝑣)))
286285biimpd 229 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢𝑣 → (𝐺𝑢) ≠ (𝐺𝑣)))
287280, 286mpd 15 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺𝑢) ≠ (𝐺𝑣))
288197, 244, 275grpsubeq0 19045 . . . . . . . . . . . . . . . . . . 19 (((Poly1𝐾) ∈ Grp ∧ (𝐺𝑢) ∈ (Base‘(Poly1𝐾)) ∧ (𝐺𝑣) ∈ (Base‘(Poly1𝐾))) → (((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)) = (0g‘(Poly1𝐾)) ↔ (𝐺𝑢) = (𝐺𝑣)))
289288necon3bid 2984 . . . . . . . . . . . . . . . . . 18 (((Poly1𝐾) ∈ Grp ∧ (𝐺𝑢) ∈ (Base‘(Poly1𝐾)) ∧ (𝐺𝑣) ∈ (Base‘(Poly1𝐾))) → (((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)) ≠ (0g‘(Poly1𝐾)) ↔ (𝐺𝑢) ≠ (𝐺𝑣)))
290252, 268, 274, 289syl3anc 1372 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)) ≠ (0g‘(Poly1𝐾)) ↔ (𝐺𝑢) ≠ (𝐺𝑣)))
291287, 290mpbird 257 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)) ≠ (0g‘(Poly1𝐾)))
292195, 197, 242, 194, 243, 244, 247, 277, 291fta1g 26210 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ≤ ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))))
293242, 195, 197deg1xrcl 26122 . . . . . . . . . . . . . . . . . 18 (((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)) ∈ (Base‘(Poly1𝐾)) → ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ ℝ*)
294277, 293syl 17 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ ℝ*)
295104ad4antr 732 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ)
296 1red 11263 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 1 ∈ ℝ)
297295, 296resubcld 11692 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ)
298297rexrd 11312 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ*)
299 simp-4l 782 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝜑)
300 fvexd 6920 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ V)
301 cnvexg 7947 . . . . . . . . . . . . . . . . . . . 20 (((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ V → ((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ V)
302300, 301syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ V)
303302imaexd 7939 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)}) ∈ V)
304 hashxnn0 14379 . . . . . . . . . . . . . . . . . 18 ((((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)}) ∈ V → (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ∈ ℕ0*)
305 xnn0xr 12606 . . . . . . . . . . . . . . . . . 18 ((♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ∈ ℕ0* → (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ∈ ℝ*)
306299, 303, 304, 3054syl 19 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ∈ ℝ*)
307242, 195, 197deg1xrcl 26122 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝑣) ∈ (Base‘(Poly1𝐾)) → ((deg1𝐾)‘(𝐺𝑣)) ∈ ℝ*)
308274, 307syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1𝐾)‘(𝐺𝑣)) ∈ ℝ*)
309242, 195, 197deg1xrcl 26122 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝑢) ∈ (Base‘(Poly1𝐾)) → ((deg1𝐾)‘(𝐺𝑢)) ∈ ℝ*)
310268, 309syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1𝐾)‘(𝐺𝑢)) ∈ ℝ*)
311308, 310ifcld 4571 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑢))) ∈ ℝ*)
312247idomringd 20729 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Ring)
313195, 242, 312, 197, 275, 268, 274deg1suble 26147 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ≤ if(((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑢))))
314 id 22 . . . . . . . . . . . . . . . . . . . 20 (((deg1𝐾)‘(𝐺𝑣)) = if(((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑢))) → ((deg1𝐾)‘(𝐺𝑣)) = if(((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑢))))
315314breq1d 5152 . . . . . . . . . . . . . . . . . . 19 (((deg1𝐾)‘(𝐺𝑣)) = if(((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑢))) → (((deg1𝐾)‘(𝐺𝑣)) ≤ (𝐷 − 1) ↔ if(((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑢))) ≤ (𝐷 − 1)))
316 id 22 . . . . . . . . . . . . . . . . . . . 20 (((deg1𝐾)‘(𝐺𝑢)) = if(((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑢))) → ((deg1𝐾)‘(𝐺𝑢)) = if(((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑢))))
317316breq1d 5152 . . . . . . . . . . . . . . . . . . 19 (((deg1𝐾)‘(𝐺𝑢)) = if(((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑢))) → (((deg1𝐾)‘(𝐺𝑢)) ≤ (𝐷 − 1) ↔ if(((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑢))) ≤ (𝐷 − 1)))
318 aks6d1c6.1 . . . . . . . . . . . . . . . . . . . . 21 = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1𝐾)‘𝑓)‘𝑦)) = (((eval1𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))}
319198ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝐾 ∈ Field)
3203ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑃 ∈ ℙ)
3215ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑅 ∈ ℕ)
3222ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑁 ∈ ℕ)
3234ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑃𝑁)
3246ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → (𝑁 gcd 𝑅) = 1)
325215ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝐴 < 𝑃)
32615ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝐴 ∈ ℕ0)
327 aks6d1c6.14 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
328327ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
329 aks6d1c6.15 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
330329ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
331201ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
332 simpllr 775 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑣𝑆)
333332, 271syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑣 ∈ (ℕ0m (0...𝐴)))
334318, 214, 319, 320, 321, 322, 323, 324, 325, 218, 326, 7, 8, 328, 330, 331, 120, 1, 137, 333aks6d1c6lem1 42172 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → ((deg1𝐾)‘(𝐺𝑣)) = Σ𝑡 ∈ (0...𝐴)(𝑣𝑡))
335 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 = 𝑣𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑣)
336335fveq1d 6907 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 = 𝑣𝑡 ∈ (0...𝐴)) → (𝑠𝑡) = (𝑣𝑡))
337336sumeq2dv 15739 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = 𝑣 → Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑣𝑡))
338337breq1d 5152 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = 𝑣 → (Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑣𝑡) ≤ (𝐷 − 1)))
339338elrab 3691 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∈ {𝑠 ∈ (ℕ0m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠𝑡) ≤ (𝐷 − 1)} ↔ (𝑣 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣𝑡) ≤ (𝐷 − 1)))
340269, 339bitri 275 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣𝑆 ↔ (𝑣 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣𝑡) ≤ (𝐷 − 1)))
341332, 340sylib 218 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → (𝑣 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣𝑡) ≤ (𝐷 − 1)))
342341simprd 495 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑣𝑡) ≤ (𝐷 − 1))
343334, 342eqbrtrd 5164 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → ((deg1𝐾)‘(𝐺𝑣)) ≤ (𝐷 − 1))
344198ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝐾 ∈ Field)
3453ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑃 ∈ ℙ)
3465ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑅 ∈ ℕ)
3472ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑁 ∈ ℕ)
3484ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑃𝑁)
3496ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → (𝑁 gcd 𝑅) = 1)
350215ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝐴 < 𝑃)
35115ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝐴 ∈ ℕ0)
352327ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
353329ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
354201ad5antr 734 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
355267adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑢 ∈ (ℕ0m (0...𝐴)))
356318, 214, 344, 345, 346, 347, 348, 349, 350, 218, 351, 7, 8, 352, 353, 354, 120, 1, 137, 355aks6d1c6lem1 42172 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → ((deg1𝐾)‘(𝐺𝑢)) = Σ𝑡 ∈ (0...𝐴)(𝑢𝑡))
357 simp-4r 783 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → 𝑢𝑆)
358257, 262bitri 275 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢𝑆 ↔ (𝑢 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢𝑡) ≤ (𝐷 − 1)))
359357, 358sylib 218 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → (𝑢 ∈ (ℕ0m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢𝑡) ≤ (𝐷 − 1)))
360359simprd 495 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑢𝑡) ≤ (𝐷 − 1))
361356, 360eqbrtrd 5164 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣))) → ((deg1𝐾)‘(𝐺𝑢)) ≤ (𝐷 − 1))
362315, 317, 343, 361ifbothda 4563 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg1𝐾)‘(𝐺𝑢)) ≤ ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑣)), ((deg1𝐾)‘(𝐺𝑢))) ≤ (𝐷 − 1))
363294, 311, 298, 313, 362xrletrd 13205 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ≤ (𝐷 − 1))
364295rexrd 11312 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ*)
365295ltm1d 12201 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < 𝐷)
366 simpllr 775 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢𝑆)
367 simplr 768 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣𝑆)
368299, 366, 367jca31 514 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝜑𝑢𝑆) ∧ 𝑣𝑆))
369 simpr 484 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣))
370368, 369jca 511 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)))
371198ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Field)
3723ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∈ ℙ)
3735ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑅 ∈ ℕ)
3742ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑁 ∈ ℕ)
3754ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃𝑁)
3766ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑁 gcd 𝑅) = 1)
377215ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 < 𝑃)
37815ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 ∈ ℕ0)
379327ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ∀𝑎 ∈ (1...𝐴)𝑁 ((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
380329ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
381201ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
382 simpllr 775 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢𝑆)
383 simplr 768 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣𝑆)
384 simprl 770 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣))
385279adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢𝑣)
386 aks6d1c6lem3.1 . . . . . . . . . . . . . . . . . . . 20 𝐽 = (𝑗 ∈ (ℕ0 × ℕ0) ↦ ((𝐸𝑗)(.g‘(mulGrp‘𝐾))𝑀))
387 aks6d1c6lem3.2 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ≤ (♯‘(𝐽 “ (ℕ0 × ℕ0))))
388387ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ≤ (♯‘(𝐽 “ (ℕ0 × ℕ0))))
389318, 214, 371, 372, 373, 374, 375, 376, 377, 218, 378, 7, 8, 379, 380, 381, 120, 1, 137, 382, 383, 384, 385, 386, 388aks6d1c6lem2 42173 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})))
390370, 389syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})))
391298, 364, 306, 365, 390xrltletrd 13204 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})))
392294, 298, 306, 363, 391xrlelttrd 13203 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) < (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})))
393242, 195, 244, 197deg1nn0clb 26130 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ Ring ∧ ((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)) ∈ (Base‘(Poly1𝐾))) → (((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)) ≠ (0g‘(Poly1𝐾)) ↔ ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ ℕ0))
394312, 277, 393syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)) ≠ (0g‘(Poly1𝐾)) ↔ ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ ℕ0))
395291, 394mpbid 232 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ ℕ0)
396395nn0red 12590 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ ℝ)
397396rexrd 11312 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ ℝ*)
398 fvexd 6920 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ V)
399398, 301syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ V)
400399imaexd 7939 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)}) ∈ V)
401400, 304syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ∈ ℕ0*)
402401, 305syl 17 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ∈ ℝ*)
403 xrltnle 11329 . . . . . . . . . . . . . . . . 17 ((((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) ∈ ℝ* ∧ (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ∈ ℝ*) → (((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) < (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ↔ ¬ (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ≤ ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)))))
404397, 402, 403syl2anc 584 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) < (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ↔ ¬ (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ≤ ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣)))))
405392, 404mpbid 232 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ¬ (♯‘(((eval1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))) “ {(0g𝐾)})) ≤ ((deg1𝐾)‘((𝐺𝑢)(-g‘(Poly1𝐾))(𝐺𝑣))))
406292, 405pm2.21dd 195 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆)))
407406ex 412 . . . . . . . . . . . . 13 ((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) → ((((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))))
408241, 407sylbird 260 . . . . . . . . . . . 12 ((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) → (¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))))
409 biidd 262 . . . . . . . . . . . . . . . . . 18 (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → (𝑢 = 𝑣𝑢 = 𝑣))
410409necon3abid 2976 . . . . . . . . . . . . . . . . 17 (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → (𝑢𝑣 ↔ ¬ 𝑢 = 𝑣))
411410necon1bbid 2979 . . . . . . . . . . . . . . . 16 (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → (¬ ¬ 𝑢 = 𝑣𝑢 = 𝑣))
412411pm5.74i 271 . . . . . . . . . . . . . . 15 ((((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → 𝑢 = 𝑣))
413412notbii 320 . . . . . . . . . . . . . 14 (¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → 𝑢 = 𝑣))
414413a1i 11 . . . . . . . . . . . . 13 ((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) → (¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → 𝑢 = 𝑣)))
415414imbi1d 341 . . . . . . . . . . . 12 ((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) → ((¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))) ↔ (¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆)))))
416408, 415mpbid 232 . . . . . . . . . . 11 ((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) → (¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))))
417416imp 406 . . . . . . . . . 10 (((((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢𝑆) ∧ 𝑣𝑆) ∧ ¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆)))
418 fveqeq2 6914 . . . . . . . . . . . . . . 15 (𝑥 = 𝑢 → (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) ↔ ((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑦)))
419 equequ1 2023 . . . . . . . . . . . . . . 15 (𝑥 = 𝑢 → (𝑥 = 𝑦𝑢 = 𝑦))
420418, 419imbi12d 344 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → ((((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑦) → 𝑢 = 𝑦)))
421420notbid 318 . . . . . . . . . . . . 13 (𝑥 = 𝑢 → (¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑦) → 𝑢 = 𝑦)))
422 fveq2 6905 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑣 → ((𝐻𝑆)‘𝑦) = ((𝐻𝑆)‘𝑣))
423422eqeq2d 2747 . . . . . . . . . . . . . . 15 (𝑦 = 𝑣 → (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑦) ↔ ((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣)))
424 equequ2 2024 . . . . . . . . . . . . . . 15 (𝑦 = 𝑣 → (𝑢 = 𝑦𝑢 = 𝑣))
425423, 424imbi12d 344 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → ((((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → 𝑢 = 𝑣)))
426425notbid 318 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → (¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ ¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → 𝑢 = 𝑣)))
427421, 426cbvrex2vw 3241 . . . . . . . . . . . 12 (∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ∃𝑢𝑆𝑣𝑆 ¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → 𝑢 = 𝑣))
428427biimpi 216 . . . . . . . . . . 11 (∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦) → ∃𝑢𝑆𝑣𝑆 ¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → 𝑢 = 𝑣))
429428adantl 481 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) → ∃𝑢𝑆𝑣𝑆 ¬ (((𝐻𝑆)‘𝑢) = ((𝐻𝑆)‘𝑣) → 𝑢 = 𝑣))
430417, 429r19.29vva 3215 . . . . . . . . 9 ((𝜑 ∧ ∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆)))
431430ex 412 . . . . . . . 8 (𝜑 → (∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))))
432 rexnal2 3134 . . . . . . . . . 10 (∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦))
433432a1i 11 . . . . . . . . 9 (𝜑 → (∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)))
434433imbi1d 341 . . . . . . . 8 (𝜑 → ((∃𝑥𝑆𝑦𝑆 ¬ (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))) ↔ (¬ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆)))))
435431, 434mpbid 232 . . . . . . 7 (𝜑 → (¬ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))))
436239, 435jaod 859 . . . . . 6 (𝜑 → ((¬ (𝐻𝑆):𝑆⟶(𝐻𝑆) ∨ ¬ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))))
437 ianor 983 . . . . . . . . 9 (¬ ((𝐻𝑆):𝑆⟶(𝐻𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻𝑆):𝑆⟶(𝐻𝑆) ∨ ¬ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)))
438437a1i 11 . . . . . . . 8 (𝜑 → (¬ ((𝐻𝑆):𝑆⟶(𝐻𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻𝑆):𝑆⟶(𝐻𝑆) ∨ ¬ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦))))
439438biimpd 229 . . . . . . 7 (𝜑 → (¬ ((𝐻𝑆):𝑆⟶(𝐻𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) → (¬ (𝐻𝑆):𝑆⟶(𝐻𝑆) ∨ ¬ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦))))
440439imim1d 82 . . . . . 6 (𝜑 → (((¬ (𝐻𝑆):𝑆⟶(𝐻𝑆) ∨ ¬ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))) → (¬ ((𝐻𝑆):𝑆⟶(𝐻𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆)))))
441436, 440mpd 15 . . . . 5 (𝜑 → (¬ ((𝐻𝑆):𝑆⟶(𝐻𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))))
442 dff13 7276 . . . . . . . . 9 ((𝐻𝑆):𝑆1-1→(𝐻𝑆) ↔ ((𝐻𝑆):𝑆⟶(𝐻𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)))
443442a1i 11 . . . . . . . 8 (𝜑 → ((𝐻𝑆):𝑆1-1→(𝐻𝑆) ↔ ((𝐻𝑆):𝑆⟶(𝐻𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦))))
444443notbid 318 . . . . . . 7 (𝜑 → (¬ (𝐻𝑆):𝑆1-1→(𝐻𝑆) ↔ ¬ ((𝐻𝑆):𝑆⟶(𝐻𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦))))
445444biimpd 229 . . . . . 6 (𝜑 → (¬ (𝐻𝑆):𝑆1-1→(𝐻𝑆) → ¬ ((𝐻𝑆):𝑆⟶(𝐻𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦))))
446445imim1d 82 . . . . 5 (𝜑 → ((¬ ((𝐻𝑆):𝑆⟶(𝐻𝑆) ∧ ∀𝑥𝑆𝑦𝑆 (((𝐻𝑆)‘𝑥) = ((𝐻𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))) → (¬ (𝐻𝑆):𝑆1-1→(𝐻𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆)))))
447441, 446mpd 15 . . . 4 (𝜑 → (¬ (𝐻𝑆):𝑆1-1→(𝐻𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆))))
448447imp 406 . . 3 ((𝜑 ∧ ¬ (𝐻𝑆):𝑆1-1→(𝐻𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆)))
449182, 448pm2.61dan 812 . 2 (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻𝑆)))
450 hashss 14449 . . 3 (((𝐻 “ (ℕ0m (0...𝐴))) ∈ V ∧ (𝐻𝑆) ⊆ (𝐻 “ (ℕ0m (0...𝐴)))) → (♯‘(𝐻𝑆)) ≤ (♯‘(𝐻 “ (ℕ0m (0...𝐴)))))
451124, 142, 450syl2anc 584 . 2 (𝜑 → (♯‘(𝐻𝑆)) ≤ (♯‘(𝐻 “ (ℕ0m (0...𝐴)))))
452119, 147, 151, 449, 451xrletrd 13205 1 (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ0m (0...𝐴)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1539  wcel 2107  wne 2939  wral 3060  wrex 3069  {crab 3435  Vcvv 3479  wss 3950  c0 4332  ifcif 4524  {csn 4625   class class class wbr 5142  {copab 5204  cmpt 5224   × cxp 5682  ccnv 5683  ran crn 5685  cres 5686  cima 5687   Fn wfn 6555  wf 6556  1-1wf1 6557  cfv 6560  (class class class)co 7432  cmpo 7434  m cmap 8867  Fincfn 8986  cr 11155  0cc0 11156  1c1 11157   + caddc 11159   · cmul 11161  *cxr 11295   < clt 11296  cle 11297  cmin 11493   / cdiv 11921  cn 12267  0cn0 12528  0*cxnn0 12601  cz 12615  cuz 12879  ...cfz 13548  cexp 14103  Ccbc 14342  chash 14370  Σcsu 15723  cdvds 16291   gcd cgcd 16532  cprime 16709  Basecbs 17248  +gcplusg 17298  0gc0g 17485   Σg cgsu 17486  Grpcgrp 18952  -gcsg 18954  .gcmg 19086  CMndccmn 19799  mulGrpcmgp 20138  Ringcrg 20231  CRingccrg 20232   RingHom crh 20470   RingIso crs 20471  IDomncidom 20694  Fieldcfield 20731  ringczring 21458  ℤRHomczrh 21511  chrcchr 21513  ℤ/nczn 21514  algSccascl 21873  var1cv1 22178  Poly1cpl1 22179  eval1ce1 22319  deg1cdg1 26094   PrimRoots cprimroots 42093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-inf2 9682  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234  ax-addf 11235  ax-mulf 11236
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-iin 4993  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-of 7698  df-ofr 7699  df-om 7889  df-1st 8015  df-2nd 8016  df-supp 8187  df-tpos 8252  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-oadd 8511  df-er 8746  df-ec 8748  df-qs 8752  df-map 8869  df-pm 8870  df-ixp 8939  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-fsupp 9403  df-sup 9483  df-inf 9484  df-oi 9551  df-dju 9942  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12529  df-xnn0 12602  df-z 12616  df-dec 12736  df-uz 12880  df-rp 13036  df-ico 13394  df-fz 13549  df-fzo 13696  df-fl 13833  df-mod 13911  df-seq 14044  df-exp 14104  df-fac 14314  df-bc 14343  df-hash 14371  df-cj 15139  df-re 15140  df-im 15141  df-sqrt 15275  df-abs 15276  df-clim 15525  df-sum 15724  df-dvds 16292  df-gcd 16533  df-prm 16710  df-phi 16804  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17249  df-ress 17276  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-hom 17322  df-cco 17323  df-0g 17487  df-gsum 17488  df-prds 17493  df-pws 17495  df-imas 17554  df-qus 17555  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18654  df-sgrp 18733  df-mnd 18749  df-mhm 18797  df-submnd 18798  df-grp 18955  df-minusg 18956  df-sbg 18957  df-mulg 19087  df-subg 19142  df-nsg 19143  df-eqg 19144  df-ghm 19232  df-cntz 19336  df-od 19547  df-cmn 19801  df-abl 19802  df-mgp 20139  df-rng 20151  df-ur 20180  df-srg 20185  df-ring 20233  df-cring 20234  df-oppr 20335  df-dvdsr 20358  df-unit 20359  df-invr 20389  df-dvr 20402  df-rhm 20473  df-rim 20474  df-nzr 20514  df-subrng 20547  df-subrg 20571  df-rlreg 20695  df-domn 20696  df-idom 20697  df-drng 20732  df-field 20733  df-lmod 20861  df-lss 20931  df-lsp 20971  df-sra 21173  df-rgmod 21174  df-lidl 21219  df-rsp 21220  df-2idl 21261  df-cnfld 21366  df-zring 21459  df-zrh 21515  df-chr 21517  df-zn 21518  df-assa 21874  df-asp 21875  df-ascl 21876  df-psr 21930  df-mvr 21931  df-mpl 21932  df-opsr 21934  df-evls 22099  df-evl 22100  df-psr1 22182  df-vr1 22183  df-ply1 22184  df-coe1 22185  df-evl1 22321  df-mdeg 26095  df-deg1 26096  df-mon1 26171  df-uc1p 26172  df-q1p 26173  df-r1p 26174  df-primroots 42094
This theorem is referenced by:  aks6d1c6lem4  42175
  Copyright terms: Public domain W3C validator