tgbtwnconn1 - Metamath Proof Explorer

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

Theorem tgbtwnconn1 28295

Description: Connectivity law for betweenness. Theorem 5.1 of [Schwabhauser] p. 39-41. In earlier presentations of Tarski's axioms, this theorem appeared as an additional axiom. It was derived from the other axioms by Gupta, 1965. (Contributed by Thierry Arnoux, 30-Apr-2019.)

**Hypotheses**
Ref	Expression
tgbtwnconn1.p	⊢ 𝑃 = (Base‘𝐺)
tgbtwnconn1.i	⊢ 𝐼 = (Itv‘𝐺)
tgbtwnconn1.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tgbtwnconn1.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
tgbtwnconn1.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
tgbtwnconn1.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
tgbtwnconn1.d	⊢ (𝜑 → 𝐷 ∈ 𝑃)
tgbtwnconn1.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)
tgbtwnconn1.2	⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
tgbtwnconn1.3	⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))

**Assertion**
Ref	Expression
tgbtwnconn1	⊢ (𝜑 → (𝐶 ∈ (𝐴𝐼𝐷) ∨ 𝐷 ∈ (𝐴𝐼𝐶)))

Proof of Theorem tgbtwnconn1 Dummy variables 𝑒 𝑓 ℎ 𝑗 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpllr 773	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶)))
2	1	simpld 494	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → 𝐷 ∈ (𝐴𝐼𝑒))
3	2	adantr 480	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 = 𝑒) → 𝐷 ∈ (𝐴𝐼𝑒))
4		simpr 484	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 = 𝑒) → 𝐶 = 𝑒)
5	4	oveq2d 7417	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 = 𝑒) → (𝐴𝐼𝐶) = (𝐴𝐼𝑒))
6	3, 5	eleqtrrd 2828	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 = 𝑒) → 𝐷 ∈ (𝐴𝐼𝐶))
7	6	olcd 871	. . . 4 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 = 𝑒) → (𝐶 ∈ (𝐴𝐼𝐷) ∨ 𝐷 ∈ (𝐴𝐼𝐶)))
8		simprl 768	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → 𝐶 ∈ (𝐴𝐼𝑓))
9	8	adantr 480	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐷 = 𝑓) → 𝐶 ∈ (𝐴𝐼𝑓))
10		simpr 484	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐷 = 𝑓) → 𝐷 = 𝑓)
11	10	oveq2d 7417	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐷 = 𝑓) → (𝐴𝐼𝐷) = (𝐴𝐼𝑓))
12	9, 11	eleqtrrd 2828	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐷 = 𝑓) → 𝐶 ∈ (𝐴𝐼𝐷))
13	12	orcd 870	. . . 4 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐷 = 𝑓) → (𝐶 ∈ (𝐴𝐼𝐷) ∨ 𝐷 ∈ (𝐴𝐼𝐶)))
14		df-ne 2933	. . . . . 6 ⊢ (𝐶 ≠ 𝑒 ↔ ¬ 𝐶 = 𝑒)
15		tgbtwnconn1.p	. . . . . . . . . . 11 ⊢ 𝑃 = (Base‘𝐺)
16		tgbtwnconn1.i	. . . . . . . . . . 11 ⊢ 𝐼 = (Itv‘𝐺)
17		tgbtwnconn1.g	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
18	17	ad4antr 729	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → 𝐺 ∈ TarskiG)
19	18	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐺 ∈ TarskiG)
20		tgbtwnconn1.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
21	20	ad4antr 729	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → 𝐴 ∈ 𝑃)
22	21	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐴 ∈ 𝑃)
23		tgbtwnconn1.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
24	23	ad4antr 729	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → 𝐵 ∈ 𝑃)
25	24	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐵 ∈ 𝑃)
26		tgbtwnconn1.c	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
27	26	ad4antr 729	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → 𝐶 ∈ 𝑃)
28	27	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐶 ∈ 𝑃)
29		tgbtwnconn1.d	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
30	29	ad4antr 729	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → 𝐷 ∈ 𝑃)
31	30	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐷 ∈ 𝑃)
32		simp-11l 794	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝜑)
33		tgbtwnconn1.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
34	32, 33	syl 17	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐴 ≠ 𝐵)
35		tgbtwnconn1.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶))
36	32, 35	syl 17	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐵 ∈ (𝐴𝐼𝐶))
37		tgbtwnconn1.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷))
38	32, 37	syl 17	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐵 ∈ (𝐴𝐼𝐷))
39		eqid 2724	. . . . . . . . . . 11 ⊢ (dist‘𝐺) = (dist‘𝐺)
40		simp-4r 781	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → 𝑒 ∈ 𝑃)
41	40	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝑒 ∈ 𝑃)
42		simplr 766	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → 𝑓 ∈ 𝑃)
43	42	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝑓 ∈ 𝑃)
44		simp-6r 785	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → ℎ ∈ 𝑃)
45		simp-4r 781	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝑗 ∈ 𝑃)
46	2	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐷 ∈ (𝐴𝐼𝑒))
47	8	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐶 ∈ (𝐴𝐼𝑓))
48		simp-5r 783	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶)))
49	48	simpld 494	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝑒 ∈ (𝐴𝐼ℎ))
50		simpllr 773	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷)))
51	50	simpld 494	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝑓 ∈ (𝐴𝐼𝑗))
52	1	simprd 495	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))
53	52	ad7antr 735	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))
54	15, 39, 16, 19, 31, 41, 31, 28, 53	tgcgrcomlr 28200	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → (𝑒(dist‘𝐺)𝐷) = (𝐶(dist‘𝐺)𝐷))
55		simprr 770	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))
56	55	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))
57	48	simprd 495	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))
58	50	simprd 495	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))
59		simplr 766	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝑥 ∈ 𝑃)
60		simprl 768	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝑥 ∈ (𝐶𝐼𝑒))
61		simprr 770	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝑥 ∈ (𝐷𝐼𝑓))
62		simp-7r 787	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐶 ≠ 𝑒)
63	15, 16, 19, 22, 25, 28, 31, 34, 36, 38, 39, 41, 43, 44, 45, 46, 47, 49, 51, 54, 56, 57, 58, 59, 60, 61, 62	tgbtwnconn1lem3 28294	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓))) → 𝐷 = 𝑓)
64	15, 39, 16, 18, 21, 27, 42, 8	tgbtwncom 28208	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → 𝐶 ∈ (𝑓𝐼𝐴))
65	15, 39, 16, 18, 21, 30, 40, 2	tgbtwncom 28208	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → 𝐷 ∈ (𝑒𝐼𝐴))
66	15, 39, 16, 18, 42, 40, 21, 27, 30, 64, 65	axtgpasch 28187	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓)))
67	66	ad5antr 731	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐶𝐼𝑒) ∧ 𝑥 ∈ (𝐷𝐼𝑓)))
68	63, 67	r19.29a 3154	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) ∧ 𝑗 ∈ 𝑃) ∧ (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷))) → 𝐷 = 𝑓)
69	15, 39, 16, 18, 21, 42, 24, 30	axtgsegcon 28184	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → ∃𝑗 ∈ 𝑃 (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷)))
70	69	ad3antrrr 727	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) → ∃𝑗 ∈ 𝑃 (𝑓 ∈ (𝐴𝐼𝑗) ∧ (𝑓(dist‘𝐺)𝑗) = (𝐵(dist‘𝐺)𝐷)))
71	68, 70	r19.29a 3154	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) ∧ ℎ ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶))) → 𝐷 = 𝑓)
72	15, 39, 16, 18, 21, 40, 24, 27	axtgsegcon 28184	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → ∃ℎ ∈ 𝑃 (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶)))
73	72	adantr 480	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) → ∃ℎ ∈ 𝑃 (𝑒 ∈ (𝐴𝐼ℎ) ∧ (𝑒(dist‘𝐺)ℎ) = (𝐵(dist‘𝐺)𝐶)))
74	71, 73	r19.29a 3154	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) ∧ 𝐶 ≠ 𝑒) → 𝐷 = 𝑓)
75	74	ex 412	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → (𝐶 ≠ 𝑒 → 𝐷 = 𝑓))
76	14, 75	biimtrrid 242	. . . . 5 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → (¬ 𝐶 = 𝑒 → 𝐷 = 𝑓))
77	76	orrd 860	. . . 4 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → (𝐶 = 𝑒 ∨ 𝐷 = 𝑓))
78	7, 13, 77	mpjaodan 955	. . 3 ⊢ (((((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) ∧ 𝑓 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷))) → (𝐶 ∈ (𝐴𝐼𝐷) ∨ 𝐷 ∈ (𝐴𝐼𝐶)))
79	15, 39, 16, 17, 20, 26, 26, 29	axtgsegcon 28184	. . . 4 ⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷)))
80	79	ad2antrr 723	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) → ∃𝑓 ∈ 𝑃 (𝐶 ∈ (𝐴𝐼𝑓) ∧ (𝐶(dist‘𝐺)𝑓) = (𝐶(dist‘𝐺)𝐷)))
81	78, 80	r19.29a 3154	. 2 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝑃) ∧ (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶))) → (𝐶 ∈ (𝐴𝐼𝐷) ∨ 𝐷 ∈ (𝐴𝐼𝐶)))
82	15, 39, 16, 17, 20, 29, 29, 26	axtgsegcon 28184	. 2 ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝐷 ∈ (𝐴𝐼𝑒) ∧ (𝐷(dist‘𝐺)𝑒) = (𝐷(dist‘𝐺)𝐶)))
83	81, 82	r19.29a 3154	1 ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐼𝐷) ∨ 𝐷 ∈ (𝐴𝐼𝐶)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 844 = wceq 1533 ∈ wcel 2098 ≠ wne 2932 ∃wrex 3062 ‘cfv 6533 (class class class)co 7401 Basecbs 17143 distcds 17205 TarskiGcstrkg 28147 Itvcitv 28153

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-tp 4625 df-op 4627 df-uni 4900 df-int 4941 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7357 df-ov 7404 df-oprab 7405 df-mpo 7406 df-om 7849 df-1st 7968 df-2nd 7969 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-1o 8461 df-oadd 8465 df-er 8699 df-pm 8819 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-dju 9892 df-card 9930 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-nn 12210 df-2 12272 df-3 12273 df-n0 12470 df-xnn0 12542 df-z 12556 df-uz 12820 df-fz 13482 df-fzo 13625 df-hash 14288 df-word 14462 df-concat 14518 df-s1 14543 df-s2 14796 df-s3 14797 df-trkgc 28168 df-trkgb 28169 df-trkgcb 28170 df-trkg 28173 df-cgrg 28231

This theorem is referenced by: tgbtwnconn2 28296 tgbtwnconnln1 28300 hltr 28330 hlbtwn 28331

W3C validator