Theorem btwnhl

Description: Swap betweenness for a half-line. (Contributed by Thierry Arnoux, 2-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	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	btwnhl.1	⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐷 ) 𝐵 )
	btwnhl.3	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) )
Assertion	btwnhl	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) )

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		btwnhl.1	⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐷 ) 𝐵 )
10		btwnhl.3	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) )
11		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
12	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐶 ∈ 𝑃 )
14	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐷 ∈ 𝑃 )
15	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
16	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
17	1 2 3 4 5 8 7	ishlg	⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐷 ) 𝐵 ↔ ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ) ) )
18	9 17	mpbid	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ) )
19	18	simp1d	⊢ ( 𝜑 → 𝐴 ≠ 𝐷 )
20	19	necomd	⊢ ( 𝜑 → 𝐷 ≠ 𝐴 )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐷 ≠ 𝐴 )
22	10	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) )
23	1 11 2 12 16 14 13 22	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐷 ∈ ( 𝐶 𝐼 𝐴 ) )
24		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) )
25	1 11 2 12 13 14 16 15 21 23 24	tgbtwnouttr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐷 ∈ ( 𝐶 𝐼 𝐵 ) )
26	1 11 2 12 13 14 15 25	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) )
27	7	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) → 𝐺 ∈ TarskiG )
28	4	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) → 𝐴 ∈ 𝑃 )
29	5	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) → 𝐵 ∈ 𝑃 )
30	8	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) → 𝐷 ∈ 𝑃 )
31	6	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) → 𝐶 ∈ 𝑃 )
32		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) → 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) )
33	1 11 2 27 30 29 28 32	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
34	10	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) → 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) )
35	1 11 2 27 28 29 30 31 33 34	tgbtwnexch3	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) → 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) )
36	18	simp3d	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) )
37	26 35 36	mpjaodan	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) )