Theorem tgrpgrp

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

	Ref	Expression
Hypotheses	tgrpgrp.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	tgrpgrp.g	$$⊢G=\mathrm{TGrp}\left(K\right)\left(W\right)$$
Assertion	tgrpgrp	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to G\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		tgrpgrp.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		tgrpgrp.g	$$⊢G=\mathrm{TGrp}\left(K\right)\left(W\right)$$
3		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
4		eqid	$$⊢{+}_G={+}_G$$
5		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
6	1 3 2 4 5	tgrpgrplem	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to G\in \mathrm{Grp}$$