aks6d1c6lem3 - Mathbox for metakunt

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

Theorem aks6d1c6lem3 42154

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‘(Poly₁‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘𝑓)‘𝑦)) = (((eval₁‘𝐾)‘𝑓)‘(𝑒(._g‘(mulGrp‘𝐾))𝑦)))}
aks6d1c6.2	⊢ 𝑃 = (chr‘𝐾)
aks6d1c6.3	⊢ (𝜑 → 𝐾 ∈ Field)
aks6d1c6.4	⊢ (𝜑 → 𝑃 ∈ ℙ)
aks6d1c6.5	⊢ (𝜑 → 𝑅 ∈ ℕ)
aks6d1c6.6	⊢ (𝜑 → 𝑁 ∈ ℕ)
aks6d1c6.7	⊢ (𝜑 → 𝑃 ∥ 𝑁)
aks6d1c6.8	⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)
aks6d1c6.9	⊢ (𝜑 → 𝐴 < 𝑃)
aks6d1c6.10	⊢ 𝐺 = (𝑔 ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ ((mulGrp‘(Poly₁‘𝐾)) Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(._g‘(mulGrp‘(Poly₁‘𝐾)))((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
aks6d1c6.11	⊢ (𝜑 → 𝐴 ∈ ℕ₀)
aks6d1c6.12	⊢ 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)))
aks6d1c6.13	⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))
aks6d1c6.14	⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
aks6d1c6.15	⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
aks6d1c6.16	⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
aks6d1c6.17	⊢ 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀))
aks6d1c6.18	⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))
aks6d1c6.19	⊢ 𝑆 = {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)}
aks6d1c6lem3.1	⊢ 𝐽 = (𝑗 ∈ (ℕ₀ × ℕ₀) ↦ ((𝐸‘𝑗)(._g‘(mulGrp‘𝐾))𝑀))
aks6d1c6lem3.2	⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ≤ (♯‘(𝐽 “ (ℕ₀ × ℕ₀))))

**Assertion**
Ref	Expression
aks6d1c6lem3	⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))

Distinct variable groups: 𝐴,𝑔,𝑖 𝐴,ℎ,𝑗 𝐴,𝑠,𝑡 𝐷,𝑠 𝑥,𝐸,𝑦 𝑔,𝐺,𝑖 ℎ,𝐺 𝑡,𝐺,𝑖 𝑔,𝐻,𝑖,𝑥,𝑦 𝑗,𝐻 𝑡,𝐻,𝑥,𝑦 𝑔,𝐾,𝑖 ℎ,𝐾,𝑗 𝑡,𝐾 ℎ,𝑀 𝑘,𝑁,𝑙 𝑃,𝑘,𝑙 𝑆,𝑔,𝑖,𝑥,𝑦 𝑆,ℎ,𝑗 𝑡,𝑆 𝜑,𝑔,𝑖,𝑥,𝑦 𝜑,ℎ,𝑗 𝜑,𝑘,𝑥,𝑦,𝑙 𝜑,𝑠,𝑡 ∼ ,𝑎 𝐴,𝑎 𝑥,𝐴 𝑒,𝐸,𝑓,𝑦 𝑗,𝐸 𝑒,𝐺,𝑓,𝑦 𝐻,𝑎 ℎ,𝐻 𝐻,𝑠 𝐾,𝑎 𝑒,𝐾,𝑓,𝑦 𝑥,𝐾 𝑗,𝑀 𝑦,𝑀 𝑁,𝑎 𝑒,𝑁,𝑓 𝑁,𝑠,𝑘,𝑙 𝑥,𝑁 𝑃,𝑒,𝑓 𝑃,𝑠 𝑥,𝑃 𝑅,𝑒,𝑓,𝑦 𝑥,𝑅 𝑆,𝑎 𝑆,𝑠 𝜑,𝑎 Allowed substitution hints: 𝜑(𝑒,𝑓) 𝐴(𝑦,𝑒,𝑓,𝑘,𝑙) 𝐷(𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,ℎ,𝑖,𝑗,𝑘,𝑎,𝑙) 𝑃(𝑦,𝑡,𝑔,ℎ,𝑖,𝑗,𝑎) ∼ (𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,ℎ,𝑖,𝑗,𝑘,𝑠,𝑙) 𝑅(𝑡,𝑔,ℎ,𝑖,𝑗,𝑘,𝑠,𝑎,𝑙) 𝑆(𝑒,𝑓,𝑘,𝑙) 𝐸(𝑡,𝑔,ℎ,𝑖,𝑘,𝑠,𝑎,𝑙) 𝐺(𝑥,𝑗,𝑘,𝑠,𝑎,𝑙) 𝐻(𝑒,𝑓,𝑘,𝑙) 𝐽(𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,ℎ,𝑖,𝑗,𝑘,𝑠,𝑎,𝑙) 𝐾(𝑘,𝑠,𝑙) 𝐿(𝑥,𝑦,𝑡,𝑒,𝑓,𝑔,ℎ,𝑖,𝑗,𝑘,𝑠,𝑎,𝑙) 𝑀(𝑥,𝑡,𝑒,𝑓,𝑔,𝑖,𝑘,𝑠,𝑎,𝑙) 𝑁(𝑦,𝑡,𝑔,ℎ,𝑖,𝑗)

