tgaaddcpbllem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tgaaddcpbllem1		Structured version Visualization version GIF version

Theorem tgaaddcpbllem1 29203

Description: Lemma for tgaaddcpbl 29206. (Contributed by Thierry Arnoux, 2-Aug-2026.)

**Hypotheses**
Ref	Expression
tgaaddcpbl.p	⊢ 𝑃 = (Base‘𝐺)
tgaaddcpbl.i	⊢ 𝐼 = (Itv‘𝐺)
tgaaddcpbl.l	⊢ 𝐿 = (LineG‘𝐺)
tgaaddcpbl.c	⊢ ∼ = (cgrA‘𝐺)
tgaaddcpbl.o	⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))}
tgaaddcpbl.q	⊢ 𝑄 = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑐𝐼𝑑))}
tgaaddcpbl.1	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tgaaddcpbl.s	⊢ (𝜑 → 𝑆 ∈ 𝑃)
tgaaddcpbl.t	⊢ (𝜑 → 𝑇 ∈ 𝑃)
tgaaddcpbl.u	⊢ (𝜑 → 𝑈 ∈ 𝑃)
tgaaddcpbl.v	⊢ (𝜑 → 𝑉 ∈ 𝑃)
tgaaddcpbl.w	⊢ (𝜑 → 𝑊 ∈ 𝑃)
tgaaddcpbl.x	⊢ (𝜑 → 𝑋 ∈ 𝑃)
tgaaddcpbl.y	⊢ (𝜑 → 𝑌 ∈ 𝑃)
tgaaddcpbl.z	⊢ (𝜑 → 𝑍 ∈ 𝑃)
tgaaddcpbl.2	⊢ (𝜑 → 𝑌 ≠ 𝑆)
tgaaddcpbl.3	⊢ (𝜑 → 𝑉 ≠ 𝑇)
tgaaddcpbl.4	⊢ (𝜑 → 𝑋𝑂𝑍)
tgaaddcpbl.5	⊢ (𝜑 → 𝑈𝑄𝑊)
tgaaddcpbl.6	⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)
tgaaddcpbl.7	⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)
tgaaddcpbllem3.1	⊢ (𝜑 → ¬ 𝑌 ∈ (𝑋𝐼𝑍))
tgaaddcpbllem1.1	⊢ 𝐾 = (hlG‘𝐺)
tgaaddcpbllem1.2	⊢ (𝜑 → 𝑅 ∈ (𝑌𝐿𝑆))
tgaaddcpbllem1.3	⊢ (𝜑 → 𝑅 ∈ (𝑋𝐼𝑍))
tgaaddcpbllem1.4	⊢ (𝜑 → 𝑅(𝐾‘𝑌)𝑆)

**Assertion**
Ref	Expression
tgaaddcpbllem1	⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)

Distinct variable groups: ∼ ,𝑠 𝑡, ∼ 𝐺,𝑐,𝑑,𝑡 𝐺,𝑠 𝐼,𝑎,𝑏,𝑠 𝐼,𝑐,𝑑,𝑡 𝑡,𝐾 𝐿,𝑎,𝑏,𝑠 𝐿,𝑐,𝑑,𝑡 𝑂,𝑠 𝑃,𝑎,𝑏,𝑠 𝑃,𝑐,𝑑,𝑡 𝑄,𝑐,𝑑,𝑡 𝑡,𝑅 𝑆,𝑎,𝑏,𝑠 𝑡,𝑆 𝑇,𝑐,𝑑,𝑡 𝑈,𝑐,𝑑,𝑡 𝑈,𝑠 𝑉,𝑐,𝑑,𝑡 𝑉,𝑠 𝑊,𝑠 𝑡,𝑊 𝑋,𝑠 𝑡,𝑋 𝑌,𝑎,𝑏,𝑠 𝑡,𝑌 𝑍,𝑠 𝑡,𝑍 𝜑,𝑠 𝜑,𝑡 Allowed substitution hints: 𝜑(𝑎, 𝑏, 𝑐, 𝑑) 𝑄(𝑠, 𝑎, 𝑏) ∼ (𝑎, 𝑏, 𝑐, 𝑑) 𝑅(𝑠, 𝑎, 𝑏, 𝑐, 𝑑) 𝑆(𝑐, 𝑑) 𝑇(𝑠, 𝑎, 𝑏) 𝑈(𝑎, 𝑏) 𝐺(𝑎, 𝑏) 𝐾(𝑠, 𝑎, 𝑏, 𝑐, 𝑑) 𝑂(𝑡, 𝑎, 𝑏, 𝑐, 𝑑) 𝑉(𝑎, 𝑏) 𝑊(𝑎, 𝑏, 𝑐, 𝑑) 𝑋(𝑎, 𝑏, 𝑐, 𝑑) 𝑌(𝑐, 𝑑) 𝑍(𝑎, 𝑏, 𝑐, 𝑑)

