tgaaddcpbl - Metamath Proof Explorer

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

Theorem tgaaddcpbl 29359

Description: The angular addition is compatible with angle congruence: by adding congruent angles together, we obtain congruent angles. Theorem 11.22 of [Schwabhauser] p. 99. The angles ⟨“𝑋𝑌𝑆”⟩ and ⟨“𝑆𝑌𝑍”⟩ are added to result in ⟨“𝑋𝑌𝑍”⟩, and ⟨“𝑈𝑉𝑇”⟩ and ⟨“𝑇𝑉𝑊”⟩ are added to result in ⟨“𝑈𝑉𝑊”⟩. (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	⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)

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

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

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

Step	Hyp	Ref	Expression
1		tgaaddcpbl.c	. . . . . . . . 9 ⊢ ∼ = (cgrA‘𝐺)
2	1	a1i 11	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ∼ = (cgrA‘𝐺))
3	2	eqcomd 2766	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → (cgrA‘𝐺) = ∼ )
4		tgaaddcpbl.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
5		tgaaddcpbl.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
6		eqid 2760	. . . . . . . 8 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
7		tgaaddcpbl.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
8	7	ad4antr 745	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝐺 ∈ TarskiG)
9	8	ad3antrrr 743	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝐺 ∈ TarskiG)
10		tgaaddcpbl.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
11	10	ad7antr 751	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑋 ∈ 𝑃)
12		tgaaddcpbl.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
13	12	ad4antr 745	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑌 ∈ 𝑃)
14	13	ad3antrrr 743	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑌 ∈ 𝑃)
15		tgaaddcpbl.z	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
16	15	ad4antr 745	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑍 ∈ 𝑃)
17	16	ad3antrrr 743	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑍 ∈ 𝑃)
18		tgaaddcpbl.u	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ 𝑃)
19	18	ad7antr 751	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑈 ∈ 𝑃)
20		tgaaddcpbl.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ 𝑃)
21	20	ad4antr 745	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑉 ∈ 𝑃)
22	21	ad3antrrr 743	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑉 ∈ 𝑃)
23		simpllr 788	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑤 ∈ 𝑃)
24		eqid 2760	. . . . . . . . 9 ⊢ (dist‘𝐺) = (dist‘𝐺)
25		simp-7r 802	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑌 ∈ (𝑋𝐼𝑍))
26		simpllr 788	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑢 ∈ 𝑃)
27	26	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑢 ∈ 𝑃)
28		simp-5r 798	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑢((hlG‘𝐺)‘𝑉)𝑈)
29		simplr 781	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑉 ∈ (𝑢𝐼𝑤))
30	4, 5, 6, 27, 19, 23, 9, 22, 28, 29	btwnhl 29087	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑉 ∈ (𝑈𝐼𝑤))
31		tgaaddcpbl.l	. . . . . . . . . . . . 13 ⊢ 𝐿 = (LineG‘𝐺)
32		tgaaddcpbl.s	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ 𝑃)
33		tgaaddcpbl.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ≠ 𝑆)
34	4, 5, 31, 7, 12, 32, 33	tglinerflx1 29108	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ (𝑌𝐿𝑆))
35		tgaaddcpbl.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))}
36	4, 5, 31, 7, 12, 32, 33	tgelrnln 29105	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌𝐿𝑆) ∈ ran 𝐿)
37		tgaaddcpbl.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋𝑂𝑍)
38	4, 24, 5, 35, 31, 36, 7, 10, 15, 37	oppne1 29224	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑆))
39		nelne2 3053	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) → 𝑌 ≠ 𝑋)
40	34, 38, 39	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
41	40	necomd 3010	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
42	41	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑋 ≠ 𝑌)
43	4, 24, 5, 35, 31, 36, 7, 10, 15, 37	oppne2 29225	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑌𝐿𝑆))
44		nelne2 3053	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → 𝑌 ≠ 𝑍)
45	34, 43, 44	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑍)
46	45	necomd 3010	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ≠ 𝑌)
47	46	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑍 ≠ 𝑌)
48		tgaaddcpbl.t	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ 𝑃)
49		tgaaddcpbl.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑉 ≠ 𝑇)
50	4, 5, 31, 7, 20, 48, 49	tglinerflx1 29108	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ∈ (𝑉𝐿𝑇))
51		tgaaddcpbl.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈𝑄𝑊)
52		tgaaddcpbl.q	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑐𝐼𝑑))}
53		tgaaddcpbl.w	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
54	4, 24, 5, 52, 18, 53	islnopp 29222	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈𝑄𝑊 ↔ ((¬ 𝑈 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑊 ∈ (𝑉𝐿𝑇)) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑈𝐼𝑊))))
55	51, 54	mpbid 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((¬ 𝑈 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑊 ∈ (𝑉𝐿𝑇)) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑈𝐼𝑊)))
56	55	simplld 780	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑈 ∈ (𝑉𝐿𝑇))
57		nelne2 3053	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑈 ∈ (𝑉𝐿𝑇)) → 𝑉 ≠ 𝑈)
58	50, 56, 57	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ≠ 𝑈)
59	58	necomd 3010	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
60	59	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑈 ≠ 𝑉)
61		simpr 490	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍))
62	61	eqcomd 2766	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → (𝑌(dist‘𝐺)𝑍) = (𝑉(dist‘𝐺)𝑤))
63	45	ad7antr 751	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑌 ≠ 𝑍)
64	4, 24, 5, 9, 14, 17, 22, 23, 62, 63	tgcgrneq 28952	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑉 ≠ 𝑤)
65	64	necomd 3010	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑤 ≠ 𝑉)
66	4, 5, 24, 9, 11, 14, 17, 19, 22, 23, 25, 30, 42, 47, 60, 65	flatcgra 29339	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑋𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑤”⟩)
67	53	ad7antr 751	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑊 ∈ 𝑃)
68	32	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑆 ∈ 𝑃)
69	48	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑇 ∈ 𝑃)
70		eqid 2760	. . . . . . . . . . 11 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
71		eqid 2760	. . . . . . . . . . 11 ⊢ ((pInvG‘𝐺)‘𝑇) = ((pInvG‘𝐺)‘𝑇)
72	4, 24, 5, 31, 70, 7, 48, 71, 18	mircl 29140	. . . . . . . . . 10 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ 𝑃)
73	72	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → (((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ 𝑃)
74	7	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝐺 ∈ TarskiG)
75	12	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑌 ∈ 𝑃)
76	32	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑆 ∈ 𝑃)
77	15	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑍 ∈ 𝑃)
78	33	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑌 ≠ 𝑆)
79		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑆 ∈ (𝑌𝐿𝑍))
80	45	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑌 ≠ 𝑍)
81	4, 5, 31, 74, 75, 77, 80	tglinecom 29110	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → (𝑌𝐿𝑍) = (𝑍𝐿𝑌))
82	79, 81	eleqtrd 2862	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑆 ∈ (𝑍𝐿𝑌))
83	46	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑍 ≠ 𝑌)
84	4, 5, 31, 74, 75, 76, 77, 78, 82, 83	lnrot1 29098	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑍 ∈ (𝑌𝐿𝑆))
85	43, 84	mtand 828	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑆 ∈ (𝑌𝐿𝑍))
86	45	neneqd 2960	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑌 = 𝑍)
87		ioran 999	. . . . . . . . . . 11 ⊢ (¬ (𝑆 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍) ↔ (¬ 𝑆 ∈ (𝑌𝐿𝑍) ∧ ¬ 𝑌 = 𝑍))
88	85, 86, 87	sylanbrc 595	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝑆 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))
89	88	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ¬ (𝑆 ∈ (𝑌𝐿𝑍) ∨ 𝑌 = 𝑍))
90	7	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝐺 ∈ TarskiG)
91	48	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝑇 ∈ 𝑃)
92	18	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝑈 ∈ 𝑃)
93	4, 24, 5, 31, 70, 90, 91, 71, 92	mirmir 29141	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘(((pInvG‘𝐺)‘𝑇)‘𝑈)) = 𝑈)
94	4, 5, 31, 7, 20, 48, 49	tgelrnln 29105	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉𝐿𝑇) ∈ ran 𝐿)
95	94	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (𝑉𝐿𝑇) ∈ ran 𝐿)
96	4, 5, 31, 7, 20, 48, 49	tglinerflx2 29109	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ (𝑉𝐿𝑇))
97	96	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝑇 ∈ (𝑉𝐿𝑇))
98	72	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ 𝑃)
99	20	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝑉 ∈ 𝑃)
100		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈)))
101	4, 31, 5, 90, 99, 98, 91, 100	colcom 29028	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (𝑇 ∈ ((((pInvG‘𝐺)‘𝑇)‘𝑈)𝐿𝑉) ∨ (((pInvG‘𝐺)‘𝑇)‘𝑈) = 𝑉))
102	4, 31, 5, 90, 98, 99, 91, 101	colrot1 29029	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → ((((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ (𝑉𝐿𝑇) ∨ 𝑉 = 𝑇))
103	49	neneqd 2960	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ 𝑉 = 𝑇)
104	103	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → ¬ 𝑉 = 𝑇)
105	102, 104	olcnd 891	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ (𝑉𝐿𝑇))
106	4, 24, 5, 31, 70, 90, 71, 95, 97, 105	mirln 29155	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∈ (𝑉𝐿𝑇))
107	93, 106	eqeltrrd 2861	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → 𝑈 ∈ (𝑉𝐿𝑇))
108	56, 107	mtand 828	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈)))
109	108	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ¬ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈)))
110	1	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ∼ = (cgrA‘𝐺))
111		tgaaddcpbl.7	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)
112	110, 111	breqdi 5117	. . . . . . . . . 10 ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑊”⟩)
113	112	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑊”⟩)
114		tgaaddcpbl.6	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)
115	110, 114	breqdi 5117	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑇”⟩)
116	4, 5, 7, 6, 10, 12, 32, 18, 20, 48, 115	cgracom 29336	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⟨“𝑈𝑉𝑇”⟩(cgrA‘𝐺)⟨“𝑋𝑌𝑆”⟩)
117	116	ad7antr 751	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑈𝑉𝑇”⟩(cgrA‘𝐺)⟨“𝑋𝑌𝑆”⟩)
118	4, 5, 24, 9, 19, 22, 69, 11, 14, 68, 23, 17, 117, 30, 25, 64, 63	sacgr 29346	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑤𝑉𝑇”⟩(cgrA‘𝐺)⟨“𝑍𝑌𝑆”⟩)
119	4, 5, 24, 9, 23, 22, 69, 17, 14, 68, 118	cgraswaplr 29340	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑇𝑉𝑤”⟩(cgrA‘𝐺)⟨“𝑆𝑌𝑍”⟩)
120	4, 5, 9, 6, 69, 22, 23, 68, 14, 17, 119	cgracom 29336	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑤”⟩)
121	4, 5, 31, 7, 20, 48, 49	tglinecom 29110	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉𝐿𝑇) = (𝑇𝐿𝑉))
122	121	fveq2d 6892	. . . . . . . . . . 11 ⊢ (𝜑 → ((hpG‘𝐺)‘(𝑉𝐿𝑇)) = ((hpG‘𝐺)‘(𝑇𝐿𝑉)))
123	18, 56	eldifd 4049	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ (𝑃 ∖ (𝑉𝐿𝑇)))
124	4, 5, 70, 71, 52, 7, 94, 96, 123, 31	oppmir 29239	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈𝑄(((pInvG‘𝐺)‘𝑇)‘𝑈))
125	4, 24, 5, 52, 31, 94, 7, 18, 72, 124	oppcom 29227	. . . . . . . . . . . 12 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈)
126	4, 24, 5, 52, 31, 94, 7, 18, 53, 51	oppcom 29227	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊𝑄𝑈)
127	4, 5, 31, 52, 7, 94, 53, 72, 18, 126	lnopp2hpgb 29248	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈 ↔ 𝑊((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈)))
128	125, 127	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈))
129	122, 128	breqdi 5117	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊((hpG‘𝐺)‘(𝑇𝐿𝑉))(((pInvG‘𝐺)‘𝑇)‘𝑈))
130	129	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑊((hpG‘𝐺)‘(𝑇𝐿𝑉))(((pInvG‘𝐺)‘𝑇)‘𝑈))
131	122	ad7antr 751	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ((hpG‘𝐺)‘(𝑉𝐿𝑇)) = ((hpG‘𝐺)‘(𝑇𝐿𝑉)))
132	125	ad7antr 751	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → (((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈)
133	94	ad7antr 751	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → (𝑉𝐿𝑇) ∈ ran 𝐿)
134	50	ad7antr 751	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑉 ∈ (𝑉𝐿𝑇))
135	8	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝐺 ∈ TarskiG)
136	21	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ 𝑃)
137	48	ad5antr 747	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑇 ∈ 𝑃)
138	18	ad5antr 747	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ∈ 𝑃)
139	49	ad5antr 747	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑉 ≠ 𝑇)
140	26	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑢 ∈ 𝑃)
141	10	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑋 ∈ 𝑃)
142		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋))
143	142	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → (𝑌(dist‘𝐺)𝑋) = (𝑉(dist‘𝐺)𝑢))
144	40	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑌 ≠ 𝑋)
145	4, 24, 5, 8, 13, 141, 21, 26, 143, 144	tgcgrneq 28952	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑉 ≠ 𝑢)
146	145	necomd 3010	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑢 ≠ 𝑉)
147	146	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑢 ≠ 𝑉)
148		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑢 ∈ (𝑉𝐿𝑇))
149	4, 5, 31, 135, 140, 136, 137, 147, 148, 139	lnrot2 29099	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑇 ∈ (𝑢𝐿𝑉))
150	59	ad5antr 747	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ≠ 𝑉)
151	4, 5, 31, 135, 140, 136, 147	tgelrnln 29105	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑉) ∈ ran 𝐿)
152	18	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑈 ∈ 𝑃)
153		simplr 781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑢((hlG‘𝐺)‘𝑉)𝑈)
154	4, 5, 6, 26, 152, 21, 8, 153	hlcomd 29077	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑈((hlG‘𝐺)‘𝑉)𝑢)
155	4, 5, 6, 152, 26, 21, 8, 31, 154	hlln 29080	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑈 ∈ (𝑢𝐿𝑉))
156	155	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ∈ (𝑢𝐿𝑉))
157	4, 5, 31, 135, 140, 136, 147	tglinerflx2 29109	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ (𝑢𝐿𝑉))
158	4, 5, 31, 135, 138, 136, 150, 150, 151, 156, 157	tglinethru 29111	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑉) = (𝑈𝐿𝑉))
159	149, 158	eleqtrd 2862	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑇 ∈ (𝑈𝐿𝑉))
160	4, 5, 31, 135, 136, 137, 138, 139, 159, 150	lnrot1 29098	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ∈ (𝑉𝐿𝑇))
161	56	ad5antr 747	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → ¬ 𝑈 ∈ (𝑉𝐿𝑇))
162	160, 161	pm2.65da 829	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → ¬ 𝑢 ∈ (𝑉𝐿𝑇))
163	162	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ¬ 𝑢 ∈ (𝑉𝐿𝑇))
164	64	neneqd 2960	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ¬ 𝑉 = 𝑤)
165	9	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝐺 ∈ TarskiG)
166	27	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑢 ∈ 𝑃)
167	23	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ 𝑃)
168	9	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝐺 ∈ TarskiG)
169	23	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑤 ∈ 𝑃)
170	22	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑉 ∈ 𝑃)
171		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑉 ∈ (𝑢𝐼𝑤))
172		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑢 = 𝑤)
173	172	oveq1d 7437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → (𝑢𝐼𝑤) = (𝑤𝐼𝑤))
174	171, 173	eleqtrd 2862	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑉 ∈ (𝑤𝐼𝑤))
175	4, 24, 5, 168, 169, 170, 174	axtgbtwnid 28935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑤 = 𝑉)
176	175	eqcomd 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑉 = 𝑤)
177	64, 176	mteqand 3046	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑢 ≠ 𝑤)
178	177	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑢 ≠ 𝑤)
179	4, 5, 31, 165, 166, 167, 178	tgelrnln 29105	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑤) ∈ ran 𝐿)
180	133	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → (𝑉𝐿𝑇) ∈ ran 𝐿)
181	4, 5, 31, 165, 166, 167, 178	tglinerflx1 29108	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑢 ∈ (𝑢𝐿𝑤))
182	163	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → ¬ 𝑢 ∈ (𝑉𝐿𝑇))
183		nelne1 3052	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ (𝑢𝐿𝑤) ∧ ¬ 𝑢 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑤) ≠ (𝑉𝐿𝑇))
184	181, 182, 183	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑤) ≠ (𝑉𝐿𝑇))
185	22	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ 𝑃)
186		simpllr 788	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ (𝑢𝐼𝑤))
187	4, 5, 31, 165, 166, 167, 185, 178, 186	btwnlng1 29094	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ (𝑢𝐿𝑤))
188	134	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ (𝑉𝐿𝑇))
189	187, 188	elind 4096	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ ((𝑢𝐿𝑤) ∩ (𝑉𝐿𝑇)))
190	4, 5, 31, 165, 166, 167, 178	tglinerflx2 29109	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ (𝑢𝐿𝑤))
191		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ (𝑉𝐿𝑇))
192	190, 191	elind 4096	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ ((𝑢𝐿𝑤) ∩ (𝑉𝐿𝑇)))
193	4, 5, 31, 165, 179, 180, 184, 189, 192	tglineineq 29118	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 = 𝑤)
194	164, 193	mtand 828	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ¬ 𝑤 ∈ (𝑉𝐿𝑇))
195	4, 24, 5, 52, 27, 23, 134, 163, 194, 29	islnoppd 29223	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑢𝑄𝑤)
196	4, 24, 5, 52, 31, 133, 9, 6, 27, 19, 23, 195, 134, 28	opphl 29237	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑈𝑄𝑤)
197	4, 24, 5, 52, 31, 133, 9, 19, 23, 196	oppcom 29227	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑤𝑄𝑈)
198	4, 5, 31, 52, 9, 133, 23, 73, 19, 197	lnopp2hpgb 29248	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ((((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈 ↔ 𝑤((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈)))
199	132, 198	mpbid 235	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑤((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈))
200	131, 199	breqdi 5117	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑤((hpG‘𝐺)‘(𝑇𝐿𝑉))(((pInvG‘𝐺)‘𝑇)‘𝑈))
201	4, 5, 24, 9, 68, 14, 17, 69, 22, 73, 31, 89, 109, 67, 23, 6, 113, 120, 130, 200	acopyeu 29349	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑊((hlG‘𝐺)‘𝑉)𝑤)
202	4, 5, 6, 9, 11, 14, 17, 19, 22, 23, 66, 67, 201	cgrahl2 29331	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑋𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑊”⟩)
203	3, 202	breqdi 5117	. . . . . 6 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
204	203	anasss 472	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ (𝑉 ∈ (𝑢𝐼𝑤) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍))) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
205	4, 24, 5, 8, 26, 21, 13, 16	axtgsegcon 28933	. . . . 5 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → ∃𝑤 ∈ 𝑃 (𝑉 ∈ (𝑢𝐼𝑤) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)))
206	204, 205	r19.29a 3170	. . . 4 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
207	206	anasss 472	. . 3 ⊢ ((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ (𝑢((hlG‘𝐺)‘𝑉)𝑈 ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋))) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
208	4, 5, 6, 20, 12, 10, 7, 18, 24, 59, 40	hlcgrex 29089	. . . 4 ⊢ (𝜑 → ∃𝑢 ∈ 𝑃 (𝑢((hlG‘𝐺)‘𝑉)𝑈 ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)))
209	208	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → ∃𝑢 ∈ 𝑃 (𝑢((hlG‘𝐺)‘𝑉)𝑈 ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)))
210	207, 209	r19.29a 3170	. 2 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
211	7	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐺 ∈ TarskiG)
212	32	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑆 ∈ 𝑃)
213	48	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑇 ∈ 𝑃)
214	18	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑈 ∈ 𝑃)
215	20	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑉 ∈ 𝑃)
216	53	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑊 ∈ 𝑃)
217	10	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑋 ∈ 𝑃)
218	12	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑌 ∈ 𝑃)
219	15	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑍 ∈ 𝑃)
220	33	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑌 ≠ 𝑆)
221	49	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑉 ≠ 𝑇)
222	37	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑋𝑂𝑍)
223	51	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑈𝑄𝑊)
224	114	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)
225	111	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)
226		simpr 490	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → ¬ 𝑌 ∈ (𝑋𝐼𝑍))
227	4, 5, 31, 1, 35, 52, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226	tgaaddcpbllem3 29358	. 2 ⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑋𝐼𝑍)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
228	210, 227	pm2.61dan 825	1 ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∨ wo 861 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∃wrex 3086 ∖ cdif 4044 class class class wbr 5102 {copab 5166 ran crn 5651 ‘cfv 6541 (class class class)co 7422 ⟨“cs3 14999 Basecbs 17394 distcds 17444 TarskiGcstrkg 28896 Itvcitv 28902 LineGclng 28903 hlGchlg 29070 pInvGcmir 29131 hpGchpg 29242 cgrAccgra 29321

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7753 ax-cnex 11261 ax-resscn 11262 ax-1cn 11263 ax-icn 11264 ax-addcl 11265 ax-addrcl 11266 ax-mulcl 11267 ax-mulrcl 11268 ax-mulcom 11269 ax-addass 11270 ax-mulass 11271 ax-distr 11272 ax-i2m1 11273 ax-1ne0 11274 ax-1rid 11275 ax-rnegex 11276 ax-rrecex 11277 ax-cnre 11278 ax-pre-lttri 11279 ax-pre-lttrn 11280 ax-pre-ltadd 11281 ax-pre-mulgt0 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7379 df-ov 7425 df-oprab 7426 df-mpo 7427 df-om 7880 df-1st 8003 df-2nd 8004 df-frecs 8304 df-wrecs 8335 df-recs 8384 df-rdg 8423 df-1o 8481 df-oadd 8485 df-er 8722 df-map 8854 df-pm 8855 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-dju 9987 df-card 10025 df-pnf 11350 df-mnf 11351 df-xr 11352 df-ltxr 11353 df-le 11354 df-sub 11548 df-neg 11549 df-nn 12341 df-2 12410 df-3 12411 df-n0 12612 df-xnn0 12685 df-z 12699 df-uz 12971 df-fz 13645 df-fzo 13794 df-hash 14480 df-word 14664 df-concat 14721 df-s1 14748 df-s2 15005 df-s3 15006 df-trkgc 28917 df-trkgb 28918 df-trkgcb 28919 df-trkgld 28921 df-trkg 28922 df-cgrg 28981 df-leg 29053 df-hlg 29071 df-mir 29132 df-rag 29176 df-perpg 29178 df-hpg 29243 df-mid 29286 df-lmi 29287 df-cgra 29322

This theorem is used by: tgaaddcpbl2 29360

W3C validator