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 29345

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 2767	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → (cgrA‘𝐺) = ∼ )
4		tgaaddcpbl.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
5		tgaaddcpbl.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
6		eqid 2761	. . . . . . . 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 2761	. . . . . . . . 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 29073	. . . . . . . . 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 29094	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ (𝑌𝐿𝑆))
35		tgaaddcpbl.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))}
36	4, 5, 31, 7, 12, 32, 33	tgelrnln 29091	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌𝐿𝑆) ∈ ran 𝐿)
37		tgaaddcpbl.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋𝑂𝑍)
38	4, 24, 5, 35, 31, 36, 7, 10, 15, 37	oppne1 29210	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑆))
39		nelne2 3054	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑋 ∈ (𝑌𝐿𝑆)) → 𝑌 ≠ 𝑋)
40	34, 38, 39	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
41	40	necomd 3011	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
42	41	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑋 ≠ 𝑌)
43	4, 24, 5, 35, 31, 36, 7, 10, 15, 37	oppne2 29211	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑌𝐿𝑆))
44		nelne2 3054	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) → 𝑌 ≠ 𝑍)
45	34, 43, 44	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑍)
46	45	necomd 3011	. . . . . . . . . 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 29094	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ∈ (𝑉𝐿𝑇))
51		tgaaddcpbl.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈𝑄𝑊)
52		tgaaddcpbl.q	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑐𝐼𝑑))}
53		tgaaddcpbl.w	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
54	4, 24, 5, 52, 18, 53	islnopp 29208	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈𝑄𝑊 ↔ ((¬ 𝑈 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑊 ∈ (𝑉𝐿𝑇)) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑈𝐼𝑊))))
55	51, 54	mpbid 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((¬ 𝑈 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑊 ∈ (𝑉𝐿𝑇)) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑈𝐼𝑊)))
56	55	simplld 780	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑈 ∈ (𝑉𝐿𝑇))
57		nelne2 3054	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ (𝑉𝐿𝑇) ∧ ¬ 𝑈 ∈ (𝑉𝐿𝑇)) → 𝑉 ≠ 𝑈)
58	50, 56, 57	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ≠ 𝑈)
59	58	necomd 3011	. . . . . . . . . 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 2767	. . . . . . . . . . 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 28938	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑉 ≠ 𝑤)
65	64	necomd 3011	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑤 ≠ 𝑉)
66	4, 5, 24, 9, 11, 14, 17, 19, 22, 23, 25, 30, 42, 47, 60, 65	flatcgra 29325	. . . . . . . 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 2761	. . . . . . . . . . 11 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
71		eqid 2761	. . . . . . . . . . 11 ⊢ ((pInvG‘𝐺)‘𝑇) = ((pInvG‘𝐺)‘𝑇)
72	4, 24, 5, 31, 70, 7, 48, 71, 18	mircl 29126	. . . . . . . . . 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 29096	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → (𝑌𝐿𝑍) = (𝑍𝐿𝑌))
82	79, 81	eleqtrd 2863	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑆 ∈ (𝑍𝐿𝑌))
83	46	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑍 ≠ 𝑌)
84	4, 5, 31, 74, 75, 76, 77, 78, 82, 83	lnrot1 29084	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑌𝐿𝑍)) → 𝑍 ∈ (𝑌𝐿𝑆))
85	43, 84	mtand 828	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑆 ∈ (𝑌𝐿𝑍))
86	45	neneqd 2961	. . . . . . . . . . 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 29127	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘(((pInvG‘𝐺)‘𝑇)‘𝑈)) = 𝑈)
94	4, 5, 31, 7, 20, 48, 49	tgelrnln 29091	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉𝐿𝑇) ∈ ran 𝐿)
95	94	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (𝑉𝐿𝑇) ∈ ran 𝐿)
96	4, 5, 31, 7, 20, 48, 49	tglinerflx2 29095	. . . . . . . . . . . . . 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 29014	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (𝑇 ∈ ((((pInvG‘𝐺)‘𝑇)‘𝑈)𝐿𝑉) ∨ (((pInvG‘𝐺)‘𝑇)‘𝑈) = 𝑉))
102	4, 31, 5, 90, 98, 99, 91, 101	colrot1 29015	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → ((((pInvG‘𝐺)‘𝑇)‘𝑈) ∈ (𝑉𝐿𝑇) ∨ 𝑉 = 𝑇))
103	49	neneqd 2961	. . . . . . . . . . . . . . 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 29141	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑇 ∈ (𝑉𝐿(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∨ 𝑉 = (((pInvG‘𝐺)‘𝑇)‘𝑈))) → (((pInvG‘𝐺)‘𝑇)‘(((pInvG‘𝐺)‘𝑇)‘𝑈)) ∈ (𝑉𝐿𝑇))
107	93, 106	eqeltrrd 2862	. . . . . . . . . . 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 5118	. . . . . . . . . 10 ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑊”⟩)
113	112	ad7antr 751	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑊”⟩)
114		tgaaddcpbl.6	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)
115	110, 114	breqdi 5118	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑇”⟩)
116	4, 5, 7, 6, 10, 12, 32, 18, 20, 48, 115	cgracom 29322	. . . . . . . . . . . . 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 29332	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑤𝑉𝑇”⟩(cgrA‘𝐺)⟨“𝑍𝑌𝑆”⟩)
119	4, 5, 24, 9, 23, 22, 69, 17, 14, 68, 118	cgraswaplr 29326	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑇𝑉𝑤”⟩(cgrA‘𝐺)⟨“𝑆𝑌𝑍”⟩)
120	4, 5, 9, 6, 69, 22, 23, 68, 14, 17, 119	cgracom 29322	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑆𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑇𝑉𝑤”⟩)
121	4, 5, 31, 7, 20, 48, 49	tglinecom 29096	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉𝐿𝑇) = (𝑇𝐿𝑉))
122	121	fveq2d 6887	. . . . . . . . . . 11 ⊢ (𝜑 → ((hpG‘𝐺)‘(𝑉𝐿𝑇)) = ((hpG‘𝐺)‘(𝑇𝐿𝑉)))
123	18, 56	eldifd 3910	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ (𝑃 ∖ (𝑉𝐿𝑇)))
124	4, 5, 70, 71, 52, 7, 94, 96, 123, 31	oppmir 29225	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈𝑄(((pInvG‘𝐺)‘𝑇)‘𝑈))
125	4, 24, 5, 52, 31, 94, 7, 18, 72, 124	oppcom 29213	. . . . . . . . . . . 12 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈)
126	4, 24, 5, 52, 31, 94, 7, 18, 53, 51	oppcom 29213	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊𝑄𝑈)
127	4, 5, 31, 52, 7, 94, 53, 72, 18, 126	lnopp2hpgb 29234	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((pInvG‘𝐺)‘𝑇)‘𝑈)𝑄𝑈 ↔ 𝑊((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈)))
128	125, 127	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊((hpG‘𝐺)‘(𝑉𝐿𝑇))(((pInvG‘𝐺)‘𝑇)‘𝑈))
129	122, 128	breqdi 5118	. . . . . . . . . 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 2767	. . . . . . . . . . . . . . . . . . . . . . 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 28938	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑉 ≠ 𝑢)
146	145	necomd 3011	. . . . . . . . . . . . . . . . . . . . 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 29085	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑇 ∈ (𝑢𝐿𝑉))
150	59	ad5antr 747	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ≠ 𝑉)
151	4, 5, 31, 135, 140, 136, 147	tgelrnln 29091	. . . . . . . . . . . . . . . . . . . 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 29063	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑈((hlG‘𝐺)‘𝑉)𝑢)
155	4, 5, 6, 152, 26, 21, 8, 31, 154	hlln 29066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → 𝑈 ∈ (𝑢𝐿𝑉))
156	155	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑈 ∈ (𝑢𝐿𝑉))
157	4, 5, 31, 135, 140, 136, 147	tglinerflx2 29095	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ (𝑢𝐿𝑉))
158	4, 5, 31, 135, 138, 136, 150, 150, 151, 156, 157	tglinethru 29097	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → (𝑢𝐿𝑉) = (𝑈𝐿𝑉))
159	149, 158	eleqtrd 2863	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑢 ∈ (𝑉𝐿𝑇)) → 𝑇 ∈ (𝑈𝐿𝑉))
160	4, 5, 31, 135, 136, 137, 138, 139, 159, 150	lnrot1 29084	. . . . . . . . . . . . . . . . 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 2961	. . . . . . . . . . . . . . . 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 7433	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → (𝑢𝐼𝑤) = (𝑤𝐼𝑤))
174	171, 173	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑉 ∈ (𝑤𝐼𝑤))
175	4, 24, 5, 168, 169, 170, 174	axtgbtwnid 28921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑤 = 𝑉)
176	175	eqcomd 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑢 = 𝑤) → 𝑉 = 𝑤)
177	64, 176	mteqand 3047	. . . . . . . . . . . . . . . . . . 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 29091	. . . . . . . . . . . . . . . . 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 29094	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑢 ∈ (𝑢𝐿𝑤))
182	163	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → ¬ 𝑢 ∈ (𝑉𝐿𝑇))
183		nelne1 3053	. . . . . . . . . . . . . . . . . 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 29080	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ (𝑢𝐿𝑤))
188	134	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ (𝑉𝐿𝑇))
189	187, 188	elind 4146	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑉 ∈ ((𝑢𝐿𝑤) ∩ (𝑉𝐿𝑇)))
190	4, 5, 31, 165, 166, 167, 178	tglinerflx2 29095	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ (𝑢𝐿𝑤))
191		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ (𝑉𝐿𝑇))
192	190, 191	elind 4146	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) ∧ 𝑤 ∈ (𝑉𝐿𝑇)) → 𝑤 ∈ ((𝑢𝐿𝑤) ∩ (𝑉𝐿𝑇)))
193	4, 5, 31, 165, 179, 180, 184, 189, 192	tglineineq 29104	. . . . . . . . . . . . . . . 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 29209	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑢𝑄𝑤)
196	4, 24, 5, 52, 31, 133, 9, 6, 27, 19, 23, 195, 134, 28	opphl 29223	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑈𝑄𝑤)
197	4, 24, 5, 52, 31, 133, 9, 19, 23, 196	oppcom 29213	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑤𝑄𝑈)
198	4, 5, 31, 52, 9, 133, 23, 73, 19, 197	lnopp2hpgb 29234	. . . . . . . . . . 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 5118	. . . . . . . . 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 29335	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → 𝑊((hlG‘𝐺)‘𝑉)𝑤)
202	4, 5, 6, 9, 11, 14, 17, 19, 22, 23, 66, 67, 201	cgrahl2 29317	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) ∧ 𝑤 ∈ 𝑃) ∧ 𝑉 ∈ (𝑢𝐼𝑤)) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)) → ⟨“𝑋𝑌𝑍”⟩(cgrA‘𝐺)⟨“𝑈𝑉𝑊”⟩)
203	3, 202	breqdi 5118	. . . . . 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 28919	. . . . 5 ⊢ (((((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) ∧ 𝑢 ∈ 𝑃) ∧ 𝑢((hlG‘𝐺)‘𝑉)𝑈) ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)) → ∃𝑤 ∈ 𝑃 (𝑉 ∈ (𝑢𝐼𝑤) ∧ (𝑉(dist‘𝐺)𝑤) = (𝑌(dist‘𝐺)𝑍)))
206	204, 205	r19.29a 3171	. . . 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 29075	. . . 4 ⊢ (𝜑 → ∃𝑢 ∈ 𝑃 (𝑢((hlG‘𝐺)‘𝑉)𝑈 ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)))
209	208	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → ∃𝑢 ∈ 𝑃 (𝑢((hlG‘𝐺)‘𝑉)𝑈 ∧ (𝑉(dist‘𝐺)𝑢) = (𝑌(dist‘𝐺)𝑋)))
210	207, 209	r19.29a 3171	. 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 29344	. 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 2145 ≠ wne 2956 ∃wrex 3087 ∖ cdif 3896 class class class wbr 5103 {copab 5167 ran crn 5652 ‘cfv 6537 (class class class)co 7418 ⟨“cs3 14986 Basecbs 17380 distcds 17430 TarskiGcstrkg 28882 Itvcitv 28888 LineGclng 28889 hlGchlg 29056 pInvGcmir 29117 hpGchpg 29228 cgrAccgra 29307

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 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-oadd 8473 df-er 8710 df-map 8842 df-pm 8843 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-dju 9975 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-nn 12329 df-2 12398 df-3 12399 df-n0 12600 df-xnn0 12673 df-z 12687 df-uz 12959 df-fz 13633 df-fzo 13782 df-hash 14468 df-word 14652 df-concat 14709 df-s1 14736 df-s2 14992 df-s3 14993 df-trkgc 28903 df-trkgb 28904 df-trkgcb 28905 df-trkgld 28907 df-trkg 28908 df-cgrg 28967 df-leg 29039 df-hlg 29057 df-mir 29118 df-rag 29162 df-perpg 29164 df-hpg 29229 df-mid 29272 df-lmi 29273 df-cgra 29308

This theorem is used by: tgaaddcpbl2 29346

W3C validator