Theorem midcgr

Description: Congruence 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 )
	midcgr.1	|- ( ph -> ( A ( midG ` G ) B ) = C )
Assertion	midcgr	|- ( ph -> ( C .- A ) = ( C .- 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		midcgr.1	|- ( ph -> ( A ( midG ` G ) B ) = C )
9		eqid	|- ( pInvG ` G ) = ( pInvG ` G )
10	1 2 3 4 5 6 7	midcl	|- ( ph -> ( A ( midG ` G ) B ) e. P )
11	8 10	eqeltrrd	|- ( ph -> C e. P )
12	1 2 3 4 5 6 7 9 11	ismidb	|- ( ph -> ( B = ( ( ( pInvG ` G ) ` C ) ` A ) <-> ( A ( midG ` G ) B ) = C ) )
13	8 12	mpbird	|- ( ph -> B = ( ( ( pInvG ` G ) ` C ) ` A ) )
14	13	oveq2d	|- ( ph -> ( C .- B ) = ( C .- ( ( ( pInvG ` G ) ` C ) ` A ) ) )
15		eqid	|- ( LineG ` G ) = ( LineG ` G )
16		eqid	|- ( ( pInvG ` G ) ` C ) = ( ( pInvG ` G ) ` C )
17	1 2 3 15 9 4 11 16 6	mircgr	|- ( ph -> ( C .- ( ( ( pInvG ` G ) ` C ) ` A ) ) = ( C .- A ) )
18	14 17	eqtr2d	|- ( ph -> ( C .- A ) = ( C .- B ) )