Theorem midbtwn

Description: Betweenness of midpoint. (Contributed by Thierry Arnoux, 7-Dec-2019)

	Ref	Expression
Hypotheses	ismid.p	|- P = ( Base ` G )
	ismid.d	|- .- = ( dist ` G )
	ismid.i	|- I = ( Itv ` G )
	ismid.g	|- ( ph -> G e. TarskiG )
	ismid.1	|- ( ph -> G TarskiGDim>= 2 )
	midcl.1	|- ( ph -> A e. P )
	midcl.2	|- ( ph -> B e. P )
Assertion	midbtwn	|- ( ph -> ( A ( midG ` G ) B ) e. ( A I B ) )

Proof

Step	Hyp	Ref	Expression
1		ismid.p	|- P = ( Base ` G )
2		ismid.d	|- .- = ( dist ` G )
3		ismid.i	|- I = ( Itv ` G )
4		ismid.g	|- ( ph -> G e. TarskiG )
5		ismid.1	|- ( ph -> G TarskiGDim>= 2 )
6		midcl.1	|- ( ph -> A e. P )
7		midcl.2	|- ( ph -> B e. P )
8	1 2 3 4 5 6 7	midcl	|- ( ph -> ( A ( midG ` G ) B ) e. P )
9		eqid	|- ( LineG ` G ) = ( LineG ` G )
10		eqid	|- ( pInvG ` G ) = ( pInvG ` G )
11		eqid	|- ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) = ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) )
12	1 2 3 9 10 4 8 11 6	mirbtwn	|- ( ph -> ( A ( midG ` G ) B ) e. ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) I A ) )
13		eqidd	|- ( ph -> ( A ( midG ` G ) B ) = ( A ( midG ` G ) B ) )
14	1 2 3 4 5 6 7 10 8	ismidb	|- ( ph -> ( B = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) <-> ( A ( midG ` G ) B ) = ( A ( midG ` G ) B ) ) )
15	13 14	mpbird	|- ( ph -> B = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) )
16	15	oveq1d	|- ( ph -> ( B I A ) = ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) I A ) )
17	12 16	eleqtrrd	|- ( ph -> ( A ( midG ` G ) B ) e. ( B I A ) )
18	1 2 3 4 7 8 6 17	tgbtwncom	|- ( ph -> ( A ( midG ` G ) B ) e. ( A I B ) )