Theorem mirhl2

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

	Ref	Expression
Hypotheses	mirval.p	|- P = ( Base ` G )
	mirval.d	|- .- = ( dist ` G )
	mirval.i	|- I = ( Itv ` G )
	mirval.l	|- L = ( LineG ` G )
	mirval.s	|- S = ( pInvG ` G )
	mirval.g	|- ( ph -> G e. TarskiG )
	mirhl.m	|- M = ( S ` A )
	mirhl.k	|- K = ( hlG ` G )
	mirhl.a	|- ( ph -> A e. P )
	mirhl.x	|- ( ph -> X e. P )
	mirhl.y	|- ( ph -> Y e. P )
	mirhl.z	|- ( ph -> Z e. P )
	mirhl2.1	|- ( ph -> X =/= A )
	mirhl2.2	|- ( ph -> Y =/= A )
	mirhl2.3	|- ( ph -> A e. ( X I ( M ` Y ) ) )
Assertion	mirhl2	|- ( ph -> X ( K ` A ) Y )

Proof

Step	Hyp	Ref	Expression
1		mirval.p	|- P = ( Base ` G )
2		mirval.d	|- .- = ( dist ` G )
3		mirval.i	|- I = ( Itv ` G )
4		mirval.l	|- L = ( LineG ` G )
5		mirval.s	|- S = ( pInvG ` G )
6		mirval.g	|- ( ph -> G e. TarskiG )
7		mirhl.m	|- M = ( S ` A )
8		mirhl.k	|- K = ( hlG ` G )
9		mirhl.a	|- ( ph -> A e. P )
10		mirhl.x	|- ( ph -> X e. P )
11		mirhl.y	|- ( ph -> Y e. P )
12		mirhl.z	|- ( ph -> Z e. P )
13		mirhl2.1	|- ( ph -> X =/= A )
14		mirhl2.2	|- ( ph -> Y =/= A )
15		mirhl2.3	|- ( ph -> A e. ( X I ( M ` Y ) ) )
16	1 2 3 4 5 6 9 7 11	mircl	|- ( ph -> ( M ` Y ) e. P )
17	1 2 3 4 5 6 9 7 11 14	mirne	|- ( ph -> ( M ` Y ) =/= A )
18	1 2 3 6 10 9 16 15	tgbtwncom	|- ( ph -> A e. ( ( M ` Y ) I X ) )
19	1 2 3 4 5 6 9 7 11	mirbtwn	|- ( ph -> A e. ( ( M ` Y ) I Y ) )
20	1 3 6 16 9 10 11 17 18 19	tgbtwnconn2	|- ( ph -> ( X e. ( A I Y ) \/ Y e. ( A I X ) ) )
21	1 3 8 10 11 9 6	ishlg	|- ( ph -> ( X ( K ` A ) Y <-> ( X =/= A /\ Y =/= A /\ ( X e. ( A I Y ) \/ Y e. ( A I X ) ) ) ) )
22	13 14 20 21	mpbir3and	|- ( ph -> X ( K ` A ) Y )