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 ( ( 𝐾𝑉𝑊𝐻 ∧ ( 𝑋𝑇𝑌𝑇 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑋𝑌 ) )