Theorem tgrpopr

Description: The group operation of the translation group is function composition. (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	tgrpopr	|- ( ( K e. V /\ W e. H ) -> .+ = ( f e. T , g e. T |-> ( f o. g ) ) )

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	tgrpset	|- ( ( K e. V /\ W e. H ) -> G = { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } )
6	5	fveq2d	|- ( ( K e. V /\ W e. H ) -> ( +g ` G ) = ( +g ` { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } ) )
7	2	fvexi	|- T e. _V
8	7 7	mpoex	|- ( f e. T , g e. T |-> ( f o. g ) ) e. _V
9		eqid	|- { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } = { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. }
10	9	grpplusg	|- ( ( f e. T , g e. T |-> ( f o. g ) ) e. _V -> ( f e. T , g e. T |-> ( f o. g ) ) = ( +g ` { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } ) )
11	8 10	ax-mp	|- ( f e. T , g e. T |-> ( f o. g ) ) = ( +g ` { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } )
12	6 4 11	3eqtr4g	|- ( ( K e. V /\ W e. H ) -> .+ = ( f e. T , g e. T |-> ( f o. g ) ) )