Metamath Proof Explorer


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 )