tgbtwnconnln1

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

Step	Hyp	Ref	Expression
1		tgbtwnconn.p	$⊢ P = {Base}_{G}$
2		tgbtwnconn.i	$⊢ I = Itv (G)$
3		tgbtwnconn.g	$⊢ φ \to G \in 𝒢_{Tarski}$
4		tgbtwnconn.a	$⊢ φ \to A \in P$
5		tgbtwnconn.b	$⊢ φ \to B \in P$
6		tgbtwnconn.c	$⊢ φ \to C \in P$
7		tgbtwnconn.d	$⊢ φ \to D \in P$
8		tgbtwnconnln1.l	$⊢ L = {Line}_{𝒢} (G)$
9		tgbtwnconnln1.1	$⊢ φ \to A \neq B$
10		tgbtwnconnln1.2	$⊢ φ \to B \in (A I C)$
11		tgbtwnconnln1.3	$⊢ φ \to B \in (A I D)$
12	3	adantr	$⊢ (φ \land C \in (A I D)) \to G \in 𝒢_{Tarski}$
13	6	adantr	$⊢ (φ \land C \in (A I D)) \to C \in P$
14	7	adantr	$⊢ (φ \land C \in (A I D)) \to D \in P$
15	4	adantr	$⊢ (φ \land C \in (A I D)) \to A \in P$
16		simpr	$⊢ (φ \land C \in (A I D)) \to C \in (A I D)$
17	1 8 2 12 13 14 15 16	btwncolg2	$⊢ (φ \land C \in (A I D)) \to (A \in (C L D) \lor C = D)$
18	3	adantr	$⊢ (φ \land D \in (A I C)) \to G \in 𝒢_{Tarski}$
19	6	adantr	$⊢ (φ \land D \in (A I C)) \to C \in P$
20	7	adantr	$⊢ (φ \land D \in (A I C)) \to D \in P$
21	4	adantr	$⊢ (φ \land D \in (A I C)) \to A \in P$
22		eqid	$⊢ dist (G) = dist (G)$
23		simpr	$⊢ (φ \land D \in (A I C)) \to D \in (A I C)$
24	1 22 2 18 21 20 19 23	tgbtwncom	$⊢ (φ \land D \in (A I C)) \to D \in (C I A)$
25	1 8 2 18 19 20 21 24	btwncolg3	$⊢ (φ \land D \in (A I C)) \to (A \in (C L D) \lor C = D)$
26	1 2 3 4 5 6 7 9 10 11	tgbtwnconn1	$⊢ φ \to (C \in (A I D) \lor D \in (A I C))$
27	17 25 26	mpjaodan	$⊢ φ \to (A \in (C L D) \lor C = D)$

Metamath Proof Explorer