Theorem dfcgra2 26624

Description: This is the full statement of definition 11.2 of [Schwabhauser] p. 95. This proof serves to confirm that the definition we have chosen, df-cgra 26602 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.)

Hypotheses

Ref	Expression
dfcgra2.p	⊢ 𝑃 = (Base‘𝐺)
dfcgra2.i	⊢ 𝐼 = (Itv‘𝐺)
dfcgra2.m	⊢ − = (dist‘𝐺)
dfcgra2.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
dfcgra2.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
dfcgra2.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
dfcgra2.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
dfcgra2.d	⊢ (𝜑 → 𝐷 ∈ 𝑃)
dfcgra2.e	⊢ (𝜑 → 𝐸 ∈ 𝑃)
dfcgra2.f	⊢ (𝜑 → 𝐹 ∈ 𝑃)

Assertion

Ref	Expression
dfcgra2	⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))))

Distinct variable groups:   − ,𝑎,𝑐,𝑑,𝑓   𝐴,𝑎,𝑐,𝑑,𝑓   𝐵,𝑎,𝑐,𝑑,𝑓   𝐶,𝑎,𝑐,𝑑,𝑓   𝐷,𝑎,𝑐,𝑑,𝑓   𝐸,𝑎,𝑐,𝑑,𝑓   𝐹,𝑎,𝑐,𝑑,𝑓   𝐺,𝑎,𝑐,𝑑,𝑓   𝐼,𝑎,𝑐,𝑑,𝑓   𝑃,𝑎,𝑐,𝑑,𝑓   𝜑,𝑎,𝑐,𝑑,𝑓

Proof of Theorem dfcgra2