Proof of Theorem aks6d1c6lem3 Dummy variables 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		aks6d1c6.18	. . . . . . . . . . . 12 ⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))))
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 ⊢ 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)))
8		aks6d1c6.13	. . . . . . . . . . . . 13 ⊢ 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))
9		eqid 2735	. . . . . . . . . . . . 13 ⊢ (ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅)
10	2, 3, 4, 5, 6, 7, 8, 9	hashscontpowcl 42102	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ∈ ℕ₀)
11	1, 10	eqeltrid 2843	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ₀)
12	11	nn0zd 12637	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℤ)
13	12	zcnd 12721	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℂ)
14		1cnd 11254	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
15		aks6d1c6.11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
16	15	nn0cnd 12587	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
17	13, 14, 16	nppcan3d 11645	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = (𝐷 + 𝐴))
18	17	eqcomd 2741	. . . . . . 7 ⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (𝐴 + 1)))
19		hashfz0 14468	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℕ₀ → (♯‘(0...𝐴)) = (𝐴 + 1))
20	15, 19	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) = (𝐴 + 1))
21	20	eqcomd 2741	. . . . . . . 8 ⊢ (𝜑 → (𝐴 + 1) = (♯‘(0...𝐴)))
22	21	oveq2d 7447	. . . . . . 7 ⊢ (𝜑 → ((𝐷 − 1) + (𝐴 + 1)) = ((𝐷 − 1) + (♯‘(0...𝐴))))
23	18, 22	eqtrd 2775	. . . . . 6 ⊢ (𝜑 → (𝐷 + 𝐴) = ((𝐷 − 1) + (♯‘(0...𝐴))))
24		1zzd 12646	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
25	12, 24	zsubcld 12725	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 − 1) ∈ ℤ)
26		0p1e1 12386	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
27	26	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (0 + 1) = 1)
28		fvexd 6922	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤRHom‘(ℤ/nℤ‘𝑅)) ∈ V)
29	8, 28	eqeltrid 2843	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ V)
30	29	imaexd 7939	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V)
31	15	ne0d 4348	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℕ₀ ≠ ∅)
32	31, 31	jca 511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℕ₀ ≠ ∅ ∧ ℕ₀ ≠ ∅))
33		xpnz 6181	. . . . . . . . . . . . . . 15 ⊢ ((ℕ₀ ≠ ∅ ∧ ℕ₀ ≠ ∅) ↔ (ℕ₀ × ℕ₀) ≠ ∅)
34	32, 33	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℕ₀ × ℕ₀) ≠ ∅)
35		ovexd 7466	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ 𝑙 ∈ ℕ₀) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
36	35	ralrimiva 3144	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
37	36	ralrimiva 3144	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑘 ∈ ℕ₀ ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V)
38	7	fnmpo 8093	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ ℕ₀ ∀𝑙 ∈ ℕ₀ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) ∈ V → 𝐸 Fn (ℕ₀ × ℕ₀))
39	37, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 Fn (ℕ₀ × ℕ₀))
40		ssidd 4019	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℕ₀ × ℕ₀) ⊆ (ℕ₀ × ℕ₀))
41		fnimaeq0 6702	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸 Fn (ℕ₀ × ℕ₀) ∧ (ℕ₀ × ℕ₀) ⊆ (ℕ₀ × ℕ₀)) → ((𝐸 “ (ℕ₀ × ℕ₀)) = ∅ ↔ (ℕ₀ × ℕ₀) = ∅))
42	39, 40, 41	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) = ∅ ↔ (ℕ₀ × ℕ₀) = ∅))
43	42	necon3bid 2983	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅ ↔ (ℕ₀ × ℕ₀) ≠ ∅))
44	34, 43	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅)
45	5	nnnn0d 12585	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
46	9	zncrng 21581	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ ℕ₀ → (ℤ/nℤ‘𝑅) ∈ CRing)
47	45, 46	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℤ/nℤ‘𝑅) ∈ CRing)
48		crngring 20263	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑅) ∈ CRing → (ℤ/nℤ‘𝑅) ∈ Ring)
49	8	zrhrhm 21540	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom (ℤ/nℤ‘𝑅)))
50		zringbas 21482	. . . . . . . . . . . . . . . . . 18 ⊢ ℤ = (Base‘ℤ_ring)
51		eqid 2735	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(ℤ/nℤ‘𝑅)) = (Base‘(ℤ/nℤ‘𝑅))
52	50, 51	rhmf 20502	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ∈ (ℤ_ring RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
53	47, 48, 49, 52	4syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
54	53	ffnd 6738	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐿 Fn ℤ)
55	7	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝐸 = (𝑘 ∈ ℕ₀, 𝑙 ∈ ℕ₀ ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))))
56		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑘 = 𝑥)
57	56	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → (𝑃↑𝑘) = (𝑃↑𝑥))
58		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → 𝑙 = 𝑦)
59	58	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑁 / 𝑃)↑𝑙) = ((𝑁 / 𝑃)↑𝑦))
60	57, 59	oveq12d 7449	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) ∧ (𝑘 = 𝑥 ∧ 𝑙 = 𝑦)) → ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙)) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)))
61		simplr 769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑥 ∈ ℕ₀)
62		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑦 ∈ ℕ₀)
63		ovexd 7466	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ V)
64	55, 60, 61, 62, 63	ovmpod 7585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑥𝐸𝑦) = ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)))
65	3	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℙ)
66		prmnn 16708	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
67	65, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℕ)
68	67	nnzd 12638	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∈ ℤ)
69	68, 61	zexpcld 14125	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑃↑𝑥) ∈ ℤ)
70	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ∥ 𝑁)
71	67	nnne0d 12314	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑃 ≠ 0)
72	2	nnzd 12638	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ∈ ℤ)
73	72	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → 𝑁 ∈ ℤ)
74	73	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → 𝑁 ∈ ℤ)
75		dvdsval2 16290	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
76	68, 71, 74, 75	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑃 ∥ 𝑁 ↔ (𝑁 / 𝑃) ∈ ℤ))
77	70, 76	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑁 / 𝑃) ∈ ℤ)
78	77, 62	zexpcld 14125	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑁 / 𝑃)↑𝑦) ∈ ℤ)
79	69, 78	zmulcld 12726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → ((𝑃↑𝑥) · ((𝑁 / 𝑃)↑𝑦)) ∈ ℤ)
80	64, 79	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ₀) ∧ 𝑦 ∈ ℕ₀) → (𝑥𝐸𝑦) ∈ ℤ)
81	80	ralrimiva 3144	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ₀) → ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ)
82	81	ralrimiva 3144	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ)
83	39, 82	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 Fn (ℕ₀ × ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ))
84		ffnov 7559	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸:(ℕ₀ × ℕ₀)⟶ℤ ↔ (𝐸 Fn (ℕ₀ × ℕ₀) ∧ ∀𝑥 ∈ ℕ₀ ∀𝑦 ∈ ℕ₀ (𝑥𝐸𝑦) ∈ ℤ))
85	83, 84	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸:(ℕ₀ × ℕ₀)⟶ℤ)
86		frn 6744	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸:(ℕ₀ × ℕ₀)⟶ℤ → ran 𝐸 ⊆ ℤ)
87	85, 86	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝐸 ⊆ ℤ)
88		fnima 6699	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 Fn (ℕ₀ × ℕ₀) → (𝐸 “ (ℕ₀ × ℕ₀)) = ran 𝐸)
89	39, 88	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) = ran 𝐸)
90	89	sseq1d 4027	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ ↔ ran 𝐸 ⊆ ℤ))
91	87, 90	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ)
92		fnimaeq0 6702	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 Fn ℤ ∧ (𝐸 “ (ℕ₀ × ℕ₀)) ⊆ ℤ) → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) = ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) = ∅))
93	54, 91, 92	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) = ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) = ∅))
94	93	necon3bid 2983	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅ ↔ (𝐸 “ (ℕ₀ × ℕ₀)) ≠ ∅))
95	44, 94	mpbird 257	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅)
96		hashge1 14425	. . . . . . . . . . . . 13 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → 1 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))))
97	1	eqcomi 2744	. . . . . . . . . . . . . 14 ⊢ (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) = 𝐷
98	97	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) = 𝐷)
99	96, 98	breqtrd 5174	. . . . . . . . . . . 12 ⊢ (((𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ∈ V ∧ (𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀))) ≠ ∅) → 1 ≤ 𝐷)
100	30, 95, 99	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ≤ 𝐷)
101	27, 100	eqbrtrd 5170	. . . . . . . . . 10 ⊢ (𝜑 → (0 + 1) ≤ 𝐷)
102		0red 11262	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℝ)
103		1red 11260	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
104	11	nn0red 12586	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
105		leaddsub 11737	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
106	102, 103, 104, 105	syl3anc 1370	. . . . . . . . . 10 ⊢ (𝜑 → ((0 + 1) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1)))
107	101, 106	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝐷 − 1))
108	25, 107	jca 511	. . . . . . . 8 ⊢ (𝜑 → ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
109		elnn0z 12624	. . . . . . . 8 ⊢ ((𝐷 − 1) ∈ ℕ₀ ↔ ((𝐷 − 1) ∈ ℤ ∧ 0 ≤ (𝐷 − 1)))
110	108, 109	sylibr 234	. . . . . . 7 ⊢ (𝜑 → (𝐷 − 1) ∈ ℕ₀)
111		fzfid 14011	. . . . . . . 8 ⊢ (𝜑 → (0...𝐴) ∈ Fin)
112		hashcl 14392	. . . . . . . 8 ⊢ ((0...𝐴) ∈ Fin → (♯‘(0...𝐴)) ∈ ℕ₀)
113	111, 112	syl 17	. . . . . . 7 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℕ₀)
114	110, 113	nn0addcld 12589	. . . . . 6 ⊢ (𝜑 → ((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ₀)
115	23, 114	eqeltrd 2839	. . . . 5 ⊢ (𝜑 → (𝐷 + 𝐴) ∈ ℕ₀)
116		bccl 14358	. . . . 5 ⊢ (((𝐷 + 𝐴) ∈ ℕ₀ ∧ (𝐷 − 1) ∈ ℤ) → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ₀)
117	115, 25, 116	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℕ₀)
118	117	nn0red 12586	. . 3 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ)
119	118	rexrd 11309	. 2 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ∈ ℝ^*)
120		aks6d1c6.17	. . . . . . 7 ⊢ 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀))
121		ovexd 7466	. . . . . . . 8 ⊢ (𝜑 → (ℕ₀ ↑_m (0...𝐴)) ∈ V)
122	121	mptexd 7244	. . . . . . 7 ⊢ (𝜑 → (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V)
123	120, 122	eqeltrid 2843	. . . . . 6 ⊢ (𝜑 → 𝐻 ∈ V)
124	123	imaexd 7939	. . . . 5 ⊢ (𝜑 → (𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V)
125		simprl 771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))) → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)))
126	125	ex 412	. . . . . . . . 9 ⊢ (𝜑 → ((𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)) → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴))))
127		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = 𝑤 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑤)
128	127	fveq1d 6909	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑤 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑤‘𝑡))
129	128	sumeq2dv 15735	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑤 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡))
130	129	breq1d 5158	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑤 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)))
131	130	elrab 3695	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)))
132	131	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))))
133	132	biimpd 229	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → (𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1))))
134	133	imim1d 82	. . . . . . . . 9 ⊢ (𝜑 → (((𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑤‘𝑡) ≤ (𝐷 − 1)) → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴))) → (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴)))))
135	126, 134	mpd 15	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑤 ∈ (ℕ₀ ↑_m (0...𝐴))))
136	135	ssrdv 4001	. . . . . . 7 ⊢ (𝜑 → {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴)))
137		aks6d1c6.19	. . . . . . . . 9 ⊢ 𝑆 = {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)}
138	137	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑆 = {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
139	138	sseq1d 4027	. . . . . . 7 ⊢ (𝜑 → (𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)) ↔ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴))))
140	136, 139	mpbird 257	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)))
141		imass2 6123	. . . . . 6 ⊢ (𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)) → (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴))))
142	140, 141	syl 17	. . . . 5 ⊢ (𝜑 → (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴))))
143	124, 142	ssexd 5330	. . . 4 ⊢ (𝜑 → (𝐻 “ 𝑆) ∈ V)
144		hashxnn0 14375	. . . 4 ⊢ ((𝐻 “ 𝑆) ∈ V → (♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^*)
145	143, 144	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^*)
146		xnn0xr 12602	. . 3 ⊢ ((♯‘(𝐻 “ 𝑆)) ∈ ℕ₀^* → (♯‘(𝐻 “ 𝑆)) ∈ ℝ^*)
147	145, 146	syl 17	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ∈ ℝ^*)
148		hashxnn0 14375	. . . 4 ⊢ ((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^*)
149	124, 148	syl 17	. . 3 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^*)
150		xnn0xr 12602	. . 3 ⊢ ((♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℕ₀^* → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℝ^*)
151	149, 150	syl 17	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) ∈ ℝ^*)
152	110	nn0cnd 12587	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 − 1) ∈ ℂ)
153	113	nn0cnd 12587	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℂ)
154	152, 153	pncand 11619	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))) = (𝐷 − 1))
155	154	eqcomd 2741	. . . . . . 7 ⊢ (𝜑 → (𝐷 − 1) = (((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴))))
156	23, 155	oveq12d 7449	. . . . . 6 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
157	15	nn0ge0d 12588	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 𝐴)
158		0zd 12623	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℤ)
159	15	nn0zd 12637	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℤ)
160		eluz 12890	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ (ℤ_≥‘0) ↔ 0 ≤ 𝐴))
161	158, 159, 160	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ (ℤ_≥‘0) ↔ 0 ≤ 𝐴))
162	157, 161	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (ℤ_≥‘0))
163		fzn0 13575	. . . . . . . . . 10 ⊢ ((0...𝐴) ≠ ∅ ↔ 𝐴 ∈ (ℤ_≥‘0))
164	162, 163	sylibr 234	. . . . . . . . 9 ⊢ (𝜑 → (0...𝐴) ≠ ∅)
165	110, 111, 164, 137	sticksstones23 42151	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))))
166	113	nn0zd 12637	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(0...𝐴)) ∈ ℤ)
167		bccmpl 14345	. . . . . . . . 9 ⊢ ((((𝐷 − 1) + (♯‘(0...𝐴))) ∈ ℕ₀ ∧ (♯‘(0...𝐴)) ∈ ℤ) → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
168	114, 166, 167	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(♯‘(0...𝐴))) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
169	165, 168	eqtrd 2775	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑆) = (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))))
170	169	eqcomd 2741	. . . . . 6 ⊢ (𝜑 → (((𝐷 − 1) + (♯‘(0...𝐴)))C(((𝐷 − 1) + (♯‘(0...𝐴))) − (♯‘(0...𝐴)))) = (♯‘𝑆))
171	156, 170	eqtrd 2775	. . . . 5 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
172	171	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) = (♯‘𝑆))
173	120	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)))
174		ovexd 7466	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℕ₀ ↑_m (0...𝐴)) ∈ V)
175	174	mptexd 7244	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)) ∈ V)
176	173, 175	eqeltrd 2839	. . . . . 6 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → 𝐻 ∈ V)
177	176	resexd 6048	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆) ∈ V)
178	176	imaexd 7939	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 “ 𝑆) ∈ V)
179		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆))
180		hashf1dmcdm 14480	. . . . 5 ⊢ (((𝐻 ↾ 𝑆) ∈ V ∧ (𝐻 “ 𝑆) ∈ V ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆)))
181	177, 178, 179, 180	syl3anc 1370	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → (♯‘𝑆) ≤ (♯‘(𝐻 “ 𝑆)))
182	172, 181	eqbrtrd 5170	. . 3 ⊢ ((𝜑 ∧ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
183	120	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐻 = (ℎ ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀)))
184		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ℎ = 𝑗)
185	184	fveq2d 6911	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (𝐺‘ℎ) = (𝐺‘𝑗))
186	185	fveq2d 6911	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → ((eval₁‘𝐾)‘(𝐺‘ℎ)) = ((eval₁‘𝐾)‘(𝐺‘𝑗)))
187	186	fveq1d 6909	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ ℎ = 𝑗) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) = (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀))
188		simp2 1136	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)) → 𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)))
189	188	rabssdv 4085	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ⊆ (ℕ₀ ↑_m (0...𝐴)))
190	137, 189	eqsstrid 4044	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 ⊆ (ℕ₀ ↑_m (0...𝐴)))
191	190	sselda 3995	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ (ℕ₀ ↑_m (0...𝐴)))
192		fvexd 6922	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ V)
193	183, 187, 191, 192	fvmptd 7023	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) = (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀))
194		eqid 2735	. . . . . . . . . . . . . . . 16 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
195		eqid 2735	. . . . . . . . . . . . . . . 16 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
196		eqid 2735	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐾) = (Base‘𝐾)
197		eqid 2735	. . . . . . . . . . . . . . . 16 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
198		aks6d1c6.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ Field)
199	198	fldcrngd 20759	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ CRing)
200	199	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐾 ∈ CRing)
201		aks6d1c6.16	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
202		eqid 2735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
203	202	crngmgp 20259	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐾 ∈ CRing → (mulGrp‘𝐾) ∈ CMnd)
204	199, 203	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd)
205		eqid 2735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (._g‘(mulGrp‘𝐾)) = (._g‘(mulGrp‘𝐾))
206	204, 45, 205	isprimroot 42075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) ↔ (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣))))
207	206	biimpd 229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣))))
208	201, 207	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) ∧ ∀𝑣 ∈ ℕ₀ ((𝑣(._g‘(mulGrp‘𝐾))𝑀) = (0_g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑣)))
209	208	simp1d 1141	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (Base‘(mulGrp‘𝐾)))
210	202, 196	mgpbas 20158	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
211	210	eqcomi 2744	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(mulGrp‘𝐾)) = (Base‘𝐾)
212	209, 211	eleqtrdi 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾))
213	212	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑀 ∈ (Base‘𝐾))
214		aks6d1c6.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑃 = (chr‘𝐾)
215		aks6d1c6.9	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < 𝑃)
216		eqid 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ (var₁‘𝐾) = (var₁‘𝐾)
217		eqid 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ (._g‘(mulGrp‘(Poly₁‘𝐾))) = (._g‘(mulGrp‘(Poly₁‘𝐾)))
218		aks6d1c6.10	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺 = (𝑔 ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ ((mulGrp‘(Poly₁‘𝐾)) Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(._g‘(mulGrp‘(Poly₁‘𝐾)))((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
219	198, 3, 214, 15, 215, 216, 217, 218	aks6d1c5lem0 42117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
220	219	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
221	220, 191	ffvelcdmd 7105	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺‘𝑗) ∈ (Base‘(Poly₁‘𝐾)))
222	194, 195, 196, 197, 200, 213, 221	fveval1fvcl 22353	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((eval₁‘𝐾)‘(𝐺‘𝑗))‘𝑀) ∈ (Base‘𝐾))
223	193, 222	eqeltrd 2839	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐻‘𝑗) ∈ (Base‘𝐾))
224		eqid 2735	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗))
225	223, 224	fmptd 7134	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾))
226		fvexd 6922	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ℎ ∈ (ℕ₀ ↑_m (0...𝐴))) → (((eval₁‘𝐾)‘(𝐺‘ℎ))‘𝑀) ∈ V)
227	226, 120	fmptd 7134	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:(ℕ₀ ↑_m (0...𝐴))⟶V)
228	227, 190	feqresmpt 6978	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻 ↾ 𝑆) = (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)))
229	228	feq1d 6721	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) ↔ (𝑗 ∈ 𝑆 ↦ (𝐻‘𝑗)):𝑆⟶(Base‘𝐾)))
230	225, 229	mpbird 257	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾))
231		ffrn 6750	. . . . . . . . . . . 12 ⊢ ((𝐻 ↾ 𝑆):𝑆⟶(Base‘𝐾) → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆))
232	230, 231	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆))
233		df-ima 5702	. . . . . . . . . . . . 13 ⊢ (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆)
234	233	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻 “ 𝑆) = ran (𝐻 ↾ 𝑆))
235	234	feq3d 6724	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ↔ (𝐻 ↾ 𝑆):𝑆⟶ran (𝐻 ↾ 𝑆)))
236	232, 235	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆))
237	236	notnotd 144	. . . . . . . . 9 ⊢ (𝜑 → ¬ ¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆))
238	237	a1d 25	. . . . . . . 8 ⊢ (𝜑 → (¬ ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)) → ¬ ¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆)))
239	238	con4d 115	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
240		df-an 396	. . . . . . . . . . . . . 14 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣))
241	240	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣)))
242		eqid 2735	. . . . . . . . . . . . . . . 16 ⊢ (deg₁‘𝐾) = (deg₁‘𝐾)
243		eqid 2735	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
244		eqid 2735	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘(Poly₁‘𝐾)) = (0_g‘(Poly₁‘𝐾))
245		fldidom 20788	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn)
246	198, 245	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ IDomn)
247	246	ad4antr 732	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ IDomn)
248	195	ply1crng 22216	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ CRing → (Poly₁‘𝐾) ∈ CRing)
249		crngring 20263	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Poly₁‘𝐾) ∈ CRing → (Poly₁‘𝐾) ∈ Ring)
250		ringgrp 20256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Poly₁‘𝐾) ∈ Ring → (Poly₁‘𝐾) ∈ Grp)
251	199, 248, 249, 250	4syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Poly₁‘𝐾) ∈ Grp)
252	251	ad4antr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (Poly₁‘𝐾) ∈ Grp)
253	198, 3, 214, 15, 215, 216, 217, 218	aks6d1c5 42121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)))
254	253	ad4antr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)))
255		f1f 6805	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
256	254, 255	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐺:(ℕ₀ ↑_m (0...𝐴))⟶(Base‘(Poly₁‘𝐾)))
257	137	eleq2i 2831	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝑆 ↔ 𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
258		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑢)
259	258	fveq1d 6909	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 = 𝑢 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑢‘𝑡))
260	259	sumeq2dv 15735	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑢 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡))
261	260	breq1d 5158	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑢 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
262	261	elrab 3695	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
263	262	simplbi 497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
264	257, 263	sylbi 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
265	264	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
266	265	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
267	266	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
268	256, 267	ffvelcdmd 7105	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)))
269	137	eleq2i 2831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑆 ↔ 𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)})
270		elrabi 3690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
271	269, 270	sylbi 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
272	271	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
273	272	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
274	256, 273	ffvelcdmd 7105	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾)))
275		eqid 2735	. . . . . . . . . . . . . . . . . 18 ⊢ (-_g‘(Poly₁‘𝐾)) = (-_g‘(Poly₁‘𝐾))
276	197, 275	grpsubcl 19051	. . . . . . . . . . . . . . . . 17 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)))
277	252, 268, 274, 276	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)))
278		neqne 2946	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑢 = 𝑣 → 𝑢 ≠ 𝑣)
279	278	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → 𝑢 ≠ 𝑣)
280	279	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣)
281	267, 273	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴))))
282		f1fveq 7282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:(ℕ₀ ↑_m (0...𝐴))–1-1→(Base‘(Poly₁‘𝐾)) ∧ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣))
283	254, 281, 282	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢) = (𝐺‘𝑣) ↔ 𝑢 = 𝑣))
284	283	bicomd 223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 = 𝑣 ↔ (𝐺‘𝑢) = (𝐺‘𝑣)))
285	284	necon3bid 2983	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
286	285	biimpd 229	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑢 ≠ 𝑣 → (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
287	280, 286	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐺‘𝑢) ≠ (𝐺‘𝑣))
288	197, 244, 275	grpsubeq0 19057	. . . . . . . . . . . . . . . . . . 19 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) = (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) = (𝐺‘𝑣)))
289	288	necon3bid 2983	. . . . . . . . . . . . . . . . . 18 ⊢ (((Poly₁‘𝐾) ∈ Grp ∧ (𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) ∧ (𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
290	252, 268, 274, 289	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ (𝐺‘𝑢) ≠ (𝐺‘𝑣)))
291	287, 290	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)))
292	195, 197, 242, 194, 243, 244, 247, 277, 291	fta1g 26224	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))))
293	242, 195, 197	deg1xrcl 26136	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
294	277, 293	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
295	104	ad4antr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ)
296		1red 11260	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 1 ∈ ℝ)
297	295, 296	resubcld 11689	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ)
298	297	rexrd 11309	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) ∈ ℝ^*)
299		simp-4l 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝜑)
300		fvexd 6922	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
301		cnvexg 7947	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
302	300, 301	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
303	302	imaexd 7939	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V)
304		hashxnn0 14375	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℕ₀^*)
305		xnn0xr 12602	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℕ₀^* → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℝ^*)
306	299, 303, 304, 305	4syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℝ^*)
307	242, 195, 197	deg1xrcl 26136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺‘𝑣) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ∈ ℝ^*)
308	274, 307	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ∈ ℝ^*)
309	242, 195, 197	deg1xrcl 26136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺‘𝑢) ∈ (Base‘(Poly₁‘𝐾)) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ∈ ℝ^*)
310	268, 309	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ∈ ℝ^*)
311	308, 310	ifcld 4577	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ∈ ℝ^*)
312	247	idomringd 20745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Ring)
313	195, 242, 312, 197, 275, 268, 274	deg1suble 26161	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ≤ if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))))
314		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((deg₁‘𝐾)‘(𝐺‘𝑣)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))))
315	314	breq1d 5158	. . . . . . . . . . . . . . . . . . 19 ⊢ (((deg₁‘𝐾)‘(𝐺‘𝑣)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) → (((deg₁‘𝐾)‘(𝐺‘𝑣)) ≤ (𝐷 − 1) ↔ if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1)))
316		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((deg₁‘𝐾)‘(𝐺‘𝑢)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))))
317	316	breq1d 5158	. . . . . . . . . . . . . . . . . . 19 ⊢ (((deg₁‘𝐾)‘(𝐺‘𝑢)) = if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) → (((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ (𝐷 − 1) ↔ if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1)))
318		aks6d1c6.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly₁‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(._g‘(mulGrp‘𝐾))(((eval₁‘𝐾)‘𝑓)‘𝑦)) = (((eval₁‘𝐾)‘𝑓)‘(𝑒(._g‘(mulGrp‘𝐾))𝑦)))}
319	198	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field)
320	3	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ)
321	5	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ)
322	2	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ)
323	4	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁)
324	6	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1)
325	215	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃)
326	15	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈ ℕ₀)
327		aks6d1c6.14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
328	327	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
329		aks6d1c6.15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
330	329	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
331	201	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
332		simpllr 776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑣 ∈ 𝑆)
333	332, 271	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)))
334	318, 214, 319, 320, 321, 322, 323, 324, 325, 218, 326, 7, 8, 328, 330, 331, 120, 1, 137, 333	aks6d1c6lem1 42152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡))
335		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → 𝑠 = 𝑣)
336	335	fveq1d 6909	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 = 𝑣 ∧ 𝑡 ∈ (0...𝐴)) → (𝑠‘𝑡) = (𝑣‘𝑡))
337	336	sumeq2dv 15735	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑣 → Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) = Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡))
338	337	breq1d 5158	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑣 → (Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1) ↔ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
339	338	elrab 3695	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∈ {𝑠 ∈ (ℕ₀ ↑_m (0...𝐴)) ∣ Σ𝑡 ∈ (0...𝐴)(𝑠‘𝑡) ≤ (𝐷 − 1)} ↔ (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
340	269, 339	bitri 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ 𝑆 ↔ (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
341	332, 340	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑣 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1)))
342	341	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑣‘𝑡) ≤ (𝐷 − 1))
343	334, 342	eqbrtrd 5170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑣)) ≤ (𝐷 − 1))
344	198	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐾 ∈ Field)
345	3	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∈ ℙ)
346	5	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑅 ∈ ℕ)
347	2	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑁 ∈ ℕ)
348	4	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑃 ∥ 𝑁)
349	6	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑁 gcd 𝑅) = 1)
350	215	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 < 𝑃)
351	15	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝐴 ∈ ℕ₀)
352	327	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
353	329	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
354	201	ad5antr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
355	267	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)))
356	318, 214, 344, 345, 346, 347, 348, 349, 350, 218, 351, 7, 8, 352, 353, 354, 120, 1, 137, 355	aks6d1c6lem1 42152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) = Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡))
357		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → 𝑢 ∈ 𝑆)
358	257, 262	bitri 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ 𝑆 ↔ (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
359	357, 358	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → (𝑢 ∈ (ℕ₀ ↑_m (0...𝐴)) ∧ Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1)))
360	359	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → Σ𝑡 ∈ (0...𝐴)(𝑢‘𝑡) ≤ (𝐷 − 1))
361	356, 360	eqbrtrd 5170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) ∧ ¬ ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣))) → ((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ (𝐷 − 1))
362	315, 317, 343, 361	ifbothda 4569	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → if(((deg₁‘𝐾)‘(𝐺‘𝑢)) ≤ ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑣)), ((deg₁‘𝐾)‘(𝐺‘𝑢))) ≤ (𝐷 − 1))
363	294, 311, 298, 313, 362	xrletrd 13201	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ≤ (𝐷 − 1))
364	295	rexrd 11309	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ∈ ℝ^*)
365	295	ltm1d 12198	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < 𝐷)
366		simpllr 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆)
367		simplr 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆)
368	299, 366, 367	jca31 514	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆))
369		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣))
370	368, 369	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)))
371	198	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐾 ∈ Field)
372	3	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∈ ℙ)
373	5	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑅 ∈ ℕ)
374	2	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑁 ∈ ℕ)
375	4	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑃 ∥ 𝑁)
376	6	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑁 gcd 𝑅) = 1)
377	215	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 < 𝑃)
378	15	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐴 ∈ ℕ₀)
379	327	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼ ((var₁‘𝐾)(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
380	329	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(._g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
381	201	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
382		simpllr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ∈ 𝑆)
383		simplr 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑣 ∈ 𝑆)
384		simprl 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣))
385	279	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝑢 ≠ 𝑣)
386		aks6d1c6lem3.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 = (𝑗 ∈ (ℕ₀ × ℕ₀) ↦ ((𝐸‘𝑗)(._g‘(mulGrp‘𝐾))𝑀))
387		aks6d1c6lem3.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ≤ (♯‘(𝐽 “ (ℕ₀ × ℕ₀))))
388	387	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(𝐿 “ (𝐸 “ (ℕ₀ × ℕ₀)))) ≤ (♯‘(𝐽 “ (ℕ₀ × ℕ₀))))
389	318, 214, 371, 372, 373, 374, 375, 376, 377, 218, 378, 7, 8, 379, 380, 381, 120, 1, 137, 382, 383, 384, 385, 386, 388	aks6d1c6lem2 42153	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
390	370, 389	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → 𝐷 ≤ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
391	298, 364, 306, 365, 390	xrltletrd 13200	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (𝐷 − 1) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
392	294, 298, 306, 363, 391	xrlelttrd 13199	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})))
393	242, 195, 244, 197	deg1nn0clb 26144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ Ring ∧ ((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ∈ (Base‘(Poly₁‘𝐾))) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀))
394	312, 277, 393	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)) ≠ (0_g‘(Poly₁‘𝐾)) ↔ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀))
395	291, 394	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℕ₀)
396	395	nn0red 12586	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ)
397	396	rexrd 11309	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^*)
398		fvexd 6922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
399	398, 301	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ V)
400	399	imaexd 7939	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)}) ∈ V)
401	400, 304	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℕ₀^*)
402	401, 305	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℝ^*)
403		xrltnle 11326	. . . . . . . . . . . . . . . . 17 ⊢ ((((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) ∈ ℝ^* ∧ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ∈ ℝ^*) → (((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ↔ ¬ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)))))
404	397, 402, 403	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → (((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) < (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ↔ ¬ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣)))))
405	392, 404	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ¬ (♯‘(^◡((eval₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))) “ {(0_g‘𝐾)})) ≤ ((deg₁‘𝐾)‘((𝐺‘𝑢)(-_g‘(Poly₁‘𝐾))(𝐺‘𝑣))))
406	292, 405	pm2.21dd 195	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
407	406	ex 412	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) ∧ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
408	241, 407	sylbird 260	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
409		biidd 262	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (𝑢 = 𝑣 ↔ 𝑢 = 𝑣))
410	409	necon3abid 2975	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (𝑢 ≠ 𝑣 ↔ ¬ 𝑢 = 𝑣))
411	410	necon1bbid 2978	. . . . . . . . . . . . . . . 16 ⊢ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → (¬ ¬ 𝑢 = 𝑣 ↔ 𝑢 = 𝑣))
412	411	pm5.74i 271	. . . . . . . . . . . . . . 15 ⊢ ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
413	412	notbii 320	. . . . . . . . . . . . . 14 ⊢ (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
414	413	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
415	414	imbi1d 341	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → ((¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → ¬ ¬ 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) ↔ (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
416	408, 415	mpbid 232	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
417	416	imp 406	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ∧ 𝑢 ∈ 𝑆) ∧ 𝑣 ∈ 𝑆) ∧ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
418		fveqeq2 6916	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑢 → (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦)))
419		equequ1 2022	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑢 → (𝑥 = 𝑦 ↔ 𝑢 = 𝑦))
420	418, 419	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑢 → ((((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦)))
421	420	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑢 → (¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦)))
422		fveq2 6907	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑣 → ((𝐻 ↾ 𝑆)‘𝑦) = ((𝐻 ↾ 𝑆)‘𝑣))
423	422	eqeq2d 2746	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) ↔ ((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣)))
424		equequ2 2023	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑣 → (𝑢 = 𝑦 ↔ 𝑢 = 𝑣))
425	423, 424	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑣 → ((((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
426	425	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑣 → (¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑢 = 𝑦) ↔ ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣)))
427	421, 426	cbvrex2vw 3240	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
428	427	biimpi 216	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
429	428	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑢) = ((𝐻 ↾ 𝑆)‘𝑣) → 𝑢 = 𝑣))
430	417, 429	r19.29vva 3214	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
431	430	ex 412	. . . . . . . 8 ⊢ (𝜑 → (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
432		rexnal2 3133	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))
433	432	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
434	433	imbi1d 341	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ¬ (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) ↔ (¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
435	431, 434	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
436	239, 435	jaod 859	. . . . . 6 ⊢ (𝜑 → ((¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
437		ianor 983	. . . . . . . . 9 ⊢ (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
438	437	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
439	438	biimpd 229	. . . . . . 7 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → (¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
440	439	imim1d 82	. . . . . 6 ⊢ (𝜑 → (((¬ (𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∨ ¬ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
441	436, 440	mpd 15	. . . . 5 ⊢ (𝜑 → (¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
442		dff13 7275	. . . . . . . . 9 ⊢ ((𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)))
443	442	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
444	443	notbid 318	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) ↔ ¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
445	444	biimpd 229	. . . . . 6 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦))))
446	445	imim1d 82	. . . . 5 ⊢ (𝜑 → ((¬ ((𝐻 ↾ 𝑆):𝑆⟶(𝐻 “ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (((𝐻 ↾ 𝑆)‘𝑥) = ((𝐻 ↾ 𝑆)‘𝑦) → 𝑥 = 𝑦)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))) → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))))
447	441, 446	mpd 15	. . . 4 ⊢ (𝜑 → (¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆))))
448	447	imp 406	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐻 ↾ 𝑆):𝑆–1-1→(𝐻 “ 𝑆)) → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
449	182, 448	pm2.61dan 813	. 2 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ 𝑆)))
450		hashss 14445	. . 3 ⊢ (((𝐻 “ (ℕ₀ ↑_m (0...𝐴))) ∈ V ∧ (𝐻 “ 𝑆) ⊆ (𝐻 “ (ℕ₀ ↑_m (0...𝐴)))) → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))
451	124, 142, 450	syl2anc 584	. 2 ⊢ (𝜑 → (♯‘(𝐻 “ 𝑆)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))
452	119, 147, 151, 449, 451	xrletrd 13201	1 ⊢ (𝜑 → ((𝐷 + 𝐴)C(𝐷 − 1)) ≤ (♯‘(𝐻 “ (ℕ₀ ↑_m (0...𝐴)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 {crab 3433 Vcvv 3478 ⊆ wss 3963 ∅c0 4339 ifcif 4531 {csn 4631 class class class wbr 5148 {copab 5210 ↦ cmpt 5231 × cxp 5687 ^◡ccnv 5688 ran crn 5690 ↾ cres 5691 “ cima 5692 Fn wfn 6558 ⟶wf 6559 –1-1→wf1 6560 ‘cfv 6563 (class class class)co 7431 ∈ cmpo 7433 ↑_m cmap 8865 Fincfn 8984 ℝcr 11152 0cc0 11153 1c1 11154 + caddc 11156 · cmul 11158 ℝ^*cxr 11292 < clt 11293 ≤ cle 11294 − cmin 11490 / cdiv 11918 ℕcn 12264 ℕ₀cn0 12524 ℕ₀^*cxnn0 12597 ℤcz 12611 ℤ_≥cuz 12876 ...cfz 13544 ↑cexp 14099 Ccbc 14338 ♯chash 14366 Σcsu 15719 ∥ cdvds 16287 gcd cgcd 16528 ℙcprime 16705 Basecbs 17245 +_gcplusg 17298 0_gc0g 17486 Σ_g cgsu 17487 Grpcgrp 18964 -_gcsg 18966 ._gcmg 19098 CMndccmn 19813 mulGrpcmgp 20152 Ringcrg 20251 CRingccrg 20252 RingHom crh 20486 RingIso crs 20487 IDomncidom 20710 Fieldcfield 20747 ℤ_ringczring 21475 ℤRHomczrh 21528 chrcchr 21530 ℤ/nℤczn 21531 algSccascl 21890 var₁cv1 22193 Poly₁cpl1 22194 eval₁ce1 22334 deg₁cdg1 26108 PrimRoots cprimroots 42073

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-inf2 9679 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231 ax-addf 11232 ax-mulf 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-tp 4636 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-iin 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-se 5642 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-isom 6572 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-ofr 7698 df-om 7888 df-1st 8013 df-2nd 8014 df-supp 8185 df-tpos 8250 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-2o 8506 df-oadd 8509 df-er 8744 df-ec 8746 df-qs 8750 df-map 8867 df-pm 8868 df-ixp 8937 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-fsupp 9400 df-sup 9480 df-inf 9481 df-oi 9548 df-dju 9939 df-card 9977 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12525 df-xnn0 12598 df-z 12612 df-dec 12732 df-uz 12877 df-rp 13033 df-ico 13390 df-fz 13545 df-fzo 13692 df-fl 13829 df-mod 13907 df-seq 14040 df-exp 14100 df-fac 14310 df-bc 14339 df-hash 14367 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272 df-clim 15521 df-sum 15720 df-dvds 16288 df-gcd 16529 df-prm 16706 df-phi 16800 df-struct 17181 df-sets 17198 df-slot 17216 df-ndx 17228 df-base 17246 df-ress 17275 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 17488 df-gsum 17489 df-prds 17494 df-pws 17496 df-imas 17555 df-qus 17556 df-mre 17631 df-mrc 17632 df-acs 17634 df-mgm 18666 df-sgrp 18745 df-mnd 18761 df-mhm 18809 df-submnd 18810 df-grp 18967 df-minusg 18968 df-sbg 18969 df-mulg 19099 df-subg 19154 df-nsg 19155 df-eqg 19156 df-ghm 19244 df-cntz 19348 df-od 19561 df-cmn 19815 df-abl 19816 df-mgp 20153 df-rng 20171 df-ur 20200 df-srg 20205 df-ring 20253 df-cring 20254 df-oppr 20351 df-dvdsr 20374 df-unit 20375 df-invr 20405 df-dvr 20418 df-rhm 20489 df-rim 20490 df-nzr 20530 df-subrng 20563 df-subrg 20587 df-rlreg 20711 df-domn 20712 df-idom 20713 df-drng 20748 df-field 20749 df-lmod 20877 df-lss 20948 df-lsp 20988 df-sra 21190 df-rgmod 21191 df-lidl 21236 df-rsp 21237 df-2idl 21278 df-cnfld 21383 df-zring 21476 df-zrh 21532 df-chr 21534 df-zn 21535 df-assa 21891 df-asp 21892 df-ascl 21893 df-psr 21947 df-mvr 21948 df-mpl 21949 df-opsr 21951 df-evls 22116 df-evl 22117 df-psr1 22197 df-vr1 22198 df-ply1 22199 df-coe1 22200 df-evl1 22336 df-mdeg 26109 df-deg1 26110 df-mon1 26185 df-uc1p 26186 df-q1p 26187 df-r1p 26188 df-primroots 42074

This theorem is referenced by: aks6d1c6lem4 42155

W3C validator