Proof of Theorem tgaaddcpbllem1 Dummy variables 𝑟 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tgaaddcpbl.c	. . . . . . . . . 10 ⊢ ∼ = (cgrA‘𝐺)
2	1	eqcomi 2774	. . . . . . . . 9 ⊢ (cgrA‘𝐺) = ∼
3	2	a1i 11	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (cgrA‘𝐺) = ∼ )
4		tgaaddcpbl.p	. . . . . . . . 9 ⊢ 𝑃 = (Base‘𝐺)
5		tgaaddcpbl.i	. . . . . . . . 9 ⊢ 𝐼 = (Itv‘𝐺)
6		tgaaddcpbllem1.1	. . . . . . . . 9 ⊢ 𝐾 = (hlG‘𝐺)
7		tgaaddcpbl.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
8	7	ad6antr 749	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) → 𝐺 ∈ TarskiG)
9	8	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝐺 ∈ TarskiG)
10		tgaaddcpbl.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
11	10	ad9antr 755	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑋 ∈ 𝑃)
12		tgaaddcpbl.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
13	12	ad9antr 755	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑌 ∈ 𝑃)
14		tgaaddcpbl.z	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
15	14	ad6antr 749	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) → 𝑍 ∈ 𝑃)
16	15	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑍 ∈ 𝑃)
17		tgaaddcpbl.u	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ 𝑃)
18	17	ad9antr 755	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑈 ∈ 𝑃)
19		tgaaddcpbl.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ 𝑃)
20	19	ad9antr 755	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑉 ∈ 𝑃)
21		simpllr 788	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑤 ∈ 𝑃)
22		simp-6r 800	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) → 𝑢 ∈ 𝑃)
23	22	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑢 ∈ 𝑃)
24		tgaaddcpbl.l	. . . . . . . . . . . . . . 15 ⊢ 𝐿 = (LineG‘𝐺)
25		tgaaddcpbl.s	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ 𝑃)
26		tgaaddcpbl.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ≠ 𝑆)
27	4, 5, 24, 7, 12, 25, 26	tglinerflx1 28957	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ (𝑌𝐿𝑆))
28		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (dist‘𝐺) = (dist‘𝐺)
29		tgaaddcpbl.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))}
30	4, 5, 24, 7, 12, 25, 26	tgelrnln 28954	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌𝐿𝑆) ∈ ran 𝐿)
31		tgaaddcpbl.4	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋𝑂𝑍)
32	4, 28, 5, 29, 24, 30, 7, 10, 14, 31	oppne1 29073	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑆))
33		nelne2 3058	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) → 𝑌 ≠ 𝑋)
34	27, 32, 33	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
35	34	necomd 3015	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
36	35	ad9antr 755	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑋 ≠ 𝑌)
37	4, 28, 5, 29, 24, 30, 7, 10, 14, 31	oppne2 29074	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑌𝐿𝑆))
38		nelne2 3058	. . . . . . . . . . . . 13 ⊢ ((𝑌 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → 𝑌 ≠ 𝑍)
39	27, 37, 38	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ≠ 𝑍)
40	39	ad9antr 755	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑌 ≠ 𝑍)
41		eqid 2765	. . . . . . . . . . . 12 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
42		simp-7r 802	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋))
43	42	eqcomd 2771	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑌(dist‘𝐺)𝑋) = (𝑉(dist‘𝐺)𝑢))
44	4, 28, 5, 9, 13, 11, 20, 23, 43	tgcgrcomlr 28800	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑋(dist‘𝐺)𝑌) = (𝑢(dist‘𝐺)𝑉))
45	44	eqcomd 2771	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑢(dist‘𝐺)𝑉) = (𝑋(dist‘𝐺)𝑌))
46		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) → 𝑟 ∈ 𝑃)
47	46	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑟 ∈ 𝑃)
48		tgaaddcpbllem1.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑅 ∈ (𝑌𝐿𝑆))
49	4, 24, 5, 7, 30, 48	tglnpt 28869	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑅 ∈ 𝑃)
50	49	ad6antr 749	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) → 𝑅 ∈ 𝑃)
51	50	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑅 ∈ 𝑃)
52		simp-5r 798	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑟(𝐾‘𝑉)𝑇)
53	9	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝐺 ∈ TarskiG)
54	11	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑋 ∈ 𝑃)
55	51	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑅 ∈ 𝑃)
56	23	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑢 ∈ 𝑃)
57	47	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑟 ∈ 𝑃)
58	13	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑌 ∈ 𝑃)
59	20	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑉 ∈ 𝑃)
60		tgaaddcpbl.t	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 ∈ 𝑃)
61	60	ad9antr 755	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑇 ∈ 𝑃)
62	61	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑇 ∈ 𝑃)
63	18	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑈 ∈ 𝑃)
64	25	ad9antr 755	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑆 ∈ 𝑃)
65	64	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑆 ∈ 𝑃)
66	1	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∼ = (cgrA‘𝐺))
67		tgaaddcpbl.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)
68	66, 67	breqdi 5126	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑇”⟩)
69	68	ad9antr 755	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑋𝑌𝑆”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑇”⟩)
70	4, 5, 9, 6, 11, 13, 64, 18, 20, 61, 69	cgracom 29184	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑈𝑉𝑇”⟩(cgrA‘𝐺)⟨“𝑋𝑌𝑆”⟩)
71	70	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → ⟨“𝑈𝑉𝑇”⟩(cgrA‘𝐺)⟨“𝑋𝑌𝑆”⟩)
72		tgaaddcpbllem1.4	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑅(𝐾‘𝑌)𝑆)
73	72	ad10antr 757	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑅(𝐾‘𝑌)𝑆)
74	4, 5, 6, 53, 63, 59, 62, 54, 58, 65, 71, 55, 73	cgrahl2 29179	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → ⟨“𝑈𝑉𝑇”⟩(cgrA‘𝐺)⟨“𝑋𝑌𝑅”⟩)
75	4, 5, 53, 6, 63, 59, 62, 54, 58, 55, 74	cgracom 29184	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → ⟨“𝑋𝑌𝑅”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑇”⟩)
76		simp-9r 806	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑢(𝐾‘𝑉)𝑈)
77	4, 5, 6, 53, 54, 58, 55, 63, 59, 62, 75, 56, 76	cgrahl1 29178	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → ⟨“𝑋𝑌𝑅”⟩(cgrA‘𝐺)⟨“𝑢𝑉𝑇”⟩)
78		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑟(𝐾‘𝑉)𝑇)
79	4, 5, 6, 53, 54, 58, 55, 56, 59, 62, 77, 57, 78	cgrahl2 29179	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → ⟨“𝑋𝑌𝑅”⟩(cgrA‘𝐺)⟨“𝑢𝑉𝑟”⟩)
80	4, 5, 6, 10, 10, 12, 7, 35	hlid 28932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑋(𝐾‘𝑌)𝑋)
81	80	ad9antr 755	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑋(𝐾‘𝑌)𝑋)
82	81	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑋(𝐾‘𝑌)𝑋)
83		tgaaddcpbllem3.1	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑋𝐼𝑍))
84		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑅 = 𝑌) → 𝑅 = 𝑌)
85		tgaaddcpbllem1.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑅 ∈ (𝑋𝐼𝑍))
86	85	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑅 = 𝑌) → 𝑅 ∈ (𝑋𝐼𝑍))
87	84, 86	eqeltrrd 2866	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑅 = 𝑌) → 𝑌 ∈ (𝑋𝐼𝑍))
88	83, 87	mtand 828	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ¬ 𝑅 = 𝑌)
89	88	neqned 2967	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 ≠ 𝑌)
90	89	necomd 3015	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑌 ≠ 𝑅)
91	90	ad10antr 757	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑌 ≠ 𝑅)
92	91	necomd 3015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑅 ≠ 𝑌)
93	4, 5, 6, 55, 54, 58, 53, 92	hlid 28932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑅(𝐾‘𝑌)𝑅)
94	43	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → (𝑌(dist‘𝐺)𝑋) = (𝑉(dist‘𝐺)𝑢))
95		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅))
96	95	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑌(dist‘𝐺)𝑅) = (𝑉(dist‘𝐺)𝑟))
97	96	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → (𝑌(dist‘𝐺)𝑅) = (𝑉(dist‘𝐺)𝑟))
98	4, 5, 6, 53, 54, 58, 55, 56, 59, 57, 79, 54, 28, 55, 82, 93, 94, 97	cgracgr 29180	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → (𝑋(dist‘𝐺)𝑅) = (𝑢(dist‘𝐺)𝑟))
99	4, 28, 5, 53, 54, 55, 56, 57, 98	tgcgrcomlr 28800	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → (𝑅(dist‘𝐺)𝑋) = (𝑟(dist‘𝐺)𝑢))
100	52, 99	mpdan 700	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑅(dist‘𝐺)𝑋) = (𝑟(dist‘𝐺)𝑢))
101	48	ad10antr 757	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑟(𝐾‘𝑉)𝑇) → 𝑅 ∈ (𝑌𝐿𝑆))
102	52, 101	mpdan 700	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑅 ∈ (𝑌𝐿𝑆))
103	32	ad9antr 755	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ¬ 𝑋 ∈ (𝑌𝐿𝑆))
104		nelne2 3058	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) → 𝑅 ≠ 𝑋)
105	102, 103, 104	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑅 ≠ 𝑋)
106	4, 28, 5, 9, 51, 11, 47, 23, 100, 105	tgcgrneq 28803	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑟 ≠ 𝑢)
107	106	necomd 3015	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑢 ≠ 𝑟)
108		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑟 ∈ (𝑢𝐼𝑤))
109	85	ad9antr 755	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑅 ∈ (𝑋𝐼𝑍))
110	100	eqcomd 2771	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑟(dist‘𝐺)𝑢) = (𝑅(dist‘𝐺)𝑋))
111	4, 28, 5, 9, 47, 23, 51, 11, 110	tgcgrcomlr 28800	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑢(dist‘𝐺)𝑟) = (𝑋(dist‘𝐺)𝑅))
112		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍))
113	4, 28, 5, 9, 20, 47, 13, 51, 95	tgcgrcomlr 28800	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑟(dist‘𝐺)𝑉) = (𝑅(dist‘𝐺)𝑌))
114	4, 28, 5, 9, 23, 47, 21, 11, 51, 16, 20, 13, 107, 108, 109, 111, 112, 45, 113	axtg5seg 28785	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑤(dist‘𝐺)𝑉) = (𝑍(dist‘𝐺)𝑌))
115	4, 28, 5, 9, 21, 20, 16, 13, 114	tgcgrcomlr 28800	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍))
116	4, 28, 5, 9, 23, 47, 21, 11, 51, 16, 108, 109, 111, 112	tgcgrextend 28805	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑢(dist‘𝐺)𝑤) = (𝑋(dist‘𝐺)𝑍))
117	4, 28, 5, 9, 23, 21, 11, 16, 116	tgcgrcomlr 28800	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑤(dist‘𝐺)𝑢) = (𝑍(dist‘𝐺)𝑋))
118	4, 28, 41, 9, 23, 20, 21, 11, 13, 16, 45, 115, 117	trgcgr 28836	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑢𝑉𝑤”⟩(cgrG‘𝐺)⟨“𝑋𝑌𝑍”⟩)
119	4, 28, 5, 41, 9, 23, 20, 21, 11, 13, 16, 118	trgcgrcom 28848	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑋𝑌𝑍”⟩(cgrG‘𝐺)⟨“𝑢𝑉𝑤”⟩)
120	4, 5, 9, 6, 11, 13, 16, 23, 20, 21, 36, 40, 119	cgrcgra 29183	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑋𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑢𝑉𝑤”⟩)
121	52, 76	mpdan 700	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑢(𝐾‘𝑉)𝑈)
122	4, 5, 6, 23, 18, 20, 9, 121	hlcomd 28927	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑈(𝐾‘𝑉)𝑢)
123	4, 5, 6, 9, 11, 13, 16, 23, 20, 21, 120, 18, 122	cgrahl1 29178	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑋𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑤”⟩)
124		tgaaddcpbl.w	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
125	124	ad9antr 755	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑊 ∈ 𝑃)
126		eqid 2765	. . . . . . . . . . . 12 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
127		eqid 2765	. . . . . . . . . . . 12 ⊢ ((pInvG‘𝐺)‘𝑇) = ((pInvG‘𝐺)‘𝑇)
128	4, 28, 5, 24, 126, 7, 60, 127, 17	mircl 28989	. . . . . . . . . . 11 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ 𝑃)
129	128	ad9antr 755	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ 𝑃)
130	7	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝐺 ∈ TarskiG)
131	12	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑌 ∈ 𝑃)
132	25	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑆 ∈ 𝑃)
133	14	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑍 ∈ 𝑃)
134	26	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑌 ≠ 𝑆)
135		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑆 ∈ (𝑌𝐿𝑍))
136	39	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑌 ≠ 𝑍)
137	4, 5, 24, 130, 131, 133, 136	tglinecom 28959	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → (𝑌𝐿𝑍) = (𝑍𝐿𝑌))
138	135, 137	eleqtrd 2867	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑆 ∈ (𝑍𝐿𝑌))
139	39	necomd 3015	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ≠ 𝑌)
140	139	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑍 ≠ 𝑌)
141	4, 5, 24, 130, 131, 132, 133, 134, 138, 140	lnrot1 28947	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑍 ∈ (𝑌𝐿𝑆))
142	37, 141	mtand 828	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑆 ∈ (𝑌𝐿𝑍))
143	39	neneqd 2965	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑌 = 𝑍)
144	142, 143	jca 521	. . . . . . . . . . . 12 ⊢ (𝜑 → (¬ 𝑆 ∈ (𝑌𝐿𝑍) ∧ ¬ 𝑌 = 𝑍))
145		ioran 999	. . . . . . . . . . . 12 ⊢ (¬ (𝑆 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍) ↔ (¬ 𝑆 ∈ (𝑌𝐿𝑍) ∧ ¬ 𝑌 = 𝑍))
146	144, 145	sylibr 237	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑆 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))
147	146	ad9antr 755	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ¬ (𝑆 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))
148		tgaaddcpbl.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈𝑄𝑊)
149		tgaaddcpbl.q	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑐𝐼𝑑))}
150	4, 28, 5, 149, 17, 124	islnopp 29071	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈𝑄𝑊 ↔ ((¬ 𝑈 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑊 ∈ (𝑉𝐿𝑇)) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑈𝐼𝑊))))
151	148, 150	mpbid 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((¬ 𝑈 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑊 ∈ (𝑉𝐿𝑇)) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑈𝐼𝑊)))
152	151	simplld 780	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑈 ∈ (𝑉𝐿𝑇))
153	7	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝐺 ∈ TarskiG)
154	60	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝑇 ∈ 𝑃)
155	17	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝑈 ∈ 𝑃)
156	4, 28, 5, 24, 126, 153, 154, 127, 155	mirmir 28990	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘(((pInvG‘𝐺)‘𝑇)‘𝑈)) = 𝑈)
157		tgaaddcpbl.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑉 ≠ 𝑇)
158	4, 5, 24, 7, 19, 60, 157	tgelrnln 28954	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑉𝐿𝑇) ∈ ran 𝐿)
159	158	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (𝑉𝐿𝑇) ∈ ran 𝐿)
160	4, 5, 24, 7, 19, 60, 157	tglinerflx2 28958	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇 ∈ (𝑉𝐿𝑇))
161	160	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝑇 ∈ (𝑉𝐿𝑇))
162	128	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ 𝑃)
163	19	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝑉 ∈ 𝑃)
164		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈)))
165	4, 24, 5, 153, 163, 162, 154, 164	colcom 28878	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (𝑇 ∈ ((((pInvG‘𝐺)‘𝑇)‘𝑈)𝐿𝑉) ∨ (((pInvG‘𝐺)‘𝑇)‘𝑈) = 𝑉))
166	4, 24, 5, 153, 162, 163, 154, 165	colrot1 28879	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → ((((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ (𝑉𝐿𝑇) ∨ 𝑉 = 𝑇))
167	157	neneqd 2965	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝑉 = 𝑇)
168	167	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → ¬ 𝑉 = 𝑇)
169	166, 168	olcnd 891	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ (𝑉𝐿𝑇))
170	4, 28, 5, 24, 126, 153, 127, 159, 161, 169	mirln 29004	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∈ (𝑉𝐿𝑇))
171	156, 170	eqeltrrd 2866	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝑈 ∈ (𝑉𝐿𝑇))
172	152, 171	mtand 828	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈)))
173	172	ad9antr 755	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ¬ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈)))
174		tgaaddcpbl.7	. . . . . . . . . . . 12 ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)
175	66, 174	breqdi 5126	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑊”⟩)
176	175	ad9antr 755	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑊”⟩)
177	52, 92	mpdan 700	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑅 ≠ 𝑌)
178	177	necomd 3015	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑌 ≠ 𝑅)
179	4, 28, 5, 9, 13, 51, 20, 47, 96, 178	tgcgrneq 28803	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑉 ≠ 𝑟)
180	179	necomd 3015	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑟 ≠ 𝑉)
181	115	eqcomd 2771	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑌(dist‘𝐺)𝑍) = (𝑉(dist‘𝐺)𝑤))
182	4, 28, 5, 9, 13, 16, 20, 21, 181, 40	tgcgrneq 28803	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑉 ≠ 𝑤)
183	4, 28, 5, 9, 47, 21, 51, 16, 112	tgcgrcomlr 28800	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑤(dist‘𝐺)𝑟) = (𝑍(dist‘𝐺)𝑅))
184	4, 28, 41, 9, 47, 20, 21, 51, 13, 16, 113, 115, 183	trgcgr 28836	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑟𝑉𝑤”⟩(cgrG‘𝐺)⟨“𝑅𝑌𝑍”⟩)
185	4, 5, 9, 6, 47, 20, 21, 51, 13, 16, 180, 182, 184	cgrcgra 29183	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑟𝑉𝑤”⟩(cgrA‘𝐺)⟨“𝑅𝑌𝑍”⟩)
186	4, 5, 6, 49, 25, 12, 7, 72	hlcomd 28927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆(𝐾‘𝑌)𝑅)
187	186	ad9antr 755	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑆(𝐾‘𝑌)𝑅)
188	4, 5, 6, 9, 47, 20, 21, 51, 13, 16, 185, 64, 187	cgrahl1 29178	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑟𝑉𝑤”⟩(cgrA‘𝐺)⟨“𝑆𝑌𝑍”⟩)
189	4, 5, 9, 6, 47, 20, 21, 64, 13, 16, 188	cgracom 29184	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑟𝑉𝑤”⟩)
190	4, 5, 6, 47, 61, 20, 9, 52	hlcomd 28927	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑇(𝐾‘𝑉)𝑟)
191	4, 5, 6, 9, 64, 13, 16, 47, 20, 21, 189, 61, 190	cgrahl1 29178	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑤”⟩)
192	4, 5, 24, 7, 19, 60, 157	tglinecom 28959	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉𝐿𝑇) = (𝑇𝐿𝑉))
193	192	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝜑 → ((hpG‘𝐺)‘(𝑉𝐿𝑇)) = ((hpG‘𝐺)‘(𝑇𝐿𝑉)))
194	17, 152	eldifd 3917	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ∈ (𝑃 ∖ (𝑉𝐿𝑇)))
195	4, 5, 126, 127, 149, 7, 158, 160, 194, 24	oppmir 29087	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈𝑄(((pInvG‘𝐺)‘𝑇)‘𝑈))
196	4, 28, 5, 149, 24, 158, 7, 17, 128, 195	oppcom 29076	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈)
197	4, 28, 5, 149, 24, 158, 7, 17, 124, 148	oppcom 29076	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊𝑄𝑈)
198	4, 5, 24, 149, 7, 158, 124, 128, 17, 197	lnopp2hpgb 29096	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈 ↔ 𝑊((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈)))
199	196, 198	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈))
200	193, 199	breqdi 5126	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊((hpG‘𝐺)‘(𝑇𝐿𝑉))(((pInvG‘𝐺)‘𝑇)‘𝑈))
201	200	ad9antr 755	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑊((hpG‘𝐺)‘(𝑇𝐿𝑉))(((pInvG‘𝐺)‘𝑇)‘𝑈))
202	193	ad9antr 755	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ((hpG‘𝐺)‘(𝑉𝐿𝑇)) = ((hpG‘𝐺)‘(𝑇𝐿𝑉)))
203	196	ad9antr 755	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈)
204	158	ad9antr 755	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑉𝐿𝑇) ∈ ran 𝐿)
205	4, 5, 6, 47, 61, 20, 9, 24, 52	hlln 28930	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑟 ∈ (𝑇𝐿𝑉))
206	192	ad9antr 755	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑉𝐿𝑇) = (𝑇𝐿𝑉))
207	205, 206	eleqtrrd 2868	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑟 ∈ (𝑉𝐿𝑇))
208		nelne2 3058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → 𝑅 ≠ 𝑍)
209	48, 37, 208	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 ≠ 𝑍)
210	209	neneqd 2965	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ 𝑅 = 𝑍)
211	210	ad9antr 755	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ¬ 𝑅 = 𝑍)
212	9	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝐺 ∈ TarskiG)
213	47	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑟 ∈ 𝑃)
214	21	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ 𝑃)
215	51	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑅 ∈ 𝑃)
216	16	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑍 ∈ 𝑃)
217	112	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍))
218	116	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑋(dist‘𝐺)𝑍) = (𝑢(dist‘𝐺)𝑤))
219	4, 28, 5, 29, 24, 30, 7, 10, 14, 31	oppne3 29075	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑋 ≠ 𝑍)
220	219	ad9antr 755	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑋 ≠ 𝑍)
221	4, 28, 5, 9, 11, 16, 23, 21, 218, 220	tgcgrneq 28803	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑢 ≠ 𝑤)
222	4, 5, 24, 9, 23, 21, 221	tgelrnln 28954	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑢𝐿𝑤) ∈ ran 𝐿)
223	222	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑤) ∈ ran 𝐿)
224	204	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → (𝑉𝐿𝑇) ∈ ran 𝐿)
225	4, 5, 24, 9, 23, 21, 221	tglinerflx1 28957	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑢 ∈ (𝑢𝐿𝑤))
226	9	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝐺 ∈ TarskiG)
227	20	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ 𝑃)
228	61	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑇 ∈ 𝑃)
229	18	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ∈ 𝑃)
230	157	ad10antr 757	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑉 ≠ 𝑇)
231	23	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑢 ∈ 𝑃)
232	34	ad9antr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑌 ≠ 𝑋)
233	4, 28, 5, 9, 13, 11, 20, 23, 43, 232	tgcgrneq 28803	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑉 ≠ 𝑢)
234	233	necomd 3015	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑢 ≠ 𝑉)
235	234	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑢 ≠ 𝑉)
236		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑢 ∈ (𝑉𝐿𝑇))
237	4, 5, 24, 226, 231, 227, 228, 235, 236, 230	lnrot2 28948	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑇 ∈ (𝑢𝐿𝑉))
238	4, 5, 24, 7, 19, 60, 157	tglinerflx1 28957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑉 ∈ (𝑉𝐿𝑇))
239		nelne2 3058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑉 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑈 ∈ (𝑉𝐿𝑇)) → 𝑉 ≠ 𝑈)
240	238, 152, 239	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑉 ≠ 𝑈)
241	240	necomd 3015	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
242	241	ad10antr 757	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ≠ 𝑉)
243	4, 5, 24, 226, 231, 227, 235	tgelrnln 28954	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑉) ∈ ran 𝐿)
244	4, 5, 6, 23, 18, 20, 9, 24, 121	hlln 28930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑢 ∈ (𝑈𝐿𝑉))
245	241	ad9antr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑈 ≠ 𝑉)
246	4, 5, 24, 9, 18, 20, 245	tglinecom 28959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑈𝐿𝑉) = (𝑉𝐿𝑈))
247	244, 246	eleqtrd 2867	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑢 ∈ (𝑉𝐿𝑈))
248	240	ad9antr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑉 ≠ 𝑈)
249	4, 5, 24, 9, 23, 20, 18, 234, 247, 248	lnrot2 28948	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑈 ∈ (𝑢𝐿𝑉))
250	249	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ∈ (𝑢𝐿𝑉))
251	4, 5, 24, 226, 231, 227, 235	tglinerflx2 28958	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ (𝑢𝐿𝑉))
252	4, 5, 24, 226, 229, 227, 242, 242, 243, 250, 251	tglinethru 28960	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑉) = (𝑈𝐿𝑉))
253	237, 252	eleqtrd 2867	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑇 ∈ (𝑈𝐿𝑉))
254	4, 5, 24, 226, 227, 228, 229, 230, 253, 242	lnrot1 28947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ∈ (𝑉𝐿𝑇))
255	152	ad10antr 757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → ¬ 𝑈 ∈ (𝑉𝐿𝑇))
256	254, 255	pm2.65da 829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ¬ 𝑢 ∈ (𝑉𝐿𝑇))
257		nelne1 3057	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 ∈ (𝑢𝐿𝑤) ∧ ¬ 𝑢 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑤) ≠ (𝑉𝐿𝑇))
258	225, 256, 257	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → (𝑢𝐿𝑤) ≠ (𝑉𝐿𝑇))
259	258	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑤) ≠ (𝑉𝐿𝑇))
260	4, 5, 24, 9, 23, 21, 47, 221, 108	btwnlng1 28943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑟 ∈ (𝑢𝐿𝑤))
261	260	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑟 ∈ (𝑢𝐿𝑤))
262	207	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑟 ∈ (𝑉𝐿𝑇))
263	261, 262	elind 4153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑟 ∈ ((𝑢𝐿𝑤) ∩ (𝑉𝐿𝑇)))
264	4, 5, 24, 9, 23, 21, 221	tglinerflx2 28958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑤 ∈ (𝑢𝐿𝑤))
265	264	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ (𝑢𝐿𝑤))
266		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ (𝑉𝐿𝑇))
267	265, 266	elind 4153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ ((𝑢𝐿𝑤) ∩ (𝑉𝐿𝑇)))
268	4, 5, 24, 212, 223, 224, 259, 263, 267	tglineineq 28967	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑟 = 𝑤)
269	4, 28, 5, 212, 213, 214, 215, 216, 217, 268	tgcgreq 28802	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑅 = 𝑍)
270	211, 269	mtand 828	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ¬ 𝑤 ∈ (𝑉𝐿𝑇))
271	4, 28, 5, 9, 23, 47, 21, 108	tgbtwncom 28808	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑟 ∈ (𝑤𝐼𝑢))
272	4, 28, 5, 149, 21, 23, 207, 270, 256, 271	islnoppd 29072	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑤𝑄𝑢)
273	4, 28, 5, 149, 24, 204, 9, 21, 23, 272	oppcom 29076	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑢𝑄𝑤)
274	238	ad9antr 755	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑉 ∈ (𝑉𝐿𝑇))
275	4, 28, 5, 149, 24, 204, 9, 6, 23, 18, 21, 273, 274, 121	opphl 29086	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑈𝑄𝑤)
276	4, 28, 5, 149, 24, 204, 9, 18, 21, 275	oppcom 29076	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑤𝑄𝑈)
277	4, 5, 24, 149, 9, 204, 21, 129, 18, 276	lnopp2hpgb 29096	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ((((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈 ↔ 𝑤((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈)))
278	203, 277	mpbid 235	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑤((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈))
279	202, 278	breqdi 5126	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑤((hpG‘𝐺)‘(𝑇𝐿𝑉))(((pInvG‘𝐺)‘𝑇)‘𝑈))
280	4, 5, 28, 9, 64, 13, 16, 61, 20, 129, 24, 147, 173, 125, 21, 6, 176, 191, 201, 279	acopyeu 29196	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → 𝑊(𝐾‘𝑉)𝑤)
281	4, 5, 6, 9, 11, 13, 16, 18, 20, 21, 123, 125, 280	cgrahl2 29179	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑋𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑊”⟩)
282	3, 281	breqdi 5126	. . . . . . 7 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑟 ∈ (𝑢𝐼𝑤)) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
283	282	anasss 472	. . . . . 6 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) ∧ 𝑤 ∈ 𝑃) ∧ (𝑟 ∈ (𝑢𝐼𝑤) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍))) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
284	4, 28, 5, 8, 22, 46, 50, 15	axtgsegcon 28784	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) → ∃𝑤 ∈ 𝑃 (𝑟 ∈ (𝑢𝐼𝑤) ∧ (𝑟(dist‘𝐺)𝑤) = (𝑅(dist‘𝐺)𝑍)))
285	283, 284	r19.29a 3175	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ 𝑟(𝐾‘𝑉)𝑇) ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
286	285	anasss 472	. . . 4 ⊢ ((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟(𝐾‘𝑉)𝑇 ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅))) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
287	157	necomd 3015	. . . . . 6 ⊢ (𝜑 → 𝑇 ≠ 𝑉)
288	4, 5, 6, 19, 12, 49, 7, 60, 28, 287, 90	hlcgrex 28939	. . . . 5 ⊢ (𝜑 → ∃𝑟 ∈ 𝑃 (𝑟(𝐾‘𝑉)𝑇 ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)))
289	288	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → ∃𝑟 ∈ 𝑃 (𝑟(𝐾‘𝑉)𝑇 ∧ (𝑉(dist‘𝐺)𝑟) = (𝑌(dist‘𝐺)𝑅)))
290	286, 289	r19.29a 3175	. . 3 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑢(𝐾‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
291	290	anasss 472	. 2 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ (𝑢(𝐾‘𝑉)𝑈 ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋))) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
292	4, 5, 6, 19, 12, 10, 7, 17, 28, 241, 34	hlcgrex 28939	. 2 ⊢ (𝜑 → ∃𝑢 ∈ 𝑃 (𝑢(𝐾‘𝑉)𝑈 ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)))
293	291, 292	r19.29a 3175	1 ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∃wrex 3091 ∖ cdif 3903 class class class wbr 5111 {copab 5175 ran crn 5664 ‘cfv 6540 (class class class)co 7419 ⟨“cs3 14903 Basecbs 17291 distcds 17341 TarskiGcstrkg 28747 Itvcitv 28753 LineGclng 28754 cgrGccgrg 28830 hlGchlg 28920 pInvGcmir 28980 hpGchpg 29090 cgrAccgra 29169

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 ax-pre-mulgt0 11192

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 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 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-oadd 8463 df-er 8700 df-map 8832 df-pm 8833 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-dju 9903 df-card 9941 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-sub 11458 df-neg 11459 df-nn 12249 df-2 12318 df-3 12319 df-n0 12520 df-xnn0 12593 df-z 12607 df-uz 12879 df-fz 13552 df-fzo 13700 df-hash 14385 df-word 14569 df-concat 14626 df-s1 14653 df-s2 14909 df-s3 14910 df-trkgc 28768 df-trkgb 28769 df-trkgcb 28770 df-trkgld 28772 df-trkg 28773 df-cgrg 28831 df-leg 28903 df-hlg 28921 df-mir 28981 df-rag 29025 df-perpg 29027 df-hpg 29091 df-mid 29134 df-lmi 29135 df-cgra 29170

This theorem is used by: tgaaddcpbllem2 29204 tgaaddcpbllem3 29205

W3C validator