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 = ( LHyp ` K )
	tgrpset.t	|- T = ( ( LTrn ` K ) ` W )
	tgrpset.g	|- G = ( ( TGrp ` K ) ` W )
	tgrp.c	|- C = ( Base ` G )
Assertion	tgrpbase	|- ( ( K e. V /\ W e. H ) -> C = T )

Proof

Step	Hyp	Ref	Expression
1		tgrpset.h	|- H = ( LHyp ` K )
2		tgrpset.t	|- T = ( ( LTrn ` K ) ` W )
3		tgrpset.g	|- G = ( ( TGrp ` K ) ` W )
4		tgrp.c	|- C = ( Base ` G )
5	1 2 3	tgrpset	|- ( ( K e. V /\ W e. H ) -> G = { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } )
6	5	fveq2d	|- ( ( K e. V /\ W e. H ) -> ( Base ` G ) = ( Base ` { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } ) )
7	2	fvexi	|- T e. _V
8		eqid	|- { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } = { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. }
9	8	grpbase	|- ( T e. _V -> T = ( Base ` { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } ) )
10	7 9	ax-mp	|- T = ( Base ` { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } )
11	6 4 10	3eqtr4g	|- ( ( K e. V /\ W e. H ) -> C = T )