Theorem tgrpgrp

Description: The translation group is a group. (Contributed by NM, 6-Jun-2013)

	Ref	Expression
Hypotheses	tgrpgrp.h	|- H = ( LHyp ` K )
	tgrpgrp.g	|- G = ( ( TGrp ` K ) ` W )
Assertion	tgrpgrp	|- ( ( K e. HL /\ W e. H ) -> G e. Grp )

Proof

Step	Hyp	Ref	Expression
1		tgrpgrp.h	|- H = ( LHyp ` K )
2		tgrpgrp.g	|- G = ( ( TGrp ` K ) ` W )
3		eqid	|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
4		eqid	|- ( +g ` G ) = ( +g ` G )
5		eqid	|- ( Base ` K ) = ( Base ` K )
6	1 3 2 4 5	tgrpgrplem	|- ( ( K e. HL /\ W e. H ) -> G e. Grp )