Metamath Proof Explorer

Theorem motcgr

Description: Property of a motion: distances are preserved. (Contributed by Thierry Arnoux, 15-Dec-2019)

Ref Expression
Hypotheses ismot.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
ismot.m ⊢ − = ( dist ‘ 𝐺 )
motgrp.1 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
motcgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
motcgr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
motcgr.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
Assertion motcgr ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) = ( 𝐴 − 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ismot.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ismot.m ⊢ − = ( dist ‘ 𝐺 )
3 motgrp.1 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4 motcgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5 motcgr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6 motcgr.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
7 1 2 ismot ⊢ ( 𝐺 ∈ 𝑉 → ( 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )
8 3 7 syl ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) ↔ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) ) )
9 6 8 mpbid ⊢ ( 𝜑 → ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) )
10 9 simprd ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) )
11 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝐴 ) )
12 11 oveq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑏 ) ) )
13 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 − 𝑏 ) = ( 𝐴 − 𝑏 ) )
14 12 13 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ↔ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝐴 − 𝑏 ) ) )
15 fveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝐵 ) )
16 15 oveq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) )
17 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 − 𝑏 ) = ( 𝐴 − 𝐵 ) )
18 16 17 eqeq12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝐴 − 𝑏 ) ↔ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) = ( 𝐴 − 𝐵 ) ) )
19 14 18 rspc2va ⊢ ( ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ( 𝐹 ‘ 𝑎 ) − ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 − 𝑏 ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) = ( 𝐴 − 𝐵 ) )
20 4 5 10 19 syl21anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝐵 ) ) = ( 𝐴 − 𝐵 ) )