ltrnco4

Description: Rearrange a composition of 4 translations, analogous to an4 . (Contributed by NM, 10-Jun-2013)

	Ref	Expression
Hypotheses	ltrncom.h	$⊢ H = LHyp (K)$
	ltrncom.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrnco4	$⊢ ((K \in HL \land W \in H) \land E \in T \land F \in T) \to (D \circ E) \circ (F \circ G) = (D \circ F) \circ (E \circ G)$

Step	Hyp	Ref	Expression
1		ltrncom.h	$⊢ H = LHyp (K)$
2		ltrncom.t	$⊢ T = LTrn (K) (W)$
3	1 2	ltrncom	$⊢ ((K \in HL \land W \in H) \land E \in T \land F \in T) \to E \circ F = F \circ E$
4	3	coeq1d	$⊢ ((K \in HL \land W \in H) \land E \in T \land F \in T) \to (E \circ F) \circ G = (F \circ E) \circ G$
5		coass	$⊢ (E \circ F) \circ G = E \circ (F \circ G)$
6		coass	$⊢ (F \circ E) \circ G = F \circ (E \circ G)$
7	4 5 6	3eqtr3g	$⊢ ((K \in HL \land W \in H) \land E \in T \land F \in T) \to E \circ (F \circ G) = F \circ (E \circ G)$
8	7	coeq2d	$⊢ ((K \in HL \land W \in H) \land E \in T \land F \in T) \to D \circ (E \circ (F \circ G)) = D \circ (F \circ (E \circ G))$
9		coass	$⊢ (D \circ E) \circ (F \circ G) = D \circ (E \circ (F \circ G))$
10		coass	$⊢ (D \circ F) \circ (E \circ G) = D \circ (F \circ (E \circ G))$
11	8 9 10	3eqtr4g	$⊢ ((K \in HL \land W \in H) \land E \in T \land F \in T) \to (D \circ E) \circ (F \circ G) = (D \circ F) \circ (E \circ G)$

Metamath Proof Explorer