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