Metamath Proof Explorer

Theorem tgbtwnconnln3

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
tgbtwnconn3.1 ⊢ φ → B ∈ A I D
tgbtwnconn3.2 ⊢ φ → C ∈ A I D
tgbtwnconnln3.l ⊢ L = Line 𝒢 ⁡ G
Assertion tgbtwnconnln3 ⊢ φ → B ∈ A L C ∨ A = C

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 tgbtwnconn3.1 ⊢ φ → B ∈ A I D
9 tgbtwnconn3.2 ⊢ φ → C ∈ A I D
10 tgbtwnconnln3.l ⊢ L = Line 𝒢 ⁡ G
11 3 adantr ⊢ φ ∧ B ∈ A I C → G ∈ 𝒢 Tarski
12 4 adantr ⊢ φ ∧ B ∈ A I C → A ∈ P
13 6 adantr ⊢ φ ∧ B ∈ A I C → C ∈ P
14 5 adantr ⊢ φ ∧ B ∈ A I C → B ∈ P
15 simpr ⊢ φ ∧ B ∈ A I C → B ∈ A I C
16 1 10 2 11 12 13 14 15 btwncolg1 ⊢ φ ∧ B ∈ A I C → B ∈ A L C ∨ A = C
17 3 adantr ⊢ φ ∧ C ∈ A I B → G ∈ 𝒢 Tarski
18 4 adantr ⊢ φ ∧ C ∈ A I B → A ∈ P
19 6 adantr ⊢ φ ∧ C ∈ A I B → C ∈ P
20 5 adantr ⊢ φ ∧ C ∈ A I B → B ∈ P
21 simpr ⊢ φ ∧ C ∈ A I B → C ∈ A I B
22 1 10 2 17 18 19 20 21 btwncolg3 ⊢ φ ∧ C ∈ A I B → B ∈ A L C ∨ A = C
23 1 2 3 4 5 6 7 8 9 tgbtwnconn3 ⊢ φ → B ∈ A I C ∨ C ∈ A I B
24 16 22 23 mpjaodan ⊢ φ → B ∈ A L C ∨ A = C