Theorem midcl

Description: Closure of the midpoint. (Contributed by Thierry Arnoux, 1-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	midcl	|- ( ph -> ( A ( midG ` G ) B ) e. P )

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	midf	|- ( ph -> ( midG ` G ) : ( P X. P ) --> P )
9	8 6 7	fovrnd	|- ( ph -> ( A ( midG ` G ) B ) e. P )