Theorem midid

Description: Midpoint of a null segment. (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	midid	|- ( ph -> ( A ( midG ` G ) A ) = 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	1 2 3 4 5 6 6	midcl	|- ( ph -> ( A ( midG ` G ) A ) e. P )
9	1 2 3 4 5 6 6	midbtwn	|- ( ph -> ( A ( midG ` G ) A ) e. ( A I A ) )
10	1 2 3 4 6 8 9	axtgbtwnid	|- ( ph -> A = ( A ( midG ` G ) A ) )
11	10	eqcomd	|- ( ph -> ( A ( midG ` G ) A ) = A )