tgrpopr

Description: The group operation of the translation group is function composition. (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.o	$⊢ \underset{˙}{+} = +_{G}$
Assertion	tgrpopr	$⊢ (K \in V \land W \in H) \to \underset{˙}{+} = (f \in T, g \in T ⟼ f \circ g)$

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

Metamath Proof Explorer