Metamath Proof Explorer

Theorem motcgrg

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 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
motgrp.i ⊢ 𝐼 = { ⟨ ( Base ‘ ndx ) , ( 𝐺 Ismt 𝐺 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐺 Ismt 𝐺 ) , 𝑔 ∈ ( 𝐺 Ismt 𝐺 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ }
motcgrg.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
motcgrg.t ⊢ ( 𝜑 → 𝑇 ∈ Word 𝑃 )
motcgrg.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
Assertion motcgrg ( 𝜑 → ( 𝐹 ∘ 𝑇 ) ∼ 𝑇 )

Proof

Step Hyp Ref Expression
1 ismot.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ismot.m ⊢ − = ( dist ‘ 𝐺 )
3 motgrp.1 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4 motgrp.i ⊢ 𝐼 = { ⟨ ( Base ‘ ndx ) , ( 𝐺 Ismt 𝐺 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐺 Ismt 𝐺 ) , 𝑔 ∈ ( 𝐺 Ismt 𝐺 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ }
5 motcgrg.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
6 motcgrg.t ⊢ ( 𝜑 → 𝑇 ∈ Word 𝑃 )
7 motcgrg.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
8 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) → 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 )
9 8 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 )
10 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) )
11 1 2 3 7 motf1o ⊢ ( 𝜑 → 𝐹 : 𝑃 –1-1-onto→ 𝑃 )
12 f1of ⊢ ( 𝐹 : 𝑃 –1-1-onto→ 𝑃 → 𝐹 : 𝑃 ⟶ 𝑃 )
13 11 12 syl ⊢ ( 𝜑 → 𝐹 : 𝑃 ⟶ 𝑃 )
14 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) → 𝐹 : 𝑃 ⟶ 𝑃 )
15 fco ⊢ ( ( 𝐹 : 𝑃 ⟶ 𝑃 ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) → ( 𝐹 ∘ 𝑇 ) : ( 0 ..^ 𝑛 ) ⟶ 𝑃 )
16 14 8 15 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) → ( 𝐹 ∘ 𝑇 ) : ( 0 ..^ 𝑛 ) ⟶ 𝑃 )
17 16 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → ( 𝐹 ∘ 𝑇 ) : ( 0 ..^ 𝑛 ) ⟶ 𝑃 )
18 17 fdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → dom ( 𝐹 ∘ 𝑇 ) = ( 0 ..^ 𝑛 ) )
19 10 18 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → 𝑎 ∈ ( 0 ..^ 𝑛 ) )
20 fvco3 ⊢ ( ( 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ∧ 𝑎 ∈ ( 0 ..^ 𝑛 ) ) → ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑇 ‘ 𝑎 ) ) )
21 9 19 20 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑇 ‘ 𝑎 ) ) )
22 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) )
23 22 18 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → 𝑏 ∈ ( 0 ..^ 𝑛 ) )
24 fvco3 ⊢ ( ( 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ∧ 𝑏 ∈ ( 0 ..^ 𝑛 ) ) → ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑏 ) = ( 𝐹 ‘ ( 𝑇 ‘ 𝑏 ) ) )
25 9 23 24 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑏 ) = ( 𝐹 ‘ ( 𝑇 ‘ 𝑏 ) ) )
26 21 25 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → ( ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑎 ) − ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑏 ) ) = ( ( 𝐹 ‘ ( 𝑇 ‘ 𝑎 ) ) − ( 𝐹 ‘ ( 𝑇 ‘ 𝑏 ) ) ) )
27 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) → 𝐺 ∈ 𝑉 )
28 27 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → 𝐺 ∈ 𝑉 )
29 9 19 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → ( 𝑇 ‘ 𝑎 ) ∈ 𝑃 )
30 9 23 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → ( 𝑇 ‘ 𝑏 ) ∈ 𝑃 )
31 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → 𝐹 ∈ ( 𝐺 Ismt 𝐺 ) )
32 1 2 28 29 30 31 motcgr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → ( ( 𝐹 ‘ ( 𝑇 ‘ 𝑎 ) ) − ( 𝐹 ‘ ( 𝑇 ‘ 𝑏 ) ) ) = ( ( 𝑇 ‘ 𝑎 ) − ( 𝑇 ‘ 𝑏 ) ) )
33 26 32 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) ∧ ( 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∧ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ) ) → ( ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑎 ) − ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑏 ) ) = ( ( 𝑇 ‘ 𝑎 ) − ( 𝑇 ‘ 𝑏 ) ) )
34 33 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) → ∀ 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∀ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ( ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑎 ) − ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑏 ) ) = ( ( 𝑇 ‘ 𝑎 ) − ( 𝑇 ‘ 𝑏 ) ) )
35 fzo0ssnn0 ⊢ ( 0 ..^ 𝑛 ) ⊆ ℕ0
36 nn0ssre ⊢ ℕ0 ⊆ ℝ
37 35 36 sstri ⊢ ( 0 ..^ 𝑛 ) ⊆ ℝ
38 37 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) → ( 0 ..^ 𝑛 ) ⊆ ℝ )
39 1 2 5 27 38 16 8 iscgrgd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) → ( ( 𝐹 ∘ 𝑇 ) ∼ 𝑇 ↔ ∀ 𝑎 ∈ dom ( 𝐹 ∘ 𝑇 ) ∀ 𝑏 ∈ dom ( 𝐹 ∘ 𝑇 ) ( ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑎 ) − ( ( 𝐹 ∘ 𝑇 ) ‘ 𝑏 ) ) = ( ( 𝑇 ‘ 𝑎 ) − ( 𝑇 ‘ 𝑏 ) ) ) )
40 34 39 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 ) → ( 𝐹 ∘ 𝑇 ) ∼ 𝑇 )
41 iswrd ⊢ ( 𝑇 ∈ Word 𝑃 ↔ ∃ 𝑛 ∈ ℕ0 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 )
42 6 41 sylib ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 𝑇 : ( 0 ..^ 𝑛 ) ⟶ 𝑃 )
43 40 42 r19.29a ⊢ ( 𝜑 → ( 𝐹 ∘ 𝑇 ) ∼ 𝑇 )