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)

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 \in V \land W \in H) \to G = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩\}$
6	5	fveq2d	$⊢ (K \in V \land W \in H) \to {Base}_{G} = {Base}_{\{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩\}}$
7	2	fvexi	$⊢ T \in V$
8		eqid	$⊢ \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩\} = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩\}$
9	8	grpbase	$⊢ T \in V \to T = {Base}_{\{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩\}}$
10	7 9	ax-mp	$⊢ T = {Base}_{\{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩\}}$
11	6 4 10	3eqtr4g	$⊢ (K \in V \land W \in H) \to C = T$

Metamath Proof Explorer