tendoplco2

Description: Value of result of endomorphism sum operation on a translation composition. (Contributed by NM, 10-Jun-2013)

	Ref	Expression
Hypotheses	tendopl.h	$⊢ H = LHyp (K)$
	tendopl.t	$⊢ T = LTrn (K) (W)$
	tendopl.e	$⊢ E = TEndo (K) (W)$
	tendopl.p	$⊢ P = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
Assertion	tendoplco2	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to (U P V) (F \circ G) = (U P V) (F) \circ (U P V) (G)$

Proof

Step	Hyp	Ref	Expression
1		tendopl.h	$⊢ H = LHyp (K)$
2		tendopl.t	$⊢ T = LTrn (K) (W)$
3		tendopl.e	$⊢ E = TEndo (K) (W)$
4		tendopl.p	$⊢ P = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
5	1 2 3	tendoco2	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to U (F \circ G) \circ V (F \circ G) = (U (F) \circ V (F)) \circ (U (G) \circ V (G))$
6		simp1	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to (K \in HL \land W \in H)$
7		simp3l	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to F \in T$
8		simp3r	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to G \in T$
9	1 2	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G \in T$
10	6 7 8 9	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to F \circ G \in T$
11		simp2l	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \circ G \in T) \to U \in E$
12		simp2r	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \circ G \in T) \to V \in E$
13		simp3	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \circ G \in T) \to F \circ G \in T$
14	4 2	tendopl2	$⊢ (U \in E \land V \in E \land F \circ G \in T) \to (U P V) (F \circ G) = U (F \circ G) \circ V (F \circ G)$
15	11 12 13 14	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land F \circ G \in T) \to (U P V) (F \circ G) = U (F \circ G) \circ V (F \circ G)$
16	10 15	syld3an3	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to (U P V) (F \circ G) = U (F \circ G) \circ V (F \circ G)$
17		simp2l	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to U \in E$
18		simp2r	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to V \in E$
19	4 2	tendopl2	$⊢ (U \in E \land V \in E \land F \in T) \to (U P V) (F) = U (F) \circ V (F)$
20	17 18 7 19	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to (U P V) (F) = U (F) \circ V (F)$
21	4 2	tendopl2	$⊢ (U \in E \land V \in E \land G \in T) \to (U P V) (G) = U (G) \circ V (G)$
22	17 18 8 21	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to (U P V) (G) = U (G) \circ V (G)$
23	20 22	coeq12d	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to (U P V) (F) \circ (U P V) (G) = (U (F) \circ V (F)) \circ (U (G) \circ V (G))$
24	5 16 23	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to (U P V) (F \circ G) = (U P V) (F) \circ (U P V) (G)$

Metamath Proof Explorer

Theorem tendoplco2

Proof