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
|- H = ( LHyp ` K )
tgrpset.t
|- T = ( ( LTrn ` K ) ` W )
tgrpset.g
|- G = ( ( TGrp ` K ) ` W )
tgrp.o
|- .+ = ( +g ` G )
Assertion tgrpov
|- ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> ( X .+ Y ) = ( X o. Y ) )

Proof

Step Hyp Ref Expression
1 tgrpset.h
 |-  H = ( LHyp ` K )
2 tgrpset.t
 |-  T = ( ( LTrn ` K ) ` W )
3 tgrpset.g
 |-  G = ( ( TGrp ` K ) ` W )
4 tgrp.o
 |-  .+ = ( +g ` G )
5 1 2 3 4 tgrpopr
 |-  ( ( K e. V /\ W e. H ) -> .+ = ( f e. T , g e. T |-> ( f o. g ) ) )
6 5 3adant3
 |-  ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> .+ = ( f e. T , g e. T |-> ( f o. g ) ) )
7 6 oveqd
 |-  ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> ( X .+ Y ) = ( X ( f e. T , g e. T |-> ( f o. g ) ) Y ) )
8 simp3l
 |-  ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> X e. T )
9 simp3r
 |-  ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> Y e. T )
10 coexg
 |-  ( ( X e. T /\ Y e. T ) -> ( X o. Y ) e. _V )
11 10 3ad2ant3
 |-  ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> ( X o. Y ) e. _V )
12 coeq1
 |-  ( f = X -> ( f o. g ) = ( X o. g ) )
13 coeq2
 |-  ( g = Y -> ( X o. g ) = ( X o. Y ) )
14 eqid
 |-  ( f e. T , g e. T |-> ( f o. g ) ) = ( f e. T , g e. T |-> ( f o. g ) )
15 12 13 14 ovmpog
 |-  ( ( X e. T /\ Y e. T /\ ( X o. Y ) e. _V ) -> ( X ( f e. T , g e. T |-> ( f o. g ) ) Y ) = ( X o. Y ) )
16 8 9 11 15 syl3anc
 |-  ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> ( X ( f e. T , g e. T |-> ( f o. g ) ) Y ) = ( X o. Y ) )
17 7 16 eqtrd
 |-  ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> ( X .+ Y ) = ( X o. Y ) )