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 29409

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 2769	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → (cgrA‘𝐺) = ∼ )
4		tgaaddcpbl.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
5		tgaaddcpbl.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
6		eqid 2763	. . . . . . . 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 2763	. . . . . . . . 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 29137	. . . . . . . . 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 29158	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ (𝑌𝐿𝑆))
35		tgaaddcpbl.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))}
36	4, 5, 31, 7, 12, 32, 33	tgelrnln 29155	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌𝐿𝑆) ∈ ran 𝐿)
37		tgaaddcpbl.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋𝑂𝑍)
38	4, 24, 5, 35, 31, 36, 7, 10, 15, 37	oppne1 29274	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑆))
39		nelne2 3057	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) → 𝑌 ≠ 𝑋)
40	34, 38, 39	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
41	40	necomd 3014	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
42	41	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑋 ≠ 𝑌)
43	4, 24, 5, 35, 31, 36, 7, 10, 15, 37	oppne2 29275	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑌𝐿𝑆))
44		nelne2 3057	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → 𝑌 ≠ 𝑍)
45	34, 43, 44	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑍)
46	45	necomd 3014	. . . . . . . . . 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 29158	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ∈ (𝑉𝐿𝑇))
51		tgaaddcpbl.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈𝑄𝑊)
52		tgaaddcpbl.q	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑐𝐼𝑑))}
53		tgaaddcpbl.w	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
54	4, 24, 5, 52, 18, 53	islnopp 29272	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈𝑄𝑊 ↔ ((¬ 𝑈 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑊 ∈ (𝑉𝐿𝑇)) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑈𝐼𝑊))))
55	51, 54	mpbid 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((¬ 𝑈 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑊 ∈ (𝑉𝐿𝑇)) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑈𝐼𝑊)))
56	55	simplld 780	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑈 ∈ (𝑉𝐿𝑇))
57		nelne2 3057	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑈 ∈ (𝑉𝐿𝑇)) → 𝑉 ≠ 𝑈)
58	50, 56, 57	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ≠ 𝑈)
59	58	necomd 3014	. . . . . . . . . 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 2769	. . . . . . . . . . 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 29002	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑉 ≠ 𝑤)
65	64	necomd 3014	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑤 ≠ 𝑉)
66	4, 5, 24, 9, 11, 14, 17, 19, 22, 23, 25, 30, 42, 47, 60, 65	flatcgra 29389	. . . . . . . 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 2763	. . . . . . . . . . 11 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
71		eqid 2763	. . . . . . . . . . 11 ⊢ ((pInvG‘𝐺)‘𝑇) = ((pInvG‘𝐺)‘𝑇)
72	4, 24, 5, 31, 70, 7, 48, 71, 18	mircl 29190	. . . . . . . . . 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 29160	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → (𝑌𝐿𝑍) = (𝑍𝐿𝑌))
82	79, 81	eleqtrd 2866	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑆 ∈ (𝑍𝐿𝑌))
83	46	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑍 ≠ 𝑌)
84	4, 5, 31, 74, 75, 76, 77, 78, 82, 83	lnrot1 29148	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑍 ∈ (𝑌𝐿𝑆))
85	43, 84	mtand 828	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑆 ∈ (𝑌𝐿𝑍))
86	45	neneqd 2964	. . . . . . . . . . 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 29191	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘(((pInvG‘𝐺)‘𝑇)‘𝑈)) = 𝑈)
94	4, 5, 31, 7, 20, 48, 49	tgelrnln 29155	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉𝐿𝑇) ∈ ran 𝐿)
95	94	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (𝑉𝐿𝑇) ∈ ran 𝐿)
96	4, 5, 31, 7, 20, 48, 49	tglinerflx2 29159	. . . . . . . . . . . . . 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 29078	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (𝑇 ∈ ((((pInvG‘𝐺)‘𝑇)‘𝑈)𝐿𝑉) ∨ (((pInvG‘𝐺)‘𝑇)‘𝑈) = 𝑉))
102	4, 31, 5, 90, 98, 99, 91, 101	colrot1 29079	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → ((((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ (𝑉𝐿𝑇) ∨ 𝑉 = 𝑇))
103	49	neneqd 2964	. . . . . . . . . . . . . . 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 29205	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∈ (𝑉𝐿𝑇))
107	93, 106	eqeltrrd 2865	. . . . . . . . . . 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 5123	. . . . . . . . . 10 ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑊”⟩)
113	112	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑊”⟩)
114		tgaaddcpbl.6	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)
115	110, 114	breqdi 5123	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑇”⟩)
116	4, 5, 7, 6, 10, 12, 32, 18, 20, 48, 115	cgracom 29386	. . . . . . . . . . . . 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 29396	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑤𝑉𝑇”⟩(cgrA‘𝐺)⟨“𝑍𝑌𝑆”⟩)
119	4, 5, 24, 9, 23, 22, 69, 17, 14, 68, 118	cgraswaplr 29390	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑇𝑉𝑤”⟩(cgrA‘𝐺)⟨“𝑆𝑌𝑍”⟩)
120	4, 5, 9, 6, 69, 22, 23, 68, 14, 17, 119	cgracom 29386	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑤”⟩)
121	4, 5, 31, 7, 20, 48, 49	tglinecom 29160	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉𝐿𝑇) = (𝑇𝐿𝑉))
122	121	fveq2d 6920	. . . . . . . . . . 11 ⊢ (𝜑 → ((hpG‘𝐺)‘(𝑉𝐿𝑇)) = ((hpG‘𝐺)‘(𝑇𝐿𝑉)))
123	18, 56	eldifd 4053	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ (𝑃 ∖ (𝑉𝐿𝑇)))
124	4, 5, 70, 71, 52, 7, 94, 96, 123, 31	oppmir 29289	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈𝑄(((pInvG‘𝐺)‘𝑇)‘𝑈))
125	4, 24, 5, 52, 31, 94, 7, 18, 72, 124	oppcom 29277	. . . . . . . . . . . 12 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈)
126	4, 24, 5, 52, 31, 94, 7, 18, 53, 51	oppcom 29277	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊𝑄𝑈)
127	4, 5, 31, 52, 7, 94, 53, 72, 18, 126	lnopp2hpgb 29298	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈 ↔ 𝑊((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈)))
128	125, 127	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈))
129	122, 128	breqdi 5123	. . . . . . . . . 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 2769	. . . . . . . . . . . . . . . . . . . . . . 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 29002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑉 ≠ 𝑢)
146	145	necomd 3014	. . . . . . . . . . . . . . . . . . . . 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 29149	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑇 ∈ (𝑢𝐿𝑉))
150	59	ad5antr 747	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ≠ 𝑉)
151	4, 5, 31, 135, 140, 136, 147	tgelrnln 29155	. . . . . . . . . . . . . . . . . . . 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 29127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑈((hlG‘𝐺)‘𝑉)𝑢)
155	4, 5, 6, 152, 26, 21, 8, 31, 154	hlln 29130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑈 ∈ (𝑢𝐿𝑉))
156	155	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ∈ (𝑢𝐿𝑉))
157	4, 5, 31, 135, 140, 136, 147	tglinerflx2 29159	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ (𝑢𝐿𝑉))
158	4, 5, 31, 135, 138, 136, 150, 150, 151, 156, 157	tglinethru 29161	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑉) = (𝑈𝐿𝑉))
159	149, 158	eleqtrd 2866	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑇 ∈ (𝑈𝐿𝑉))
160	4, 5, 31, 135, 136, 137, 138, 139, 159, 150	lnrot1 29148	. . . . . . . . . . . . . . . . 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 2964	. . . . . . . . . . . . . . . 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 7466	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → (𝑢𝐼𝑤) = (𝑤𝐼𝑤))
174	171, 173	eleqtrd 2866	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑉 ∈ (𝑤𝐼𝑤))
175	4, 24, 5, 168, 169, 170, 174	axtgbtwnid 28985	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑤 = 𝑉)
176	175	eqcomd 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑉 = 𝑤)
177	64, 176	mteqand 3050	. . . . . . . . . . . . . . . . . . 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 29155	. . . . . . . . . . . . . . . . 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 29158	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑢 ∈ (𝑢𝐿𝑤))
182	163	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → ¬ 𝑢 ∈ (𝑉𝐿𝑇))
183		nelne1 3056	. . . . . . . . . . . . . . . . . 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 29144	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ (𝑢𝐿𝑤))
188	134	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ (𝑉𝐿𝑇))
189	187, 188	elind 4100	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ ((𝑢𝐿𝑤) ∩ (𝑉𝐿𝑇)))
190	4, 5, 31, 165, 166, 167, 178	tglinerflx2 29159	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ (𝑢𝐿𝑤))
191		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ (𝑉𝐿𝑇))
192	190, 191	elind 4100	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ ((𝑢𝐿𝑤) ∩ (𝑉𝐿𝑇)))
193	4, 5, 31, 165, 179, 180, 184, 189, 192	tglineineq 29168	. . . . . . . . . . . . . . . 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 29273	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑢𝑄𝑤)
196	4, 24, 5, 52, 31, 133, 9, 6, 27, 19, 23, 195, 134, 28	opphl 29287	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑈𝑄𝑤)
197	4, 24, 5, 52, 31, 133, 9, 19, 23, 196	oppcom 29277	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑤𝑄𝑈)
198	4, 5, 31, 52, 9, 133, 23, 73, 19, 197	lnopp2hpgb 29298	. . . . . . . . . . 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 5123	. . . . . . . . 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 29399	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑊((hlG‘𝐺)‘𝑉)𝑤)
202	4, 5, 6, 9, 11, 14, 17, 19, 22, 23, 66, 67, 201	cgrahl2 29381	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑋𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑊”⟩)
203	3, 202	breqdi 5123	. . . . . 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 28983	. . . . 5 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → ∃𝑤 ∈ 𝑃 (𝑉 ∈ (𝑢𝐼𝑤) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)))
206	204, 205	r19.29a 3174	. . . 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 29139	. . . 4 ⊢ (𝜑 → ∃𝑢 ∈ 𝑃 (𝑢((hlG‘𝐺)‘𝑉)𝑈 ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)))
209	208	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → ∃𝑢 ∈ 𝑃 (𝑢((hlG‘𝐺)‘𝑉)𝑈 ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)))
210	207, 209	r19.29a 3174	. 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 29408	. 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 1570 ∈ wcel 2147 ≠ wne 2959 ∃wrex 3090 ∖ cdif 4048 class class class wbr 5108 {copab 5173 ran crn 5659 ‘cfv 6566 (class class class)co 7451 ⟨“cs3 15035 Basecbs 17431 distcds 17481 TarskiGcstrkg 28946 Itvcitv 28952 LineGclng 28953 hlGchlg 29120 pInvGcmir 29181 hpGchpg 29292 cgrAccgra 29371

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-oadd 8518 df-er 8755 df-map 8887 df-pm 8888 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-dju 10019 df-card 10057 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-nn 12376 df-2 12445 df-3 12446 df-n0 12647 df-xnn0 12720 df-z 12734 df-uz 13006 df-fz 13680 df-fzo 13829 df-hash 14516 df-word 14700 df-concat 14757 df-s1 14784 df-s2 15041 df-s3 15042 df-trkgc 28967 df-trkgb 28968 df-trkgcb 28969 df-trkgld 28971 df-trkg 28972 df-cgrg 29031 df-leg 29103 df-hlg 29121 df-mir 29182 df-rag 29226 df-perpg 29228 df-hpg 29293 df-mid 29336 df-lmi 29337 df-cgra 29372

This theorem is used by: tgaaddcpbl2 29410

W3C validator