Theorem midcom

Description: Commutativity rule for the midpoint. (Contributed by Thierry Arnoux, 2-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	midcom	|- ( ph -> ( A ( midG ` G ) B ) = ( B ( midG ` G ) A ) )

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		eqid	|- ( LineG ` G ) = ( LineG ` G )
9		eqid	|- ( pInvG ` G ) = ( pInvG ` G )
10	1 2 3 4 5 7 6	midcl	|- ( ph -> ( B ( midG ` G ) A ) e. P )
11		eqid	|- ( ( pInvG ` G ) ` ( B ( midG ` G ) A ) ) = ( ( pInvG ` G ) ` ( B ( midG ` G ) A ) )
12		eqidd	|- ( ph -> ( B ( midG ` G ) A ) = ( B ( midG ` G ) A ) )
13	1 2 3 4 5 7 6 12	midcgr	|- ( ph -> ( ( B ( midG ` G ) A ) .- B ) = ( ( B ( midG ` G ) A ) .- A ) )
14	1 2 3 4 5 7 6	midbtwn	|- ( ph -> ( B ( midG ` G ) A ) e. ( B I A ) )
15	1 2 3 8 9 4 10 11 6 7 13 14	ismir	|- ( ph -> B = ( ( ( pInvG ` G ) ` ( B ( midG ` G ) A ) ) ` A ) )
16	1 2 3 4 5 6 7 9 10	ismidb	|- ( ph -> ( B = ( ( ( pInvG ` G ) ` ( B ( midG ` G ) A ) ) ` A ) <-> ( A ( midG ` G ) B ) = ( B ( midG ` G ) A ) ) )
17	15 16	mpbid	|- ( ph -> ( A ( midG ` G ) B ) = ( B ( midG ` G ) A ) )