Metamath Proof Explorer

Theorem cnvmot

Description: The converse of a motion is a motion. (Contributed by Thierry Arnoux, 15-Dec-2019)

Ref Expression
Hypotheses ismot.p ⊢ P = Base G
ismot.m ⊢ - ˙ = dist ⁡ G
motgrp.1 ⊢ φ → G ∈ V
motco.2 ⊢ φ → F ∈ G Ismt G
Assertion cnvmot ⊢ φ → F -1 ∈ G Ismt G

Proof

Step Hyp Ref Expression
1 ismot.p ⊢ P = Base G
2 ismot.m ⊢ - ˙ = dist ⁡ G
3 motgrp.1 ⊢ φ → G ∈ V
4 motco.2 ⊢ φ → F ∈ G Ismt G
5 1 2 3 4 motf1o ⊢ φ → F : P ⟶ 1-1 onto P
6 f1ocnv ⊢ F : P ⟶ 1-1 onto P → F -1 : P ⟶ 1-1 onto P
7 5 6 syl ⊢ φ → F -1 : P ⟶ 1-1 onto P
8 3 adantr ⊢ φ ∧ a ∈ P ∧ b ∈ P → G ∈ V
9 f1of ⊢ F -1 : P ⟶ 1-1 onto P → F -1 : P ⟶ P
10 7 9 syl ⊢ φ → F -1 : P ⟶ P
11 10 adantr ⊢ φ ∧ a ∈ P ∧ b ∈ P → F -1 : P ⟶ P
12 simprl ⊢ φ ∧ a ∈ P ∧ b ∈ P → a ∈ P
13 11 12 ffvelrnd ⊢ φ ∧ a ∈ P ∧ b ∈ P → F -1 ⁡ a ∈ P
14 simprr ⊢ φ ∧ a ∈ P ∧ b ∈ P → b ∈ P
15 11 14 ffvelrnd ⊢ φ ∧ a ∈ P ∧ b ∈ P → F -1 ⁡ b ∈ P
16 4 adantr ⊢ φ ∧ a ∈ P ∧ b ∈ P → F ∈ G Ismt G
17 1 2 8 13 15 16 motcgr ⊢ φ ∧ a ∈ P ∧ b ∈ P → F ⁡ F -1 ⁡ a - ˙ F ⁡ F -1 ⁡ b = F -1 ⁡ a - ˙ F -1 ⁡ b
18 f1ocnvfv2 ⊢ F : P ⟶ 1-1 onto P ∧ a ∈ P → F ⁡ F -1 ⁡ a = a
19 5 12 18 syl2an2r ⊢ φ ∧ a ∈ P ∧ b ∈ P → F ⁡ F -1 ⁡ a = a
20 f1ocnvfv2 ⊢ F : P ⟶ 1-1 onto P ∧ b ∈ P → F ⁡ F -1 ⁡ b = b
21 5 14 20 syl2an2r ⊢ φ ∧ a ∈ P ∧ b ∈ P → F ⁡ F -1 ⁡ b = b
22 19 21 oveq12d ⊢ φ ∧ a ∈ P ∧ b ∈ P → F ⁡ F -1 ⁡ a - ˙ F ⁡ F -1 ⁡ b = a - ˙ b
23 17 22 eqtr3d ⊢ φ ∧ a ∈ P ∧ b ∈ P → F -1 ⁡ a - ˙ F -1 ⁡ b = a - ˙ b
24 23 ralrimivva ⊢ φ → ∀ a ∈ P ∀ b ∈ P F -1 ⁡ a - ˙ F -1 ⁡ b = a - ˙ b
25 1 2 ismot ⊢ G ∈ V → F -1 ∈ G Ismt G ↔ F -1 : P ⟶ 1-1 onto P ∧ ∀ a ∈ P ∀ b ∈ P F -1 ⁡ a - ˙ F -1 ⁡ b = a - ˙ b
26 3 25 syl ⊢ φ → F -1 ∈ G Ismt G ↔ F -1 : P ⟶ 1-1 onto P ∧ ∀ a ∈ P ∀ b ∈ P F -1 ⁡ a - ˙ F -1 ⁡ b = a - ˙ b
27 7 24 26 mpbir2and ⊢ φ → F -1 ∈ G Ismt G