Metamath Proof Explorer

Theorem tgbtwnconnln2

Description: Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019)

Ref Expression
Hypotheses tgbtwnconn.p ⊢ P = Base G
tgbtwnconn.i ⊢ I = Itv ⁡ G
tgbtwnconn.g ⊢ φ → G ∈ 𝒢 Tarski
tgbtwnconn.a ⊢ φ → A ∈ P
tgbtwnconn.b ⊢ φ → B ∈ P
tgbtwnconn.c ⊢ φ → C ∈ P
tgbtwnconn.d ⊢ φ → D ∈ P
tgbtwnconnln1.l ⊢ L = Line 𝒢 ⁡ G
tgbtwnconnln1.1 ⊢ φ → A ≠ B
tgbtwnconnln1.2 ⊢ φ → B ∈ A I C
tgbtwnconnln1.3 ⊢ φ → B ∈ A I D
Assertion tgbtwnconnln2 ⊢ φ → B ∈ C L D ∨ C = D

Proof

Step Hyp Ref Expression
1 tgbtwnconn.p ⊢ P = Base G
2 tgbtwnconn.i ⊢ I = Itv ⁡ G
3 tgbtwnconn.g ⊢ φ → G ∈ 𝒢 Tarski
4 tgbtwnconn.a ⊢ φ → A ∈ P
5 tgbtwnconn.b ⊢ φ → B ∈ P
6 tgbtwnconn.c ⊢ φ → C ∈ P
7 tgbtwnconn.d ⊢ φ → D ∈ P
8 tgbtwnconnln1.l ⊢ L = Line 𝒢 ⁡ G
9 tgbtwnconnln1.1 ⊢ φ → A ≠ B
10 tgbtwnconnln1.2 ⊢ φ → B ∈ A I C
11 tgbtwnconnln1.3 ⊢ φ → B ∈ A I D
12 3 adantr ⊢ φ ∧ C ∈ B I D → G ∈ 𝒢 Tarski
13 6 adantr ⊢ φ ∧ C ∈ B I D → C ∈ P
14 7 adantr ⊢ φ ∧ C ∈ B I D → D ∈ P
15 5 adantr ⊢ φ ∧ C ∈ B I D → B ∈ P
16 simpr ⊢ φ ∧ C ∈ B I D → C ∈ B I D
17 1 8 2 12 13 14 15 16 btwncolg2 ⊢ φ ∧ C ∈ B I D → B ∈ C L D ∨ C = D
18 3 adantr ⊢ φ ∧ D ∈ B I C → G ∈ 𝒢 Tarski
19 6 adantr ⊢ φ ∧ D ∈ B I C → C ∈ P
20 7 adantr ⊢ φ ∧ D ∈ B I C → D ∈ P
21 5 adantr ⊢ φ ∧ D ∈ B I C → B ∈ P
22 eqid ⊢ dist ⁡ G = dist ⁡ G
23 simpr ⊢ φ ∧ D ∈ B I C → D ∈ B I C
24 1 22 2 18 21 20 19 23 tgbtwncom ⊢ φ ∧ D ∈ B I C → D ∈ C I B
25 1 8 2 18 19 20 21 24 btwncolg3 ⊢ φ ∧ D ∈ B I C → B ∈ C L D ∨ C = D
26 1 2 3 4 5 6 7 9 10 11 tgbtwnconn2 ⊢ φ → C ∈ B I D ∨ D ∈ B I C
27 17 25 26 mpjaodan ⊢ φ → B ∈ C L D ∨ C = D