This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tgrpov

Description: The group operation value of the translation group is the composition of translations. (Contributed by NM, 5-Jun-2013)

Ref Expression
Hypotheses tgrpset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tgrpset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tgrpset.g ⊢ 𝐺 = ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 )
tgrp.o ⊢ + = ( +g ‘ 𝐺 )
Assertion tgrpov ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑇 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 tgrpset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 tgrpset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tgrpset.g ⊢ 𝐺 = ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 )
4 tgrp.o ⊢ + = ( +g ‘ 𝐺 )
5 1 2 3 4 tgrpopr ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → + = ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) )
6 5 3adant3 ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑇 ) ) → + = ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) )
7 6 oveqd ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑇 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) 𝑌 ) )
8 simp3l ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑇 ) ) → 𝑋 ∈ 𝑇 )
9 simp3r ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑇 ) ) → 𝑌 ∈ 𝑇 )
10 coexg ⊢ ( ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑇 ) → ( 𝑋 ∘ 𝑌 ) ∈ V )
11 10 3ad2ant3 ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑇 ) ) → ( 𝑋 ∘ 𝑌 ) ∈ V )
12 coeq1 ⊢ ( 𝑓 = 𝑋 → ( 𝑓 ∘ 𝑔 ) = ( 𝑋 ∘ 𝑔 ) )
13 coeq2 ⊢ ( 𝑔 = 𝑌 → ( 𝑋 ∘ 𝑔 ) = ( 𝑋 ∘ 𝑌 ) )
14 eqid ⊢ ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) )
15 12 13 14 ovmpog ⊢ ( ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑇 ∧ ( 𝑋 ∘ 𝑌 ) ∈ V ) → ( 𝑋 ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )
16 8 9 11 15 syl3anc ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑇 ) ) → ( 𝑋 ( 𝑓 ∈ 𝑇 , 𝑔 ∈ 𝑇 ↦ ( 𝑓 ∘ 𝑔 ) ) 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )
17 7 16 eqtrd ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑇 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )