tgrpov

Description: The group operation value of the translation group is the composition of translations. (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	tgrpov	$⊢ (K \in V \land W \in H \land (X \in T \land Y \in T)) \to X \underset{˙}{+} Y = X \circ Y$

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 4	tgrpopr	$⊢ (K \in V \land W \in H) \to \underset{˙}{+} = (f \in T, g \in T ⟼ f \circ g)$
6	5	3adant3	$⊢ (K \in V \land W \in H \land (X \in T \land Y \in T)) \to \underset{˙}{+} = (f \in T, g \in T ⟼ f \circ g)$
7	6	oveqd	$⊢ (K \in V \land W \in H \land (X \in T \land Y \in T)) \to X \underset{˙}{+} Y = X (f \in T, g \in T ⟼ f \circ g) Y$
8		simp3l	$⊢ (K \in V \land W \in H \land (X \in T \land Y \in T)) \to X \in T$
9		simp3r	$⊢ (K \in V \land W \in H \land (X \in T \land Y \in T)) \to Y \in T$
10		coexg	$⊢ (X \in T \land Y \in T) \to X \circ Y \in V$
11	10	3ad2ant3	$⊢ (K \in V \land W \in H \land (X \in T \land Y \in T)) \to X \circ Y \in V$
12		coeq1	$⊢ f = X \to f \circ g = X \circ g$
13		coeq2	$⊢ g = Y \to X \circ g = X \circ Y$
14		eqid	$⊢ (f \in T, g \in T ⟼ f \circ g) = (f \in T, g \in T ⟼ f \circ g)$
15	12 13 14	ovmpog	$⊢ (X \in T \land Y \in T \land X \circ Y \in V) \to X (f \in T, g \in T ⟼ f \circ g) Y = X \circ Y$
16	8 9 11 15	syl3anc	$⊢ (K \in V \land W \in H \land (X \in T \land Y \in T)) \to X (f \in T, g \in T ⟼ f \circ g) Y = X \circ Y$
17	7 16	eqtrd	$⊢ (K \in V \land W \in H \land (X \in T \land Y \in T)) \to X \underset{˙}{+} Y = X \circ Y$

Metamath Proof Explorer