lmireu

Description: Any point has a unique antecedent through line mirroring. Theorem 10.6 of Schwabhauser p. 89. (Contributed by Thierry Arnoux, 11-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$
	lmif.m	$⊢ M = {lInv}_{𝒢} (G) (D)$
	lmif.l	$⊢ L = {Line}_{𝒢} (G)$
	lmif.d	$⊢ φ \to D \in ran L$
	lmicl.1	$⊢ φ \to A \in P$
Assertion	lmireu	$⊢ φ \to \exists! b \in P M (b) = A$

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		lmif.m	$⊢ M = {lInv}_{𝒢} (G) (D)$
7		lmif.l	$⊢ L = {Line}_{𝒢} (G)$
8		lmif.d	$⊢ φ \to D \in ran L$
9		lmicl.1	$⊢ φ \to A \in P$
10	1 2 3 4 5 6 7 8 9	lmicl	$⊢ φ \to M (A) \in P$
11	1 2 3 4 5 6 7 8 9	lmilmi	$⊢ φ \to M (M (A)) = A$
12	4	ad2antrr	$⊢ ((φ \land b \in P) \land M (b) = A) \to G \in 𝒢_{Tarski}$
13	5	ad2antrr	$⊢ ((φ \land b \in P) \land M (b) = A) \to G {Dim}_{𝒢} \geq 2$
14	8	ad2antrr	$⊢ ((φ \land b \in P) \land M (b) = A) \to D \in ran L$
15		simplr	$⊢ ((φ \land b \in P) \land M (b) = A) \to b \in P$
16	1 2 3 12 13 6 7 14 15	lmilmi	$⊢ ((φ \land b \in P) \land M (b) = A) \to M (M (b)) = b$
17		simpr	$⊢ ((φ \land b \in P) \land M (b) = A) \to M (b) = A$
18	17	fveq2d	$⊢ ((φ \land b \in P) \land M (b) = A) \to M (M (b)) = M (A)$
19	16 18	eqtr3d	$⊢ ((φ \land b \in P) \land M (b) = A) \to b = M (A)$
20	19	ex	$⊢ (φ \land b \in P) \to (M (b) = A \to b = M (A))$
21	20	ralrimiva	$⊢ φ \to \forall b \in P (M (b) = A \to b = M (A))$
22		fveqeq2	$⊢ b = M (A) \to (M (b) = A \leftrightarrow M (M (A)) = A)$
23	22	eqreu	$⊢ (M (A) \in P \land M (M (A)) = A \land \forall b \in P (M (b) = A \to b = M (A))) \to \exists! b \in P M (b) = A$
24	10 11 21 23	syl3anc	$⊢ φ \to \exists! b \in P M (b) = A$

Metamath Proof Explorer

Theorem lmireu

Proof