Theorem hlid

Description: The half-line relation is reflexive. Theorem 6.5 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 21-Feb-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}}$$
	hlid.1	$$⊢\phi \to A\ne C$$
Assertion	hlid	$$⊢\phi \to AK\left(C\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		hlid.1	$$⊢\phi \to A\ne C$$
9		eqid	$$⊢\mathrm{dist}\left(G\right)=\mathrm{dist}\left(G\right)$$
10	1 9 2 7 6 4	tgbtwntriv2	$$⊢\phi \to A\in \left(CIA\right)$$
11	10	olcd	$$⊢\phi \to \left(A\in \left(CIA\right)\vee A\in \left(CIA\right)\right)$$
12	1 2 3 4 4 6 7	ishlg	$$⊢\phi \to \left(AK\left(C\right)A\leftrightarrow \left(A\ne C\wedge A\ne C\wedge \left(A\in \left(CIA\right)\vee A\in \left(CIA\right)\right)\right)\right)$$
13	8 8 11 12	mpbir3and	$$⊢\phi \to AK\left(C\right)A$$