mirreu

Description: Any point has a unique antecedent through point inversion. Theorem 7.8 of Schwabhauser p. 50. (Contributed by Thierry Arnoux, 3-Jun-2019)

	Ref	Expression
Hypotheses	mirval.p	$⊢ P = {Base}_{G}$
	mirval.d	$⊢ \underset{˙}{-} = dist (G)$
	mirval.i	$⊢ I = Itv (G)$
	mirval.l	$⊢ L = {Line}_{𝒢} (G)$
	mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
	mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mirval.a	$⊢ φ \to A \in P$
	mirfv.m	$⊢ M = S (A)$
	mirmir.b	$⊢ φ \to B \in P$
Assertion	mirreu	$⊢ φ \to \exists! a \in P M (a) = B$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$⊢ P = {Base}_{G}$
2		mirval.d	$⊢ \underset{˙}{-} = dist (G)$
3		mirval.i	$⊢ I = Itv (G)$
4		mirval.l	$⊢ L = {Line}_{𝒢} (G)$
5		mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
6		mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		mirval.a	$⊢ φ \to A \in P$
8		mirfv.m	$⊢ M = S (A)$
9		mirmir.b	$⊢ φ \to B \in P$
10	1 2 3 4 5 6 7 8 9	mircl	$⊢ φ \to M (B) \in P$
11	1 2 3 4 5 6 7 8 9	mirmir	$⊢ φ \to M (M (B)) = B$
12	6	ad2antrr	$⊢ ((φ \land a \in P) \land M (a) = B) \to G \in 𝒢_{Tarski}$
13	7	ad2antrr	$⊢ ((φ \land a \in P) \land M (a) = B) \to A \in P$
14		simplr	$⊢ ((φ \land a \in P) \land M (a) = B) \to a \in P$
15	1 2 3 4 5 12 13 8 14	mirmir	$⊢ ((φ \land a \in P) \land M (a) = B) \to M (M (a)) = a$
16		simpr	$⊢ ((φ \land a \in P) \land M (a) = B) \to M (a) = B$
17	16	fveq2d	$⊢ ((φ \land a \in P) \land M (a) = B) \to M (M (a)) = M (B)$
18	15 17	eqtr3d	$⊢ ((φ \land a \in P) \land M (a) = B) \to a = M (B)$
19	18	ex	$⊢ (φ \land a \in P) \to (M (a) = B \to a = M (B))$
20	19	ralrimiva	$⊢ φ \to \forall a \in P (M (a) = B \to a = M (B))$
21		fveqeq2	$⊢ a = M (B) \to (M (a) = B \leftrightarrow M (M (B)) = B)$
22	21	eqreu	$⊢ (M (B) \in P \land M (M (B)) = B \land \forall a \in P (M (a) = B \to a = M (B))) \to \exists! a \in P M (a) = B$
23	10 11 20 22	syl3anc	$⊢ φ \to \exists! a \in P M (a) = B$

Metamath Proof Explorer

Theorem mirreu

Proof