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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
ismot.m ⊢ − = ( dist ‘ 𝐺 )
motgrp.1 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
motco.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
Assertion cnvmot ( 𝜑 → ◡ 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )

Proof

Step Hyp Ref Expression
1 ismot.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ismot.m ⊢ − = ( dist ‘ 𝐺 )
3 motgrp.1 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4 motco.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
5 1 2 3 4 motf1o ⊢ ( 𝜑 → 𝐹 : 𝑃 –1-1-onto→ 𝑃 )
6 f1ocnv ⊢ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 → ◡ 𝐹 : 𝑃 –1-1-onto→ 𝑃 )
7 5 6 syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝑃 –1-1-onto→ 𝑃 )
8 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝐺 ∈ 𝑉 )
9 f1of ⊢ ( ◡ 𝐹 : 𝑃 –1-1-onto→ 𝑃 → ◡ 𝐹 : 𝑃 ⟶ 𝑃 )
10 7 9 syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝑃 ⟶ 𝑃 )
11 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ◡ 𝐹 : 𝑃 ⟶ 𝑃 )
12 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝑎 ∈ 𝑃 )
13 11 12 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ◡ 𝐹 ‘ 𝑎 ) ∈ 𝑃 )
14 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝑏 ∈ 𝑃 )
15 11 14 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝑃 )
16 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
17 1 2 8 13 15 16 motcgr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) − ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( ( ◡ 𝐹 ‘ 𝑎 ) − ( ◡ 𝐹 ‘ 𝑏 ) ) )
18 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ 𝑎 ∈ 𝑃 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) = 𝑎 )
19 5 12 18 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) = 𝑎 )
20 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ 𝑏 ∈ 𝑃 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = 𝑏 )
21 5 14 20 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = 𝑏 )
22 19 21 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑎 ) ) − ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝑎 − 𝑏 ) )
23 17 22 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ( ( ◡ 𝐹 ‘ 𝑎 ) − ( ◡ 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) )
24 23 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( ◡ 𝐹 ‘ 𝑎 ) − ( ◡ 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) )
25 1 2 ismot ⊢ ( 𝐺 ∈ 𝑉 → ( ◡ 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( ◡ 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( ◡ 𝐹 ‘ 𝑎 ) − ( ◡ 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )
26 3 25 syl ⊢ ( 𝜑 → ( ◡ 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( ◡ 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( ◡ 𝐹 ‘ 𝑎 ) − ( ◡ 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )
27 7 24 26 mpbir2and ⊢ ( 𝜑 → ◡ 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )