Theorem mirbtwni

Description: Point inversion preserves betweenness, first half of Theorem 7.15 of Schwabhauser p. 51. (Contributed by Thierry Arnoux, 9-Jun-2019)

	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 )
	mirval.a	|- ( ph -> A e. P )
	mirfv.m	|- M = ( S ` A )
	miriso.1	|- ( ph -> X e. P )
	miriso.2	|- ( ph -> Y e. P )
	mirbtwni.z	|- ( ph -> Z e. P )
	mirbtwni.b	|- ( ph -> Y e. ( X I Z ) )
Assertion	mirbtwni	|- ( ph -> ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) )

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		mirval.a	|- ( ph -> A e. P )
8		mirfv.m	|- M = ( S ` A )
9		miriso.1	|- ( ph -> X e. P )
10		miriso.2	|- ( ph -> Y e. P )
11		mirbtwni.z	|- ( ph -> Z e. P )
12		mirbtwni.b	|- ( ph -> Y e. ( X I Z ) )
13		eqid	|- ( cgrG ` G ) = ( cgrG ` G )
14	1 2 3 4 5 6 7 8	mirf	|- ( ph -> M : P --> P )
15	14 9	ffvelrnd	|- ( ph -> ( M ` X ) e. P )
16	14 10	ffvelrnd	|- ( ph -> ( M ` Y ) e. P )
17	14 11	ffvelrnd	|- ( ph -> ( M ` Z ) e. P )
18	1 2 3 4 5 6 7 8 9 10	miriso	|- ( ph -> ( ( M ` X ) .- ( M ` Y ) ) = ( X .- Y ) )
19	18	eqcomd	|- ( ph -> ( X .- Y ) = ( ( M ` X ) .- ( M ` Y ) ) )
20	1 2 3 4 5 6 7 8 10 11	miriso	|- ( ph -> ( ( M ` Y ) .- ( M ` Z ) ) = ( Y .- Z ) )
21	20	eqcomd	|- ( ph -> ( Y .- Z ) = ( ( M ` Y ) .- ( M ` Z ) ) )
22	1 2 3 4 5 6 7 8 11 9	miriso	|- ( ph -> ( ( M ` Z ) .- ( M ` X ) ) = ( Z .- X ) )
23	22	eqcomd	|- ( ph -> ( Z .- X ) = ( ( M ` Z ) .- ( M ` X ) ) )
24	1 2 13 6 9 10 11 15 16 17 19 21 23	trgcgr	|- ( ph -> <" X Y Z "> ( cgrG ` G ) <" ( M ` X ) ( M ` Y ) ( M ` Z ) "> )
25	1 2 3 13 6 9 10 11 15 16 17 24 12	tgbtwnxfr	|- ( ph -> ( M ` Y ) e. ( ( M ` X ) I ( M ` Z ) ) )