Dummy variables 𝑡 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcgra2.p	. . . . 5 ⊢ 𝑃 = (Base‘𝐺)
2		dfcgra2.i	. . . . 5 ⊢ 𝐼 = (Itv‘𝐺)
3		eqid 2798	. . . . 5 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
4		dfcgra2.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐺 ∈ TarskiG)
6		dfcgra2.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
7	6	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴 ∈ 𝑃)
8		dfcgra2.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
9	8	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵 ∈ 𝑃)
10		dfcgra2.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
11	10	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶 ∈ 𝑃)
12		dfcgra2.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
13	12	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷 ∈ 𝑃)
14		dfcgra2.e	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
15	14	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸 ∈ 𝑃)
16		dfcgra2.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
17	16	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹 ∈ 𝑃)
18		simpr 488	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
19	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18	cgrane1 26606	. . . 4 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴 ≠ 𝐵)
20	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18	cgrane2 26607	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵 ≠ 𝐶)
21	20	necomd 3042	. . . 4 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶 ≠ 𝐵)
22	19, 21	jca 515	. . 3 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵))
23	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18	cgrane3 26608	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸 ≠ 𝐷)
24	23	necomd 3042	. . . 4 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷 ≠ 𝐸)
25	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18	cgrane4 26609	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸 ≠ 𝐹)
26	25	necomd 3042	. . . 4 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹 ≠ 𝐸)
27	24, 26	jca 515	. . 3 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))
28		simprl 770	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))))
29		simprr 772	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))
30	4	ad6antr 735	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐺 ∈ TarskiG)
31		simp-5r 785	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎 ∈ 𝑃)
32	8	ad6antr 735	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐵 ∈ 𝑃)
33		simp-4r 783	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐 ∈ 𝑃)
34		simpllr 775	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑑 ∈ 𝑃)
35	14	ad6antr 735	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐸 ∈ 𝑃)
36		simplr 768	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑓 ∈ 𝑃)
37	16	ad6antr 735	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹 ∈ 𝑃)
38	12	ad6antr 735	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷 ∈ 𝑃)
39	10	ad6antr 735	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ∈ 𝑃)
40	6	ad6antr 735	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ∈ 𝑃)
41		simp-6r 787	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
42	1, 2, 30, 3, 40, 32, 39, 38, 35, 37, 41	cgracom 26616	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
43	28	simplld 767	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ∈ (𝐵𝐼𝑎))
44		dfcgra2.m	. . . . . . . . . . . . . . . . . 18 ⊢ − = (dist‘𝐺)
45	19	ad5antr 733	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ≠ 𝐵)
46	1, 44, 2, 30, 32, 40, 31, 43, 45	tgbtwnne 26284	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐵 ≠ 𝑎)
47	1, 2, 3, 32, 31, 40, 30, 40, 43, 46, 45	btwnhl1 26406	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴((hlG‘𝐺)‘𝐵)𝑎)
48	1, 2, 3, 40, 31, 32, 30, 47	hlcomd 26398	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝐴)
49	1, 2, 3, 30, 38, 35, 37, 40, 32, 39, 42, 31, 48	cgrahl1 26610	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝐶”⟩)
50	28	simprld 771	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ∈ (𝐵𝐼𝑐))
51	21	ad5antr 733	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ≠ 𝐵)
52	1, 44, 2, 30, 32, 39, 33, 50, 51	tgbtwnne 26284	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐵 ≠ 𝑐)
53	1, 2, 3, 32, 33, 39, 30, 40, 50, 52, 51	btwnhl1 26406	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶((hlG‘𝐺)‘𝐵)𝑐)
54	1, 2, 3, 39, 33, 32, 30, 53	hlcomd 26398	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝐶)
55	1, 2, 3, 30, 38, 35, 37, 31, 32, 39, 49, 33, 54	cgrahl2 26611	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝑐”⟩)
56	1, 2, 30, 3, 38, 35, 37, 31, 32, 33, 55	cgracom 26616	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
57	29	simplld 767	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷 ∈ (𝐸𝐼𝑑))
58	24	ad5antr 733	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷 ≠ 𝐸)
59	1, 44, 2, 30, 35, 38, 34, 57, 58	tgbtwnne 26284	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐸 ≠ 𝑑)
60	1, 2, 3, 35, 34, 38, 30, 40, 57, 59, 58	btwnhl1 26406	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷((hlG‘𝐺)‘𝐸)𝑑)
61	1, 2, 3, 38, 34, 35, 30, 60	hlcomd 26398	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑑((hlG‘𝐺)‘𝐸)𝐷)
62	1, 2, 3, 30, 31, 32, 33, 38, 35, 37, 56, 34, 61	cgrahl1 26610	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝐹”⟩)
63	29	simprld 771	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹 ∈ (𝐸𝐼𝑓))
64	26	ad5antr 733	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹 ≠ 𝐸)
65	1, 44, 2, 30, 35, 37, 36, 63, 64	tgbtwnne 26284	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐸 ≠ 𝑓)
66	1, 2, 3, 35, 36, 37, 30, 40, 63, 65, 64	btwnhl1 26406	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹((hlG‘𝐺)‘𝐸)𝑓)
67	1, 2, 3, 37, 36, 35, 30, 66	hlcomd 26398	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑓((hlG‘𝐺)‘𝐸)𝐹)
68	1, 2, 3, 30, 31, 32, 33, 34, 35, 37, 62, 36, 67	cgrahl2 26611	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝑓”⟩)
69	46	necomd 3042	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎 ≠ 𝐵)
70	1, 2, 3, 31, 40, 32, 30, 69	hlid 26403	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝑎)
71	52	necomd 3042	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐 ≠ 𝐵)
72	1, 2, 3, 33, 40, 32, 30, 71	hlid 26403	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝑐)
73	1, 44, 2, 30, 32, 40, 31, 43	tgbtwncom 26282	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ∈ (𝑎𝐼𝐵))
74	28	simplrd 769	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐴 − 𝑎) = (𝐸 − 𝐷))
75	1, 44, 2, 30, 40, 31, 35, 38, 74	tgcgrcoml 26273	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑎 − 𝐴) = (𝐸 − 𝐷))
76	29	simplrd 769	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐷 − 𝑑) = (𝐵 − 𝐴))
77	76	eqcomd 2804	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝐴) = (𝐷 − 𝑑))
78	1, 44, 2, 30, 32, 40, 38, 34, 77	tgcgrcoml 26273	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐴 − 𝐵) = (𝐷 − 𝑑))
79	1, 44, 2, 30, 31, 40, 32, 35, 38, 34, 73, 57, 75, 78	tgcgrextend 26279	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑎 − 𝐵) = (𝐸 − 𝑑))
80	1, 44, 2, 30, 31, 32, 35, 34, 79	tgcgrcoml 26273	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝑎) = (𝐸 − 𝑑))
81	1, 44, 2, 30, 32, 39, 33, 50	tgbtwncom 26282	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ∈ (𝑐𝐼𝐵))
82	28	simprrd 773	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐶 − 𝑐) = (𝐸 − 𝐹))
83	1, 44, 2, 30, 39, 33, 35, 37, 82	tgcgrcoml 26273	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑐 − 𝐶) = (𝐸 − 𝐹))
84	29	simprrd 773	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐹 − 𝑓) = (𝐵 − 𝐶))
85	84	eqcomd 2804	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝐶) = (𝐹 − 𝑓))
86	1, 44, 2, 30, 32, 39, 37, 36, 85	tgcgrcoml 26273	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐶 − 𝐵) = (𝐹 − 𝑓))
87	1, 44, 2, 30, 33, 39, 32, 35, 37, 36, 81, 63, 83, 86	tgcgrextend 26279	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑐 − 𝐵) = (𝐸 − 𝑓))
88	1, 44, 2, 30, 33, 32, 35, 36, 87	tgcgrcoml 26273	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝑐) = (𝐸 − 𝑓))
89	1, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68, 31, 44, 33, 70, 72, 80, 88	cgracgr 26612	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑎 − 𝑐) = (𝑑 − 𝑓))
90	28, 29, 89	3jca 1125	. . . . . . . 8 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))
91	90	ex 416	. . . . . . 7 ⊢ ((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))
92	91	reximdva 3233	. . . . . 6 ⊢ (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) → (∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) → ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))
93	92	reximdva 3233	. . . . 5 ⊢ ((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) → (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) → ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))
94	93	imp 410	. . . 4 ⊢ (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))
95	1, 44, 2, 4, 8, 6, 14, 12	axtgsegcon 26258	. . . . . . . 8 ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)))
96	1, 44, 2, 4, 8, 10, 14, 16	axtgsegcon 26258	. . . . . . . 8 ⊢ (𝜑 → ∃𝑐 ∈ 𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))
97		reeanv 3320	. . . . . . . 8 ⊢ (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ↔ (∃𝑎 ∈ 𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ ∃𝑐 ∈ 𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))))
98	95, 96, 97	sylanbrc 586	. . . . . . 7 ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))))
99	1, 44, 2, 4, 14, 12, 8, 6	axtgsegcon 26258	. . . . . . . 8 ⊢ (𝜑 → ∃𝑑 ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)))
100	1, 44, 2, 4, 14, 16, 8, 10	axtgsegcon 26258	. . . . . . . 8 ⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))
101		reeanv 3320	. . . . . . . 8 ⊢ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ↔ (∃𝑑 ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ ∃𝑓 ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))
102	99, 100, 101	sylanbrc 586	. . . . . . 7 ⊢ (𝜑 → ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))
103	98, 102	jca 515	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
104		r19.41vv 3302	. . . . . . . . 9 ⊢ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))))
105		ancom 464	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
106	105	2rexbii 3211	. . . . . . . . 9 ⊢ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
107		ancom 464	. . . . . . . . 9 ⊢ ((∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
108	104, 106, 107	3bitr3i 304	. . . . . . . 8 ⊢ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
109	108	2rexbii 3211	. . . . . . 7 ⊢ (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
110		r19.41vv 3302	. . . . . . 7 ⊢ (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
111	109, 110	bitr2i 279	. . . . . 6 ⊢ ((∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
112	103, 111	sylib 221	. . . . 5 ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
113	112	adantr 484	. . . 4 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
114	94, 113	reximddv2 3237	. . 3 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))
115	22, 27, 114	3jca 1125	. 2 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))
116		df-3an 1086	. . 3 ⊢ (((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) ↔ (((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸)) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))
117	4	ad6antr 735	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐺 ∈ TarskiG)
118	12	ad6antr 735	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ∈ 𝑃)
119	14	ad6antr 735	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐸 ∈ 𝑃)
120	16	ad6antr 735	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹 ∈ 𝑃)
121	6	ad6antr 735	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴 ∈ 𝑃)
122	8	ad6antr 735	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐵 ∈ 𝑃)
123	10	ad6antr 735	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ∈ 𝑃)
124		simp-4r 783	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑦 ∈ 𝑃)
125		simp-5r 785	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑥 ∈ 𝑃)
126		simpllr 775	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑧 ∈ 𝑃)
127		simplr 768	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑡 ∈ 𝑃)
128		eqid 2798	. . . . . . . . . . . . . 14 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
129		simpr1 1191	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))))
130	129	simplld 767	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴 ∈ (𝐵𝐼𝑥))
131		simpr2 1192	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))))
132	131	simplld 767	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ∈ (𝐸𝐼𝑧))
133	1, 44, 2, 117, 119, 118, 126, 132	tgbtwncom 26282	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ∈ (𝑧𝐼𝐸))
134	131	simplrd 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐷 − 𝑧) = (𝐵 − 𝐴))
135	134	eqcomd 2804	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝐴) = (𝐷 − 𝑧))
136	1, 44, 2, 117, 122, 121, 118, 126, 135	tgcgrcomr 26272	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝐴) = (𝑧 − 𝐷))
137	129	simplrd 769	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐴 − 𝑥) = (𝐸 − 𝐷))
138	1, 44, 2, 117, 121, 125, 119, 118, 137	tgcgrcomr 26272	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐴 − 𝑥) = (𝐷 − 𝐸))
139	1, 44, 2, 117, 122, 121, 125, 126, 118, 119, 130, 133, 136, 138	tgcgrextend 26279	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝑥) = (𝑧 − 𝐸))
140	1, 44, 2, 117, 122, 125, 126, 119, 139	tgcgrcoml 26273	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑥 − 𝐵) = (𝑧 − 𝐸))
141	129	simprld 771	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ∈ (𝐵𝐼𝑦))
142	1, 44, 2, 117, 122, 123, 124, 141	tgbtwncom 26282	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ∈ (𝑦𝐼𝐵))
143	131	simprld 771	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹 ∈ (𝐸𝐼𝑡))
144	129	simprrd 773	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐶 − 𝑦) = (𝐸 − 𝐹))
145	1, 44, 2, 117, 123, 124, 119, 120, 144	tgcgrcoml 26273	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑦 − 𝐶) = (𝐸 − 𝐹))
146	131	simprrd 773	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐹 − 𝑡) = (𝐵 − 𝐶))
147	146	eqcomd 2804	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝐶) = (𝐹 − 𝑡))
148	1, 44, 2, 117, 122, 123, 120, 127, 147	tgcgrcoml 26273	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐶 − 𝐵) = (𝐹 − 𝑡))
149	1, 44, 2, 117, 124, 123, 122, 119, 120, 127, 142, 143, 145, 148	tgcgrextend 26279	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑦 − 𝐵) = (𝐸 − 𝑡))
150	1, 44, 2, 117, 124, 122, 119, 127, 149	tgcgrcoml 26273	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝑦) = (𝐸 − 𝑡))
151		simpr3 1193	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑥 − 𝑦) = (𝑧 − 𝑡))
152	1, 44, 2, 117, 125, 124, 126, 127, 151	tgcgrcomlr 26274	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑦 − 𝑥) = (𝑡 − 𝑧))
153	1, 44, 128, 117, 125, 122, 124, 126, 119, 127, 140, 150, 152	trgcgr 26310	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrG‘𝐺)⟨“𝑧𝐸𝑡”⟩)
154		simp-6r 787	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸)))
155	154	simprld 771	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ≠ 𝐸)
156	1, 44, 2, 117, 119, 118, 126, 132, 155	tgbtwnne 26284	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐸 ≠ 𝑧)
157	1, 2, 3, 119, 126, 118, 117, 122, 132, 156, 155	btwnhl1 26406	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷((hlG‘𝐺)‘𝐸)𝑧)
158	1, 2, 3, 118, 126, 119, 117, 157	hlcomd 26398	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑧((hlG‘𝐺)‘𝐸)𝐷)
159	154	simprrd 773	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹 ≠ 𝐸)
160	1, 44, 2, 117, 119, 120, 127, 143, 159	tgbtwnne 26284	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐸 ≠ 𝑡)
161	1, 2, 3, 119, 127, 120, 117, 122, 143, 160, 159	btwnhl1 26406	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹((hlG‘𝐺)‘𝐸)𝑡)
162	1, 2, 3, 120, 127, 119, 117, 161	hlcomd 26398	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑡((hlG‘𝐺)‘𝐸)𝐹)
163	1, 2, 3, 117, 125, 122, 124, 118, 119, 120, 126, 127, 153, 158, 162	iscgrad 26605	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
164	1, 2, 117, 3, 125, 122, 124, 118, 119, 120, 163	cgracom 26616	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑥𝐵𝑦”⟩)
165	154	simplld 767	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴 ≠ 𝐵)
166	1, 44, 2, 117, 122, 121, 125, 130, 165	tgbtwnne 26284	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐵 ≠ 𝑥)
167	1, 2, 3, 122, 125, 121, 117, 121, 130, 166, 165	btwnhl1 26406	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴((hlG‘𝐺)‘𝐵)𝑥)
168	1, 2, 3, 117, 118, 119, 120, 125, 122, 124, 164, 121, 167	cgrahl1 26610	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝑦”⟩)
169	154	simplrd 769	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ≠ 𝐵)
170	1, 44, 2, 117, 122, 123, 124, 141, 169	tgbtwnne 26284	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐵 ≠ 𝑦)
171	1, 2, 3, 122, 124, 123, 117, 121, 141, 170, 169	btwnhl1 26406	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶((hlG‘𝐺)‘𝐵)𝑦)
172	1, 2, 3, 117, 118, 119, 120, 121, 122, 124, 168, 123, 171	cgrahl2 26611	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
173	1, 2, 117, 3, 118, 119, 120, 121, 122, 123, 172	cgracom 26616	. . . . . . . 8 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
174	173	adantl3r 749	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
175		simpr 488	. . . . . . . 8 ⊢ (((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) → ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)))
176		oveq2 7143	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑧 → (𝐸𝐼𝑑) = (𝐸𝐼𝑧))
177	176	eleq2d 2875	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑧 → (𝐷 ∈ (𝐸𝐼𝑑) ↔ 𝐷 ∈ (𝐸𝐼𝑧)))
178		oveq2 7143	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑧 → (𝐷 − 𝑑) = (𝐷 − 𝑧))
179	178	eqeq1d 2800	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑧 → ((𝐷 − 𝑑) = (𝐵 − 𝐴) ↔ (𝐷 − 𝑧) = (𝐵 − 𝐴)))
180	177, 179	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑧 → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴))))
181	180	anbi1d 632	. . . . . . . . . 10 ⊢ (𝑑 = 𝑧 → (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
182		oveq1 7142	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑧 → (𝑑 − 𝑓) = (𝑧 − 𝑓))
183	182	eqeq2d 2809	. . . . . . . . . 10 ⊢ (𝑑 = 𝑧 → ((𝑥 − 𝑦) = (𝑑 − 𝑓) ↔ (𝑥 − 𝑦) = (𝑧 − 𝑓)))
184	181, 183	3anbi23d 1436	. . . . . . . . 9 ⊢ (𝑑 = 𝑧 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑓))))
185		oveq2 7143	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑡 → (𝐸𝐼𝑓) = (𝐸𝐼𝑡))
186	185	eleq2d 2875	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑡 → (𝐹 ∈ (𝐸𝐼𝑓) ↔ 𝐹 ∈ (𝐸𝐼𝑡)))
187		oveq2 7143	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑡 → (𝐹 − 𝑓) = (𝐹 − 𝑡))
188	187	eqeq1d 2800	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑡 → ((𝐹 − 𝑓) = (𝐵 − 𝐶) ↔ (𝐹 − 𝑡) = (𝐵 − 𝐶)))
189	186, 188	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑡 → ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)) ↔ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))))
190	189	anbi2d 631	. . . . . . . . . 10 ⊢ (𝑓 = 𝑡 → (((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶)))))
191		oveq2 7143	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑡 → (𝑧 − 𝑓) = (𝑧 − 𝑡))
192	191	eqeq2d 2809	. . . . . . . . . 10 ⊢ (𝑓 = 𝑡 → ((𝑥 − 𝑦) = (𝑧 − 𝑓) ↔ (𝑥 − 𝑦) = (𝑧 − 𝑡)))
193	190, 192	3anbi23d 1436	. . . . . . . . 9 ⊢ (𝑓 = 𝑡 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))))
194	184, 193	cbvrex2vw 3409	. . . . . . . 8 ⊢ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)) ↔ ∃𝑧 ∈ 𝑃 ∃𝑡 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡)))
195	175, 194	sylib 221	. . . . . . 7 ⊢ (((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) → ∃𝑧 ∈ 𝑃 ∃𝑡 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡)))
196	174, 195	r19.29vva 3292	. . . . . 6 ⊢ (((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
197	196	adantl3r 749	. . . . 5 ⊢ ((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
198		simpr 488	. . . . . 6 ⊢ (((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))
199		oveq2 7143	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑥 → (𝐵𝐼𝑎) = (𝐵𝐼𝑥))
200	199	eleq2d 2875	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (𝐴 ∈ (𝐵𝐼𝑎) ↔ 𝐴 ∈ (𝐵𝐼𝑥)))
201		oveq2 7143	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑥 → (𝐴 − 𝑎) = (𝐴 − 𝑥))
202	201	eqeq1d 2800	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → ((𝐴 − 𝑎) = (𝐸 − 𝐷) ↔ (𝐴 − 𝑥) = (𝐸 − 𝐷)))
203	200, 202	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑎 = 𝑥 → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ↔ (𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷))))
204	203	anbi1d 632	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))))
205		oveq1 7142	. . . . . . . . . 10 ⊢ (𝑎 = 𝑥 → (𝑎 − 𝑐) = (𝑥 − 𝑐))
206	205	eqeq1d 2800	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → ((𝑎 − 𝑐) = (𝑑 − 𝑓) ↔ (𝑥 − 𝑐) = (𝑑 − 𝑓)))
207	204, 206	3anbi13d 1435	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓))))
208	207	2rexbidv 3259	. . . . . . 7 ⊢ (𝑎 = 𝑥 → (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)) ↔ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓))))
209		oveq2 7143	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑦 → (𝐵𝐼𝑐) = (𝐵𝐼𝑦))
210	209	eleq2d 2875	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑦 → (𝐶 ∈ (𝐵𝐼𝑐) ↔ 𝐶 ∈ (𝐵𝐼𝑦)))
211		oveq2 7143	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑦 → (𝐶 − 𝑐) = (𝐶 − 𝑦))
212	211	eqeq1d 2800	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑦 → ((𝐶 − 𝑐) = (𝐸 − 𝐹) ↔ (𝐶 − 𝑦) = (𝐸 − 𝐹)))
213	210, 212	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑐 = 𝑦 → ((𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)) ↔ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))))
214	213	anbi2d 631	. . . . . . . . 9 ⊢ (𝑐 = 𝑦 → (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹)))))
215		oveq2 7143	. . . . . . . . . 10 ⊢ (𝑐 = 𝑦 → (𝑥 − 𝑐) = (𝑥 − 𝑦))
216	215	eqeq1d 2800	. . . . . . . . 9 ⊢ (𝑐 = 𝑦 → ((𝑥 − 𝑐) = (𝑑 − 𝑓) ↔ (𝑥 − 𝑦) = (𝑑 − 𝑓)))
217	214, 216	3anbi13d 1435	. . . . . . . 8 ⊢ (𝑐 = 𝑦 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))))
218	217	2rexbidv 3259	. . . . . . 7 ⊢ (𝑐 = 𝑦 → (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓)) ↔ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))))
219	208, 218	cbvrex2vw 3409	. . . . . 6 ⊢ (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)))
220	198, 219	sylib 221	. . . . 5 ⊢ (((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)))
221	197, 220	r19.29vva 3292	. . . 4 ⊢ (((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
222	221	anasss 470	. . 3 ⊢ ((𝜑 ∧ (((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸)) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
223	116, 222	sylan2b 596	. 2 ⊢ ((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
224	115, 223	impbida 800	1 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∃wrex 3107   class class class wbr 5030  ‘cfv 6324  (class class class)co 7135  ⟨“cs3 14195  Basecbs 16475  distcds 16566  TarskiGcstrkg 26224  Itvcitv 26230  cgrGccgrg 26304  hlGchlg 26394  cgrAccgra 26601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-map 8391  df-pm 8392  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-dju 9314  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-xnn0 11956  df-z 11970  df-uz 12232  df-fz 12886  df-fzo 13029  df-hash 13687  df-word 13858  df-concat 13914  df-s1 13941  df-s2 14201  df-s3 14202  df-trkgc 26242  df-trkgb 26243  df-trkgcb 26244  df-trkg 26247  df-cgrg 26305  df-leg 26377  df-hlg 26395  df-cgra 26602

This theorem is referenced by: (None)