ismidb

Description: Property of the midpoint. (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$
	midcl.1	$⊢ φ \to A \in P$
	midcl.2	$⊢ φ \to B \in P$
	ismidb.s	$⊢ S = {pInv}_{𝒢} (G)$
	ismidb.m	$⊢ φ \to M \in P$
Assertion	ismidb	$⊢ φ \to (B = S (M) (A) \leftrightarrow A {mid}_{𝒢} (G) B = M)$

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		midcl.1	$⊢ φ \to A \in P$
7		midcl.2	$⊢ φ \to B \in P$
8		ismidb.s	$⊢ S = {pInv}_{𝒢} (G)$
9		ismidb.m	$⊢ φ \to M \in P$
10		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
11	1 2 3 10 4 8 6 7 5	mideu	$⊢ φ \to \exists! m \in P B = S (m) (A)$
12		fveq2	$⊢ m = M \to S (m) = S (M)$
13	12	fveq1d	$⊢ m = M \to S (m) (A) = S (M) (A)$
14	13	eqeq2d	$⊢ m = M \to (B = S (m) (A) \leftrightarrow B = S (M) (A))$
15	14	riota2	$⊢ (M \in P \land \exists! m \in P B = S (m) (A)) \to (B = S (M) (A) \leftrightarrow (ι m \in P \| B = S (m) (A)) = M)$
16	9 11 15	syl2anc	$⊢ φ \to (B = S (M) (A) \leftrightarrow (ι m \in P \| B = S (m) (A)) = M)$
17		df-mid	$⊢ {mid}_{𝒢} = (g \in V ⟼ (a \in {Base}_{g}, b \in {Base}_{g} ⟼ (ι m \in {Base}_{g} \| b = {pInv}_{𝒢} (g) (m) (a))))$
18		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
19	18 1	eqtr4di	$⊢ g = G \to {Base}_{g} = P$
20		fveq2	$⊢ g = G \to {pInv}_{𝒢} (g) = {pInv}_{𝒢} (G)$
21	20 8	eqtr4di	$⊢ g = G \to {pInv}_{𝒢} (g) = S$
22	21	fveq1d	$⊢ g = G \to {pInv}_{𝒢} (g) (m) = S (m)$
23	22	fveq1d	$⊢ g = G \to {pInv}_{𝒢} (g) (m) (a) = S (m) (a)$
24	23	eqeq2d	$⊢ g = G \to (b = {pInv}_{𝒢} (g) (m) (a) \leftrightarrow b = S (m) (a))$
25	19 24	riotaeqbidv	$⊢ g = G \to (ι m \in {Base}_{g} \| b = {pInv}_{𝒢} (g) (m) (a)) = (ι m \in P \| b = S (m) (a))$
26	19 19 25	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 = S (m) (a)))$
27	4	elexd	$⊢ φ \to G \in V$
28	1	fvexi	$⊢ P \in V$
29	28 28	mpoex	$⊢ (a \in P, b \in P ⟼ (ι m \in P \| b = S (m) (a))) \in V$
30	29	a1i	$⊢ φ \to (a \in P, b \in P ⟼ (ι m \in P \| b = S (m) (a))) \in V$
31	17 26 27 30	fvmptd3	$⊢ φ \to {mid}_{𝒢} (G) = (a \in P, b \in P ⟼ (ι m \in P \| b = S (m) (a)))$
32		simprr	$⊢ (φ \land (a = A \land b = B)) \to b = B$
33		simprl	$⊢ (φ \land (a = A \land b = B)) \to a = A$
34	33	fveq2d	$⊢ (φ \land (a = A \land b = B)) \to S (m) (a) = S (m) (A)$
35	32 34	eqeq12d	$⊢ (φ \land (a = A \land b = B)) \to (b = S (m) (a) \leftrightarrow B = S (m) (A))$
36	35	riotabidv	$⊢ (φ \land (a = A \land b = B)) \to (ι m \in P \| b = S (m) (a)) = (ι m \in P \| B = S (m) (A))$
37		riotacl	$⊢ \exists! m \in P B = S (m) (A) \to (ι m \in P \| B = S (m) (A)) \in P$
38	11 37	syl	$⊢ φ \to (ι m \in P \| B = S (m) (A)) \in P$
39	31 36 6 7 38	ovmpod	$⊢ φ \to A {mid}_{𝒢} (G) B = (ι m \in P \| B = S (m) (A))$
40	39	eqeq1d	$⊢ φ \to (A {mid}_{𝒢} (G) B = M \leftrightarrow (ι m \in P \| B = S (m) (A)) = M)$
41	16 40	bitr4d	$⊢ φ \to (B = S (M) (A) \leftrightarrow A {mid}_{𝒢} (G) B = M)$

Metamath Proof Explorer

Theorem ismidb

Proof