This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ HL ∧ W ∈ H → G ∈ 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
5 eqid ⊢ Base K = Base K
6 1 3 2 4 5 tgrpgrplem ⊢ K ∈ HL ∧ W ∈ H → G ∈ Grp