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