Metamath Proof Explorer


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

Ref Expression
Hypotheses ismid.p P = Base G
ismid.d - ˙ = dist G
ismid.i I = Itv G
ismid.g φ G 𝒢 Tarski
ismid.1 φ G Dim 𝒢 2
lmif.m M = lInv 𝒢 G D
lmif.l L = Line 𝒢 G
lmif.d φ D ran L
Assertion lmimot φ M G Ismt G

Proof

Step Hyp Ref Expression
1 ismid.p P = Base G
2 ismid.d - ˙ = dist G
3 ismid.i I = Itv G
4 ismid.g φ G 𝒢 Tarski
5 ismid.1 φ G Dim 𝒢 2
6 lmif.m M = lInv 𝒢 G D
7 lmif.l L = Line 𝒢 G
8 lmif.d φ D ran L
9 1 2 3 4 5 6 7 8 lmif1o φ M : P 1-1 onto P
10 4 adantr φ a P b P G 𝒢 Tarski
11 5 adantr φ a P b P G Dim 𝒢 2
12 8 adantr φ a P b P D ran L
13 simprl φ a P b P a P
14 simprr φ a P b P b P
15 1 2 3 10 11 6 7 12 13 14 lmiiso φ a P b P M a - ˙ M b = a - ˙ b
16 15 ralrimivva φ a P b P M a - ˙ M b = a - ˙ b
17 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
18 4 17 syl φ M G Ismt G M : P 1-1 onto P a P b P M a - ˙ M b = a - ˙ b
19 9 16 18 mpbir2and φ M G Ismt G