Theorem btwnhl1

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	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	btwnhl1.3	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
Assertion	btwnhl1	⊢ ( 𝜑 → 𝐶 ( 𝐾 ‘ 𝐴 ) 𝐵 )

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		btwnhl1.3	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
12	10	necomd	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
13	9	orcd	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )
14	1 2 3 6 5 4 7	ishlg	⊢ ( 𝜑 → ( 𝐶 ( 𝐾 ‘ 𝐴 ) 𝐵 ↔ ( 𝐶 ≠ 𝐴 ∧ 𝐵 ≠ 𝐴 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ) ) )
15	11 12 13 14	mpbir3and	⊢ ( 𝜑 → 𝐶 ( 𝐾 ‘ 𝐴 ) 𝐵 )