midf

Description: Midpoint as a function. (Contributed by Thierry Arnoux, 1-Dec-2019)

	Ref	Expression
Hypotheses	ismid.p	$⊢ P = {Base}_{G}$
	ismid.d	$⊢ \underset{˙}{-} = dist (G)$
	ismid.i	$⊢ I = Itv (G)$
	ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
Assertion	midf	$⊢ φ \to {mid}_{𝒢} (G) : P \times P ⟶ P$

Proof

Step	Hyp	Ref	Expression
1		ismid.p	$⊢ P = {Base}_{G}$
2		ismid.d	$⊢ \underset{˙}{-} = dist (G)$
3		ismid.i	$⊢ I = Itv (G)$
4		ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
6		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
7	4	adantr	$⊢ (φ \land (a \in P \land b \in P)) \to G \in 𝒢_{Tarski}$
8		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
9		simprl	$⊢ (φ \land (a \in P \land b \in P)) \to a \in P$
10		simprr	$⊢ (φ \land (a \in P \land b \in P)) \to b \in P$
11	5	adantr	$⊢ (φ \land (a \in P \land b \in P)) \to G {Dim}_{𝒢} \geq 2$
12	1 2 3 6 7 8 9 10 11	mideu	$⊢ (φ \land (a \in P \land b \in P)) \to \exists! m \in P b = {pInv}_{𝒢} (G) (m) (a)$
13	12	ralrimivva	$⊢ φ \to \forall a \in P \forall b \in P \exists! m \in P b = {pInv}_{𝒢} (G) (m) (a)$
14		riotacl	$⊢ \exists! m \in P b = {pInv}_{𝒢} (G) (m) (a) \to (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a)) \in P$
15	14	2ralimi	$⊢ \forall a \in P \forall b \in P \exists! m \in P b = {pInv}_{𝒢} (G) (m) (a) \to \forall a \in P \forall b \in P (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a)) \in P$
16	13 15	syl	$⊢ φ \to \forall a \in P \forall b \in P (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a)) \in P$
17		eqid	$⊢ (a \in P, b \in P ⟼ (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a))) = (a \in P, b \in P ⟼ (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a)))$
18	17	fmpo	$⊢ \forall a \in P \forall b \in P (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a)) \in P \leftrightarrow (a \in P, b \in P ⟼ (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a))) : P \times P ⟶ P$
19	16 18	sylib	$⊢ φ \to (a \in P, b \in P ⟼ (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a))) : P \times P ⟶ P$
20		df-mid	$⊢ {mid}_{𝒢} = (g \in V ⟼ (a \in {Base}_{g}, b \in {Base}_{g} ⟼ (ι m \in {Base}_{g} \| b = {pInv}_{𝒢} (g) (m) (a))))$
21		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
22	21 1	eqtr4di	$⊢ g = G \to {Base}_{g} = P$
23		fveq2	$⊢ g = G \to {pInv}_{𝒢} (g) = {pInv}_{𝒢} (G)$
24	23	fveq1d	$⊢ g = G \to {pInv}_{𝒢} (g) (m) = {pInv}_{𝒢} (G) (m)$
25	24	fveq1d	$⊢ g = G \to {pInv}_{𝒢} (g) (m) (a) = {pInv}_{𝒢} (G) (m) (a)$
26	25	eqeq2d	$⊢ g = G \to (b = {pInv}_{𝒢} (g) (m) (a) \leftrightarrow b = {pInv}_{𝒢} (G) (m) (a))$
27	22 26	riotaeqbidv	$⊢ g = G \to (ι m \in {Base}_{g} \| b = {pInv}_{𝒢} (g) (m) (a)) = (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a))$
28	22 22 27	mpoeq123dv	$⊢ g = G \to (a \in {Base}_{g}, b \in {Base}_{g} ⟼ (ι m \in {Base}_{g} \| b = {pInv}_{𝒢} (g) (m) (a))) = (a \in P, b \in P ⟼ (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a)))$
29	4	elexd	$⊢ φ \to G \in V$
30	1	fvexi	$⊢ P \in V$
31	30 30	mpoex	$⊢ (a \in P, b \in P ⟼ (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a))) \in V$
32	31	a1i	$⊢ φ \to (a \in P, b \in P ⟼ (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a))) \in V$
33	20 28 29 32	fvmptd3	$⊢ φ \to {mid}_{𝒢} (G) = (a \in P, b \in P ⟼ (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a)))$
34	33	feq1d	$⊢ φ \to ({mid}_{𝒢} (G) : P \times P ⟶ P \leftrightarrow (a \in P, b \in P ⟼ (ι m \in P \| b = {pInv}_{𝒢} (G) (m) (a))) : P \times P ⟶ P)$
35	19 34	mpbird	$⊢ φ \to {mid}_{𝒢} (G) : P \times P ⟶ P$

Metamath Proof Explorer

Theorem midf

Proof