Theorem btwnhl2

Description: Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020)

	Ref	Expression
Hypotheses	ishlg.p	$$⊢P={\mathrm{Base}}_G$$
	ishlg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	ishlg.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	ishlg.a	$$⊢\phi \to A\in P$$
	ishlg.b	$$⊢\phi \to B\in P$$
	ishlg.c	$$⊢\phi \to C\in P$$
	hlln.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	hltr.d	$$⊢\phi \to D\in P$$
	btwnhl1.1	$$⊢\phi \to C\in \left(AIB\right)$$
	btwnhl1.2	$$⊢\phi \to A\ne B$$
	btwnhl2.3	$$⊢\phi \to C\ne B$$
Assertion	btwnhl2	$$⊢\phi \to CK\left(B\right)A$$

Proof

Step	Hyp	Ref	Expression
1		ishlg.p	$$⊢P={\mathrm{Base}}_G$$
2		ishlg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		ishlg.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
4		ishlg.a	$$⊢\phi \to A\in P$$
5		ishlg.b	$$⊢\phi \to B\in P$$
6		ishlg.c	$$⊢\phi \to C\in P$$
7		hlln.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
8		hltr.d	$$⊢\phi \to D\in P$$
9		btwnhl1.1	$$⊢\phi \to C\in \left(AIB\right)$$
10		btwnhl1.2	$$⊢\phi \to A\ne B$$
11		btwnhl2.3	$$⊢\phi \to C\ne B$$
12		eqid	$$⊢\mathrm{dist}\left(G\right)=\mathrm{dist}\left(G\right)$$
13	1 12 2 7 4 6 5 9	tgbtwncom	$$⊢\phi \to C\in \left(BIA\right)$$
14	13	orcd	$$⊢\phi \to \left(C\in \left(BIA\right)\vee A\in \left(BIC\right)\right)$$
15	1 2 3 6 4 5 7	ishlg	$$⊢\phi \to \left(CK\left(B\right)A\leftrightarrow \left(C\ne B\wedge A\ne B\wedge \left(C\in \left(BIA\right)\vee A\in \left(BIC\right)\right)\right)\right)$$
16	11 10 14 15	mpbir3and	$$⊢\phi \to CK\left(B\right)A$$