mirmot

Description: Point investion is a motion of the geometric space. Theorem 7.14 of Schwabhauser p. 51. (Contributed by Thierry Arnoux, 15-Dec-2019)

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		mirmot.m	$⊢ M = S (A)$
8		mirmot.a	$⊢ φ \to A \in P$
9	1 2 3 4 5 6 8 7	mirf1o	$⊢ φ \to M : P \underset{1-1 onto}{⟶} P$
10	6	adantr	$⊢ (φ \land (a \in P \land b \in P)) \to G \in 𝒢_{Tarski}$
11	8	adantr	$⊢ (φ \land (a \in P \land b \in P)) \to A \in P$
12		simprl	$⊢ (φ \land (a \in P \land b \in P)) \to a \in P$
13		simprr	$⊢ (φ \land (a \in P \land b \in P)) \to b \in P$
14	1 2 3 4 5 10 11 7 12 13	miriso	$⊢ (φ \land (a \in P \land b \in P)) \to M (a) \underset{˙}{-} M (b) = a \underset{˙}{-} b$
15	14	ralrimivva	$⊢ φ \to \forall a \in P \forall b \in P M (a) \underset{˙}{-} M (b) = a \underset{˙}{-} b$
16	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))$
17	6 16	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))$
18	9 15 17	mpbir2and	$⊢ φ \to M \in (G Ismt G)$

Metamath Proof Explorer