Theorem tgrpbase

Description: The base set of the translation group is the set of all translations (for a fiducial co-atom W ). (Contributed by NM, 5-Jun-2013)

	Ref	Expression
Hypotheses	tgrpset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	tgrpset.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	tgrpset.g	$$⊢G=\mathrm{TGrp}\left(K\right)\left(W\right)$$
	tgrp.c	$$⊢C={\mathrm{Base}}_G$$
Assertion	tgrpbase	$$⊢\left(K\in V\wedge W\in H\right)\to C=T$$

Proof

Step	Hyp	Ref	Expression
1		tgrpset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		tgrpset.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		tgrpset.g	$$⊢G=\mathrm{TGrp}\left(K\right)\left(W\right)$$
4		tgrp.c	$$⊢C={\mathrm{Base}}_G$$
5	1 2 3	tgrpset	$$⊢\left(K\in V\wedge W\in H\right)\to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩\right\}$$
6	5	fveq2d	$$⊢\left(K\in V\wedge W\in H\right)\to {\mathrm{Base}}_G={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩\right\}}$$
7	2	fvexi	$$⊢T\in \mathrm{V}$$
8		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩\right\}$$
9	8	grpbase	$$⊢T\in \mathrm{V}\to T={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩\right\}}$$
10	7 9	ax-mp	$$⊢T={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩\right\}}$$
11	6 4 10	3eqtr4g	$$⊢\left(K\in V\wedge W\in H\right)\to C=T$$