Metamath Proof Explorer

Theorem aks6d1c6lem3

Description: Claim 6 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf TODO, eliminate hypothesis. (Contributed by metakunt, 8-May-2025)

Ref Expression
Hypotheses aks6d1c6.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( 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 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 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 ⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
aks6d1c6.18 ⊢ 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
aks6d1c6.19 ⊢ 𝑆 = { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) }
aks6d1c6lem3.1 ⊢ 𝐽 = ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
aks6d1c6lem3.2 ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ♯ ‘ ( 𝐽 “ ( ℕ0 × ℕ0 ) ) ) )
Assertion aks6d1c6lem3 ( 𝜑 → ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) ≤ ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) )

Proof

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