Step |
Hyp |
Ref |
Expression |
1 |
|
ismot.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
ismot.m |
⊢ − = ( dist ‘ 𝐺 ) |
3 |
|
motgrp.1 |
⊢ ( 𝜑 → 𝐺 ∈ 𝑉 ) |
4 |
|
motco.2 |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ) |
5 |
1 2
|
ismot |
⊢ ( 𝐺 ∈ 𝑉 → ( 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) ) |
6 |
3 5
|
syl |
⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) ) |
7 |
4 6
|
mpbid |
⊢ ( 𝜑 → ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) |
8 |
7
|
simpld |
⊢ ( 𝜑 → 𝐹 : 𝑃 –1-1-onto→ 𝑃 ) |