Theorem dfcgra2 29119

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 29097 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 2763	. . . . 5 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
4		dfcgra2.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐺 ∈ TarskiG)
6		dfcgra2.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
7	6	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴 ∈ 𝑃)
8		dfcgra2.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
9	8	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵 ∈ 𝑃)
10		dfcgra2.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
11	10	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶 ∈ 𝑃)
12		dfcgra2.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
13	12	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷 ∈ 𝑃)
14		dfcgra2.e	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
15	14	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸 ∈ 𝑃)
16		dfcgra2.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
17	16	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹 ∈ 𝑃)
18		simpr 489	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
19	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18	cgrane1 29101	. . . 4 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴 ≠ 𝐵)
20	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18	cgrane2 29102	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵 ≠ 𝐶)
21	20	necomd 3013	. . . 4 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶 ≠ 𝐵)
22	19, 21	jca 520	. . 3 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵))
23	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18	cgrane3 29103	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸 ≠ 𝐷)
24	23	necomd 3013	. . . 4 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷 ≠ 𝐸)
25	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18	cgrane4 29104	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸 ≠ 𝐹)
26	25	necomd 3013	. . . 4 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹 ≠ 𝐸)
27	24, 26	jca 520	. . 3 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))
28		simprl 782	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))))
29		simprr 784	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))
30	4	ad6antr 748	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐺 ∈ TarskiG)
31		simp-5r 797	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎 ∈ 𝑃)
32	8	ad6antr 748	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐵 ∈ 𝑃)
33		simp-4r 795	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐 ∈ 𝑃)
34		simpllr 787	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑑 ∈ 𝑃)
35	14	ad6antr 748	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐸 ∈ 𝑃)
36		simplr 780	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑓 ∈ 𝑃)
37	16	ad6antr 748	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹 ∈ 𝑃)
38	12	ad6antr 748	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷 ∈ 𝑃)
39	10	ad6antr 748	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ∈ 𝑃)
40	6	ad6antr 748	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ∈ 𝑃)
41		simp-6r 799	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
42	1, 2, 30, 3, 40, 32, 39, 38, 35, 37, 41	cgracom 29111	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
43	28	simplld 779	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ∈ (𝐵𝐼𝑎))
44		dfcgra2.m	. . . . . . . . . . . . . . . . . 18 ⊢ − = (dist‘𝐺)
45	19	ad5antr 746	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ≠ 𝐵)
46	1, 44, 2, 30, 32, 40, 31, 43, 45	tgbtwnne 28737	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐵 ≠ 𝑎)
47	1, 2, 3, 32, 31, 40, 30, 40, 43, 46, 45	btwnhl1 28862	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴((hlG‘𝐺)‘𝐵)𝑎)
48	1, 2, 3, 40, 31, 32, 30, 47	hlcomd 28854	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝐴)
49	1, 2, 3, 30, 38, 35, 37, 40, 32, 39, 42, 31, 48	cgrahl1 29105	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝐶”⟩)
50	28	simprld 783	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ∈ (𝐵𝐼𝑐))
51	21	ad5antr 746	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ≠ 𝐵)
52	1, 44, 2, 30, 32, 39, 33, 50, 51	tgbtwnne 28737	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐵 ≠ 𝑐)
53	1, 2, 3, 32, 33, 39, 30, 40, 50, 52, 51	btwnhl1 28862	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶((hlG‘𝐺)‘𝐵)𝑐)
54	1, 2, 3, 39, 33, 32, 30, 53	hlcomd 28854	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝐶)
55	1, 2, 3, 30, 38, 35, 37, 31, 32, 39, 49, 33, 54	cgrahl2 29106	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝑐”⟩)
56	1, 2, 30, 3, 38, 35, 37, 31, 32, 33, 55	cgracom 29111	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
57	29	simplld 779	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷 ∈ (𝐸𝐼𝑑))
58	24	ad5antr 746	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷 ≠ 𝐸)
59	1, 44, 2, 30, 35, 38, 34, 57, 58	tgbtwnne 28737	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐸 ≠ 𝑑)
60	1, 2, 3, 35, 34, 38, 30, 40, 57, 59, 58	btwnhl1 28862	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷((hlG‘𝐺)‘𝐸)𝑑)
61	1, 2, 3, 38, 34, 35, 30, 60	hlcomd 28854	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑑((hlG‘𝐺)‘𝐸)𝐷)
62	1, 2, 3, 30, 31, 32, 33, 38, 35, 37, 56, 34, 61	cgrahl1 29105	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝐹”⟩)
63	29	simprld 783	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹 ∈ (𝐸𝐼𝑓))
64	26	ad5antr 746	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹 ≠ 𝐸)
65	1, 44, 2, 30, 35, 37, 36, 63, 64	tgbtwnne 28737	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐸 ≠ 𝑓)
66	1, 2, 3, 35, 36, 37, 30, 40, 63, 65, 64	btwnhl1 28862	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹((hlG‘𝐺)‘𝐸)𝑓)
67	1, 2, 3, 37, 36, 35, 30, 66	hlcomd 28854	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑓((hlG‘𝐺)‘𝐸)𝐹)
68	1, 2, 3, 30, 31, 32, 33, 34, 35, 37, 62, 36, 67	cgrahl2 29106	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝑓”⟩)
69	46	necomd 3013	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎 ≠ 𝐵)
70	1, 2, 3, 31, 40, 32, 30, 69	hlid 28859	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝑎)
71	52	necomd 3013	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐 ≠ 𝐵)
72	1, 2, 3, 33, 40, 32, 30, 71	hlid 28859	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝑐)
73	1, 44, 2, 30, 32, 40, 31, 43	tgbtwncom 28735	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ∈ (𝑎𝐼𝐵))
74	28	simplrd 781	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐴 − 𝑎) = (𝐸 − 𝐷))
75	1, 44, 2, 30, 40, 31, 35, 38, 74	tgcgrcoml 28726	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑎 − 𝐴) = (𝐸 − 𝐷))
76	29	simplrd 781	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐷 − 𝑑) = (𝐵 − 𝐴))
77	76	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝐴) = (𝐷 − 𝑑))
78	1, 44, 2, 30, 32, 40, 38, 34, 77	tgcgrcoml 28726	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐴 − 𝐵) = (𝐷 − 𝑑))
79	1, 44, 2, 30, 31, 40, 32, 35, 38, 34, 73, 57, 75, 78	tgcgrextend 28732	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑎 − 𝐵) = (𝐸 − 𝑑))
80	1, 44, 2, 30, 31, 32, 35, 34, 79	tgcgrcoml 28726	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝑎) = (𝐸 − 𝑑))
81	1, 44, 2, 30, 32, 39, 33, 50	tgbtwncom 28735	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ∈ (𝑐𝐼𝐵))
82	28	simprrd 785	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐶 − 𝑐) = (𝐸 − 𝐹))
83	1, 44, 2, 30, 39, 33, 35, 37, 82	tgcgrcoml 28726	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑐 − 𝐶) = (𝐸 − 𝐹))
84	29	simprrd 785	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐹 − 𝑓) = (𝐵 − 𝐶))
85	84	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝐶) = (𝐹 − 𝑓))
86	1, 44, 2, 30, 32, 39, 37, 36, 85	tgcgrcoml 28726	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐶 − 𝐵) = (𝐹 − 𝑓))
87	1, 44, 2, 30, 33, 39, 32, 35, 37, 36, 81, 63, 83, 86	tgcgrextend 28732	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑐 − 𝐵) = (𝐸 − 𝑓))
88	1, 44, 2, 30, 33, 32, 35, 36, 87	tgcgrcoml 28726	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝑐) = (𝐸 − 𝑓))
89	1, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68, 31, 44, 33, 70, 72, 80, 88	cgracgr 29107	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑎 − 𝑐) = (𝑑 − 𝑓))
90	28, 29, 89	3jca 1146	. . . . . . . 8 ⊢ (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))
91	90	ex 417	. . . . . . 7 ⊢ ((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))
92	91	reximdva 3178	. . . . . 6 ⊢ (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) → (∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) → ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))
93	92	reximdva 3178	. . . . 5 ⊢ ((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) → (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) → ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))
94	93	imp 411	. . . 4 ⊢ (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))
95	1, 44, 2, 4, 8, 6, 14, 12	axtgsegcon 28711	. . . . . . . 8 ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)))
96	1, 44, 2, 4, 8, 10, 14, 16	axtgsegcon 28711	. . . . . . . 8 ⊢ (𝜑 → ∃𝑐 ∈ 𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))
97		reeanv 3237	. . . . . . . 8 ⊢ (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ↔ (∃𝑎 ∈ 𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ ∃𝑐 ∈ 𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))))
98	95, 96, 97	sylanbrc 594	. . . . . . 7 ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))))
99	1, 44, 2, 4, 14, 12, 8, 6	axtgsegcon 28711	. . . . . . . 8 ⊢ (𝜑 → ∃𝑑 ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)))
100	1, 44, 2, 4, 14, 16, 8, 10	axtgsegcon 28711	. . . . . . . 8 ⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))
101		reeanv 3237	. . . . . . . 8 ⊢ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ↔ (∃𝑑 ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ ∃𝑓 ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))
102	99, 100, 101	sylanbrc 594	. . . . . . 7 ⊢ (𝜑 → ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))
103	98, 102	jca 520	. . . . . 6 ⊢ (𝜑 → (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
104		r19.41vv 3235	. . . . . . . . 9 ⊢ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))))
105		ancom 465	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
106	105	2rexbii 3141	. . . . . . . . 9 ⊢ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
107		ancom 465	. . . . . . . . 9 ⊢ ((∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
108	104, 106, 107	3bitr3i 304	. . . . . . . 8 ⊢ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
109	108	2rexbii 3141	. . . . . . 7 ⊢ (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
110		r19.41vv 3235	. . . . . . 7 ⊢ (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
111	109, 110	bitr2i 279	. . . . . 6 ⊢ ((∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
112	103, 111	sylib 221	. . . . 5 ⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
113	112	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
114	94, 113	reximddv2 3224	. . 3 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))
115	22, 27, 114	3jca 1146	. 2 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))
116		df-3an 1105	. . 3 ⊢ (((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) ↔ (((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸)) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))
117	4	ad6antr 748	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐺 ∈ TarskiG)
118	12	ad6antr 748	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ∈ 𝑃)
119	14	ad6antr 748	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐸 ∈ 𝑃)
120	16	ad6antr 748	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹 ∈ 𝑃)
121	6	ad6antr 748	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴 ∈ 𝑃)
122	8	ad6antr 748	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐵 ∈ 𝑃)
123	10	ad6antr 748	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ∈ 𝑃)
124		simp-4r 795	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑦 ∈ 𝑃)
125		simp-5r 797	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑥 ∈ 𝑃)
126		simpllr 787	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑧 ∈ 𝑃)
127		simplr 780	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑡 ∈ 𝑃)
128		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
129		simpr1 1213	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))))
130	129	simplld 779	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴 ∈ (𝐵𝐼𝑥))
131		simpr2 1214	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))))
132	131	simplld 779	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ∈ (𝐸𝐼𝑧))
133	1, 44, 2, 117, 119, 118, 126, 132	tgbtwncom 28735	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ∈ (𝑧𝐼𝐸))
134	131	simplrd 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐷 − 𝑧) = (𝐵 − 𝐴))
135	134	eqcomd 2769	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝐴) = (𝐷 − 𝑧))
136	1, 44, 2, 117, 122, 121, 118, 126, 135	tgcgrcomr 28725	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝐴) = (𝑧 − 𝐷))
137	129	simplrd 781	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐴 − 𝑥) = (𝐸 − 𝐷))
138	1, 44, 2, 117, 121, 125, 119, 118, 137	tgcgrcomr 28725	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐴 − 𝑥) = (𝐷 − 𝐸))
139	1, 44, 2, 117, 122, 121, 125, 126, 118, 119, 130, 133, 136, 138	tgcgrextend 28732	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝑥) = (𝑧 − 𝐸))
140	1, 44, 2, 117, 122, 125, 126, 119, 139	tgcgrcoml 28726	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑥 − 𝐵) = (𝑧 − 𝐸))
141	129	simprld 783	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ∈ (𝐵𝐼𝑦))
142	1, 44, 2, 117, 122, 123, 124, 141	tgbtwncom 28735	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ∈ (𝑦𝐼𝐵))
143	131	simprld 783	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹 ∈ (𝐸𝐼𝑡))
144	129	simprrd 785	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐶 − 𝑦) = (𝐸 − 𝐹))
145	1, 44, 2, 117, 123, 124, 119, 120, 144	tgcgrcoml 28726	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑦 − 𝐶) = (𝐸 − 𝐹))
146	131	simprrd 785	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐹 − 𝑡) = (𝐵 − 𝐶))
147	146	eqcomd 2769	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝐶) = (𝐹 − 𝑡))
148	1, 44, 2, 117, 122, 123, 120, 127, 147	tgcgrcoml 28726	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐶 − 𝐵) = (𝐹 − 𝑡))
149	1, 44, 2, 117, 124, 123, 122, 119, 120, 127, 142, 143, 145, 148	tgcgrextend 28732	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑦 − 𝐵) = (𝐸 − 𝑡))
150	1, 44, 2, 117, 124, 122, 119, 127, 149	tgcgrcoml 28726	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝑦) = (𝐸 − 𝑡))
151		simpr3 1215	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑥 − 𝑦) = (𝑧 − 𝑡))
152	1, 44, 2, 117, 125, 124, 126, 127, 151	tgcgrcomlr 28727	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑦 − 𝑥) = (𝑡 − 𝑧))
153	1, 44, 128, 117, 125, 122, 124, 126, 119, 127, 140, 150, 152	trgcgr 28763	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrG‘𝐺)⟨“𝑧𝐸𝑡”⟩)
154		simp-6r 799	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸)))
155	154	simprld 783	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ≠ 𝐸)
156	1, 44, 2, 117, 119, 118, 126, 132, 155	tgbtwnne 28737	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐸 ≠ 𝑧)
157	1, 2, 3, 119, 126, 118, 117, 122, 132, 156, 155	btwnhl1 28862	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷((hlG‘𝐺)‘𝐸)𝑧)
158	1, 2, 3, 118, 126, 119, 117, 157	hlcomd 28854	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑧((hlG‘𝐺)‘𝐸)𝐷)
159	154	simprrd 785	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹 ≠ 𝐸)
160	1, 44, 2, 117, 119, 120, 127, 143, 159	tgbtwnne 28737	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐸 ≠ 𝑡)
161	1, 2, 3, 119, 127, 120, 117, 122, 143, 160, 159	btwnhl1 28862	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹((hlG‘𝐺)‘𝐸)𝑡)
162	1, 2, 3, 120, 127, 119, 117, 161	hlcomd 28854	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑡((hlG‘𝐺)‘𝐸)𝐹)
163	1, 2, 3, 117, 125, 122, 124, 118, 119, 120, 126, 127, 153, 158, 162	iscgrad 29100	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
164	1, 2, 117, 3, 125, 122, 124, 118, 119, 120, 163	cgracom 29111	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑥𝐵𝑦”⟩)
165	154	simplld 779	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴 ≠ 𝐵)
166	1, 44, 2, 117, 122, 121, 125, 130, 165	tgbtwnne 28737	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐵 ≠ 𝑥)
167	1, 2, 3, 122, 125, 121, 117, 121, 130, 166, 165	btwnhl1 28862	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴((hlG‘𝐺)‘𝐵)𝑥)
168	1, 2, 3, 117, 118, 119, 120, 125, 122, 124, 164, 121, 167	cgrahl1 29105	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝑦”⟩)
169	154	simplrd 781	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ≠ 𝐵)
170	1, 44, 2, 117, 122, 123, 124, 141, 169	tgbtwnne 28737	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐵 ≠ 𝑦)
171	1, 2, 3, 122, 124, 123, 117, 121, 141, 170, 169	btwnhl1 28862	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶((hlG‘𝐺)‘𝐵)𝑦)
172	1, 2, 3, 117, 118, 119, 120, 121, 122, 124, 168, 123, 171	cgrahl2 29106	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
173	1, 2, 117, 3, 118, 119, 120, 121, 122, 123, 172	cgracom 29111	. . . . . . . 8 ⊢ (((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
174	173	adantl3r 762	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
175		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑧 → (𝐸𝐼𝑑) = (𝐸𝐼𝑧))
176	175	eleq2d 2849	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑧 → (𝐷 ∈ (𝐸𝐼𝑑) ↔ 𝐷 ∈ (𝐸𝐼𝑧)))
177		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑧 → (𝐷 − 𝑑) = (𝐷 − 𝑧))
178	177	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑧 → ((𝐷 − 𝑑) = (𝐵 − 𝐴) ↔ (𝐷 − 𝑧) = (𝐵 − 𝐴)))
179	176, 178	anbi12d 643	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑧 → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴))))
180	179	anbi1d 642	. . . . . . . . . 10 ⊢ (𝑑 = 𝑧 → (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))))
181		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑧 → (𝑑 − 𝑓) = (𝑧 − 𝑓))
182	181	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑑 = 𝑧 → ((𝑥 − 𝑦) = (𝑑 − 𝑓) ↔ (𝑥 − 𝑦) = (𝑧 − 𝑓)))
183	180, 182	3anbi23d 1467	. . . . . . . . 9 ⊢ (𝑑 = 𝑧 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑓))))
184		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑡 → (𝐸𝐼𝑓) = (𝐸𝐼𝑡))
185	184	eleq2d 2849	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑡 → (𝐹 ∈ (𝐸𝐼𝑓) ↔ 𝐹 ∈ (𝐸𝐼𝑡)))
186		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑡 → (𝐹 − 𝑓) = (𝐹 − 𝑡))
187	186	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑡 → ((𝐹 − 𝑓) = (𝐵 − 𝐶) ↔ (𝐹 − 𝑡) = (𝐵 − 𝐶)))
188	185, 187	anbi12d 643	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑡 → ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)) ↔ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))))
189	188	anbi2d 641	. . . . . . . . . 10 ⊢ (𝑓 = 𝑡 → (((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶)))))
190		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑡 → (𝑧 − 𝑓) = (𝑧 − 𝑡))
191	190	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑓 = 𝑡 → ((𝑥 − 𝑦) = (𝑧 − 𝑓) ↔ (𝑥 − 𝑦) = (𝑧 − 𝑡)))
192	189, 191	3anbi23d 1467	. . . . . . . . 9 ⊢ (𝑓 = 𝑡 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))))
193	183, 192	cbvrex2vw 3248	. . . . . . . 8 ⊢ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)) ↔ ∃𝑧 ∈ 𝑃 ∃𝑡 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡)))
194	193	bilani 509	. . . . . . 7 ⊢ (((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) → ∃𝑧 ∈ 𝑃 ∃𝑡 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡)))
195	174, 194	r19.29vva 3225	. . . . . 6 ⊢ (((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
196	195	adantl3r 762	. . . . 5 ⊢ ((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
197		oveq2 7420	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑥 → (𝐵𝐼𝑎) = (𝐵𝐼𝑥))
198	197	eleq2d 2849	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (𝐴 ∈ (𝐵𝐼𝑎) ↔ 𝐴 ∈ (𝐵𝐼𝑥)))
199		oveq2 7420	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑥 → (𝐴 − 𝑎) = (𝐴 − 𝑥))
200	199	eqeq1d 2765	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → ((𝐴 − 𝑎) = (𝐸 − 𝐷) ↔ (𝐴 − 𝑥) = (𝐸 − 𝐷)))
201	198, 200	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑎 = 𝑥 → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ↔ (𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷))))
202	201	anbi1d 642	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))))
203		oveq1 7419	. . . . . . . . . 10 ⊢ (𝑎 = 𝑥 → (𝑎 − 𝑐) = (𝑥 − 𝑐))
204	203	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → ((𝑎 − 𝑐) = (𝑑 − 𝑓) ↔ (𝑥 − 𝑐) = (𝑑 − 𝑓)))
205	202, 204	3anbi13d 1466	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓))))
206	205	2rexbidv 3230	. . . . . . 7 ⊢ (𝑎 = 𝑥 → (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)) ↔ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓))))
207		oveq2 7420	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑦 → (𝐵𝐼𝑐) = (𝐵𝐼𝑦))
208	207	eleq2d 2849	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑦 → (𝐶 ∈ (𝐵𝐼𝑐) ↔ 𝐶 ∈ (𝐵𝐼𝑦)))
209		oveq2 7420	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑦 → (𝐶 − 𝑐) = (𝐶 − 𝑦))
210	209	eqeq1d 2765	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑦 → ((𝐶 − 𝑐) = (𝐸 − 𝐹) ↔ (𝐶 − 𝑦) = (𝐸 − 𝐹)))
211	208, 210	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑐 = 𝑦 → ((𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)) ↔ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))))
212	211	anbi2d 641	. . . . . . . . 9 ⊢ (𝑐 = 𝑦 → (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹)))))
213		oveq2 7420	. . . . . . . . . 10 ⊢ (𝑐 = 𝑦 → (𝑥 − 𝑐) = (𝑥 − 𝑦))
214	213	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑐 = 𝑦 → ((𝑥 − 𝑐) = (𝑑 − 𝑓) ↔ (𝑥 − 𝑦) = (𝑑 − 𝑓)))
215	212, 214	3anbi13d 1466	. . . . . . . 8 ⊢ (𝑐 = 𝑦 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))))
216	215	2rexbidv 3230	. . . . . . 7 ⊢ (𝑐 = 𝑦 → (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓)) ↔ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))))
217	206, 216	cbvrex2vw 3248	. . . . . 6 ⊢ (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)))
218	217	bilani 509	. . . . 5 ⊢ (((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)))
219	196, 218	r19.29vva 3225	. . . 4 ⊢ (((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
220	219	anasss 471	. . 3 ⊢ ((𝜑 ∧ (((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸)) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
221	116, 220	sylan2b 605	. 2 ⊢ ((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
222	115, 221	impbida 812	1 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∃wrex 3089   class class class wbr 5110  ‘cfv 6538  (class class class)co 7412  ⟨“cs3 14881  Basecbs 17270  distcds 17320  TarskiGcstrkg 28674  Itvcitv 28680  cgrGccgrg 28757  hlGchlg 28847  cgrAccgra 29096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4874  df-int 4914  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7864  df-1st 7987  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-1o 8454  df-oadd 8458  df-er 8695  df-map 8827  df-pm 8828  df-en 8945  df-dom 8946  df-sdom 8947  df-fin 8948  df-dju 9888  df-card 9926  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-nn 12235  df-2 12304  df-3 12305  df-n0 12506  df-xnn0 12579  df-z 12593  df-uz 12864  df-fz 13537  df-fzo 13685  df-hash 14369  df-word 14553  df-concat 14610  df-s1 14636  df-s2 14887  df-s3 14888  df-trkgc 28695  df-trkgb 28696  df-trkgcb 28697  df-trkg 28700  df-cgrg 28758  df-leg 28830  df-hlg 28848  df-cgra 29097

This theorem is referenced by: (None)