Theorem tgrpopr

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

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