Step | Hyp | Ref
| Expression |
1 | | ismot.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
2 | | ismot.m |
. . . 4
⊢ − =
(dist‘𝐺) |
3 | | motgrp.1 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
4 | | motco.2 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐺Ismt𝐺)) |
5 | 1, 2, 3, 4 | motf1o 25433 |
. . 3
⊢ (𝜑 → 𝐹:𝑃–1-1-onto→𝑃) |
6 | | f1ocnv 6149 |
. . 3
⊢ (𝐹:𝑃–1-1-onto→𝑃 → ◡𝐹:𝑃–1-1-onto→𝑃) |
7 | 5, 6 | syl 17 |
. 2
⊢ (𝜑 → ◡𝐹:𝑃–1-1-onto→𝑃) |
8 | 3 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝐺 ∈ 𝑉) |
9 | | f1of 6137 |
. . . . . . . 8
⊢ (◡𝐹:𝑃–1-1-onto→𝑃 → ◡𝐹:𝑃⟶𝑃) |
10 | 7, 9 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ◡𝐹:𝑃⟶𝑃) |
11 | 10 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ◡𝐹:𝑃⟶𝑃) |
12 | | simprl 794 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝑎 ∈ 𝑃) |
13 | 11, 12 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (◡𝐹‘𝑎) ∈ 𝑃) |
14 | | simprr 796 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝑏 ∈ 𝑃) |
15 | 11, 14 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (◡𝐹‘𝑏) ∈ 𝑃) |
16 | 4 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝐹 ∈ (𝐺Ismt𝐺)) |
17 | 1, 2, 8, 13, 15, 16 | motcgr 25431 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐹‘(◡𝐹‘𝑎)) − (𝐹‘(◡𝐹‘𝑏))) = ((◡𝐹‘𝑎) − (◡𝐹‘𝑏))) |
18 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝐹:𝑃–1-1-onto→𝑃) |
19 | | f1ocnvfv2 6533 |
. . . . . 6
⊢ ((𝐹:𝑃–1-1-onto→𝑃 ∧ 𝑎 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑎)) = 𝑎) |
20 | 18, 12, 19 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (𝐹‘(◡𝐹‘𝑎)) = 𝑎) |
21 | | f1ocnvfv2 6533 |
. . . . . 6
⊢ ((𝐹:𝑃–1-1-onto→𝑃 ∧ 𝑏 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏) |
22 | 18, 14, 21 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏) |
23 | 20, 22 | oveq12d 6668 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝐹‘(◡𝐹‘𝑎)) − (𝐹‘(◡𝐹‘𝑏))) = (𝑎 − 𝑏)) |
24 | 17, 23 | eqtr3d 2658 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((◡𝐹‘𝑎) − (◡𝐹‘𝑏)) = (𝑎 − 𝑏)) |
25 | 24 | ralrimivva 2971 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ((◡𝐹‘𝑎) − (◡𝐹‘𝑏)) = (𝑎 − 𝑏)) |
26 | 1, 2 | ismot 25430 |
. . 3
⊢ (𝐺 ∈ 𝑉 → (◡𝐹 ∈ (𝐺Ismt𝐺) ↔ (◡𝐹:𝑃–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ((◡𝐹‘𝑎) − (◡𝐹‘𝑏)) = (𝑎 − 𝑏)))) |
27 | 3, 26 | syl 17 |
. 2
⊢ (𝜑 → (◡𝐹 ∈ (𝐺Ismt𝐺) ↔ (◡𝐹:𝑃–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ((◡𝐹‘𝑎) − (◡𝐹‘𝑏)) = (𝑎 − 𝑏)))) |
28 | 7, 25, 27 | mpbir2and 957 |
1
⊢ (𝜑 → ◡𝐹 ∈ (𝐺Ismt𝐺)) |