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 
|- 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 ) )