Theorem mirhl2

Description: Deduce half-line relation from mirror point. (Contributed by Thierry Arnoux, 8-Aug-2020)

	Ref	Expression
Hypotheses	mirval.p	$$⊢P={\mathrm{Base}}_G$$
	mirval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	mirval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	mirval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	mirval.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
	mirval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	mirhl.m	$$⊢M=S\left(A\right)$$
	mirhl.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	mirhl.a	$$⊢\phi \to A\in P$$
	mirhl.x	$$⊢\phi \to X\in P$$
	mirhl.y	$$⊢\phi \to Y\in P$$
	mirhl.z	$$⊢\phi \to Z\in P$$
	mirhl2.1	$$⊢\phi \to X\ne A$$
	mirhl2.2	$$⊢\phi \to Y\ne A$$
	mirhl2.3	$$⊢\phi \to A\in \left(XIM\left(Y\right)\right)$$
Assertion	mirhl2	$$⊢\phi \to XK\left(A\right)Y$$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$$⊢P={\mathrm{Base}}_G$$
2		mirval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		mirval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		mirval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		mirval.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
6		mirval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
7		mirhl.m	$$⊢M=S\left(A\right)$$
8		mirhl.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
9		mirhl.a	$$⊢\phi \to A\in P$$
10		mirhl.x	$$⊢\phi \to X\in P$$
11		mirhl.y	$$⊢\phi \to Y\in P$$
12		mirhl.z	$$⊢\phi \to Z\in P$$
13		mirhl2.1	$$⊢\phi \to X\ne A$$
14		mirhl2.2	$$⊢\phi \to Y\ne A$$
15		mirhl2.3	$$⊢\phi \to A\in \left(XIM\left(Y\right)\right)$$
16	1 2 3 4 5 6 9 7 11	mircl	$$⊢\phi \to M\left(Y\right)\in P$$
17	1 2 3 4 5 6 9 7 11 14	mirne	$$⊢\phi \to M\left(Y\right)\ne A$$
18	1 2 3 6 10 9 16 15	tgbtwncom	$$⊢\phi \to A\in \left(M\left(Y\right)IX\right)$$
19	1 2 3 4 5 6 9 7 11	mirbtwn	$$⊢\phi \to A\in \left(M\left(Y\right)IY\right)$$
20	1 3 6 16 9 10 11 17 18 19	tgbtwnconn2	$$⊢\phi \to \left(X\in \left(AIY\right)\vee Y\in \left(AIX\right)\right)$$
21	1 3 8 10 11 9 6	ishlg	$$⊢\phi \to \left(XK\left(A\right)Y\leftrightarrow \left(X\ne A\wedge Y\ne A\wedge \left(X\in \left(AIY\right)\vee Y\in \left(AIX\right)\right)\right)\right)$$
22	13 14 20 21	mpbir3and	$$⊢\phi \to XK\left(A\right)Y$$