lmimot

Description: Line mirroring is a motion of the geometric space. Theorem 10.11 of Schwabhauser p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019)

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	1 2 3 4 5 6 7 8	lmif1o	$⊢ φ \to M : P \underset{1-1 onto}{⟶} P$
10	4	adantr	$⊢ (φ \land (a \in P \land b \in P)) \to G \in 𝒢_{Tarski}$
11	5	adantr	$⊢ (φ \land (a \in P \land b \in P)) \to G {Dim}_{𝒢} \geq 2$
12	8	adantr	$⊢ (φ \land (a \in P \land b \in P)) \to D \in ran L$
13		simprl	$⊢ (φ \land (a \in P \land b \in P)) \to a \in P$
14		simprr	$⊢ (φ \land (a \in P \land b \in P)) \to b \in P$
15	1 2 3 10 11 6 7 12 13 14	lmiiso	$⊢ (φ \land (a \in P \land b \in P)) \to M (a) \underset{˙}{-} M (b) = a \underset{˙}{-} b$
16	15	ralrimivva	$⊢ φ \to \forall a \in P \forall b \in P M (a) \underset{˙}{-} M (b) = a \underset{˙}{-} b$
17	1 2	ismot	$⊢ G \in 𝒢_{Tarski} \to (M \in (G Ismt G) \leftrightarrow (M : P \underset{1-1 onto}{⟶} P \land \forall a \in P \forall b \in P M (a) \underset{˙}{-} M (b) = a \underset{˙}{-} b))$
18	4 17	syl	$⊢ φ \to (M \in (G Ismt G) \leftrightarrow (M : P \underset{1-1 onto}{⟶} P \land \forall a \in P \forall b \in P M (a) \underset{˙}{-} M (b) = a \underset{˙}{-} b))$
19	9 16 18	mpbir2and	$⊢ φ \to M \in (G Ismt G)$

Metamath Proof Explorer