Theorem btwnhl2

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

	Ref	Expression
Hypotheses	ishlg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	ishlg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	ishlg.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	ishlg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	ishlg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	ishlg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	hlln.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	hltr.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	btwnhl1.1	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
	btwnhl1.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	btwnhl2.3	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
Assertion	btwnhl2	⊢ ( 𝜑 → 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ishlg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		ishlg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		ishlg.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
4		ishlg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5		ishlg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6		ishlg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7		hlln.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		hltr.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		btwnhl1.1	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
10		btwnhl1.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
11		btwnhl2.3	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
12		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
13	1 12 2 7 4 6 5 9	tgbtwncom	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) )
14	13	orcd	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) )
15	1 2 3 6 4 5 7	ishlg	⊢ ( 𝜑 → ( 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐴 ↔ ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) ) )
16	11 10 14 15	mpbir3and	⊢ ( 𝜑 → 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐴 )