Description: Closure of motions. (Contributed by Thierry Arnoux, 15-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ismot.p | ⊢ 𝑃 = ( Base ‘ 𝐺 ) | |
ismot.m | ⊢ − = ( dist ‘ 𝐺 ) | ||
motgrp.1 | ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 ) | ||
motco.2 | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ) | ||
motcl.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) | ||
Assertion | motcl | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑃 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismot.p | ⊢ 𝑃 = ( Base ‘ 𝐺 ) | |
2 | ismot.m | ⊢ − = ( dist ‘ 𝐺 ) | |
3 | motgrp.1 | ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 ) | |
4 | motco.2 | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ) | |
5 | motcl.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) | |
6 | 1 2 3 4 | motf1o | ⊢ ( 𝜑 → 𝐹 : 𝑃 –1-1-onto→ 𝑃 ) |
7 | f1of | ⊢ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 → 𝐹 : 𝑃 ⟶ 𝑃 ) | |
8 | 6 7 | syl | ⊢ ( 𝜑 → 𝐹 : 𝑃 ⟶ 𝑃 ) |
9 | 8 5 | ffvelrnd | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑃 ) |