Metamath Proof Explorer


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 ) )