Metamath Proof Explorer


Theorem 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)

Ref Expression
Hypotheses mirval.p P = Base G
mirval.d - ˙ = dist G
mirval.i I = Itv G
mirval.l L = Line 𝒢 G
mirval.s S = pInv 𝒢 G
mirval.g φ G 𝒢 Tarski
mirmot.m M = S A
mirmot.a φ A P
Assertion mirmot φ M G Ismt G

Proof

Step Hyp Ref Expression
1 mirval.p P = Base G
2 mirval.d - ˙ = dist G
3 mirval.i I = Itv G
4 mirval.l L = Line 𝒢 G
5 mirval.s S = pInv 𝒢 G
6 mirval.g φ G 𝒢 Tarski
7 mirmot.m M = S A
8 mirmot.a φ A P
9 1 2 3 4 5 6 8 7 mirf1o φ M : P 1-1 onto P
10 6 adantr φ a P b P G 𝒢 Tarski
11 8 adantr φ a P b P A P
12 simprl φ a P b P a P
13 simprr φ a P b P b P
14 1 2 3 4 5 10 11 7 12 13 miriso φ a P b P M a - ˙ M b = a - ˙ b
15 14 ralrimivva φ a P b P M a - ˙ M b = a - ˙ b
16 1 2 ismot G 𝒢 Tarski M G Ismt G M : P 1-1 onto P a P b P M a - ˙ M b = a - ˙ b
17 6 16 syl φ M G Ismt G M : P 1-1 onto P a P b P M a - ˙ M b = a - ˙ b
18 9 15 17 mpbir2and φ M G Ismt G