mideu

Description: Existence and uniqueness of the midpoint, Theorem 8.22 of Schwabhauser p. 64. (Contributed by Thierry Arnoux, 25-Nov-2019)

	Ref	Expression
Hypotheses	colperpex.p	$⊢ P = {Base}_{G}$
	colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
	colperpex.i	$⊢ I = Itv (G)$
	colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
	colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mideu.s	$⊢ S = {pInv}_{𝒢} (G)$
	mideu.1	$⊢ φ \to A \in P$
	mideu.2	$⊢ φ \to B \in P$
	mideu.3	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
Assertion	mideu	$⊢ φ \to \exists! x \in P B = S (x) (A)$

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	$⊢ P = {Base}_{G}$
2		colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
3		colperpex.i	$⊢ I = Itv (G)$
4		colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
5		colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		mideu.s	$⊢ S = {pInv}_{𝒢} (G)$
7		mideu.1	$⊢ φ \to A \in P$
8		mideu.2	$⊢ φ \to B \in P$
9		mideu.3	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
10	1 2 3 4 5 6 7 8 9	midex	$⊢ φ \to \exists x \in P B = S (x) (A)$
11	5	ad2antrr	$⊢ ((φ \land (x \in P \land y \in P)) \land (B = S (x) (A) \land B = S (y) (A))) \to G \in 𝒢_{Tarski}$
12		simplrl	$⊢ ((φ \land (x \in P \land y \in P)) \land (B = S (x) (A) \land B = S (y) (A))) \to x \in P$
13		simplrr	$⊢ ((φ \land (x \in P \land y \in P)) \land (B = S (x) (A) \land B = S (y) (A))) \to y \in P$
14	7	ad2antrr	$⊢ ((φ \land (x \in P \land y \in P)) \land (B = S (x) (A) \land B = S (y) (A))) \to A \in P$
15	8	ad2antrr	$⊢ ((φ \land (x \in P \land y \in P)) \land (B = S (x) (A) \land B = S (y) (A))) \to B \in P$
16		simprl	$⊢ ((φ \land (x \in P \land y \in P)) \land (B = S (x) (A) \land B = S (y) (A))) \to B = S (x) (A)$
17	16	eqcomd	$⊢ ((φ \land (x \in P \land y \in P)) \land (B = S (x) (A) \land B = S (y) (A))) \to S (x) (A) = B$
18		simprr	$⊢ ((φ \land (x \in P \land y \in P)) \land (B = S (x) (A) \land B = S (y) (A))) \to B = S (y) (A)$
19	18	eqcomd	$⊢ ((φ \land (x \in P \land y \in P)) \land (B = S (x) (A) \land B = S (y) (A))) \to S (y) (A) = B$
20	1 2 3 4 6 11 12 13 14 15 17 19	miduniq	$⊢ ((φ \land (x \in P \land y \in P)) \land (B = S (x) (A) \land B = S (y) (A))) \to x = y$
21	20	ex	$⊢ (φ \land (x \in P \land y \in P)) \to ((B = S (x) (A) \land B = S (y) (A)) \to x = y)$
22	21	ralrimivva	$⊢ φ \to \forall x \in P \forall y \in P ((B = S (x) (A) \land B = S (y) (A)) \to x = y)$
23		fveq2	$⊢ x = y \to S (x) = S (y)$
24	23	fveq1d	$⊢ x = y \to S (x) (A) = S (y) (A)$
25	24	eqeq2d	$⊢ x = y \to (B = S (x) (A) \leftrightarrow B = S (y) (A))$
26	25	rmo4	$⊢ \exists^{*} x \in P B = S (x) (A) \leftrightarrow \forall x \in P \forall y \in P ((B = S (x) (A) \land B = S (y) (A)) \to x = y)$
27	22 26	sylibr	$⊢ φ \to \exists^{*} x \in P B = S (x) (A)$
28		reu5	$⊢ \exists! x \in P B = S (x) (A) \leftrightarrow (\exists x \in P B = S (x) (A) \land \exists^{*} x \in P B = S (x) (A))$
29	10 27 28	sylanbrc	$⊢ φ \to \exists! x \in P B = S (x) (A)$

Metamath Proof Explorer

Theorem mideu

Proof