tendoco2

Description: Distribution of compositions in preparation for endomorphism sum definition. (Contributed by NM, 10-Jun-2013)

	Ref	Expression
Hypotheses	tendof.h	$⊢ H = LHyp (K)$
	tendof.t	$⊢ T = LTrn (K) (W)$
	tendof.e	$⊢ E = TEndo (K) (W)$
Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		tendof.h	$⊢ H = LHyp (K)$
2		tendof.t	$⊢ T = LTrn (K) (W)$
3		tendof.e	$⊢ E = TEndo (K) (W)$
4		simp1l	$⊢ ((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$
5		simp1r	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (F \in T \land G \in T)) \to W \in H$
6		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$
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 3	tendovalco	$⊢ ((K \in HL \land W \in H \land U \in E) \land (F \in T \land G \in T)) \to U (F \circ G) = U (F) \circ U (G)$
10	4 5 6 7 8 9	syl32anc	$⊢ ((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) = U (F) \circ U (G)$
11		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$
12	1 2 3	tendovalco	$⊢ ((K \in HL \land W \in H \land V \in E) \land (F \in T \land G \in T)) \to V (F \circ G) = V (F) \circ V (G)$
13	4 5 11 7 8 12	syl32anc	$⊢ ((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 (F \circ G) = V (F) \circ V (G)$
14	10 13	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 (F \circ G) \circ V (F \circ G) = (U (F) \circ U (G)) \circ (V (F) \circ V (G))$
15		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)$
16	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land G \in T) \to U (G) \in T$
17	15 6 8 16	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 (G) \in T$
18	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land V \in E \land F \in T) \to V (F) \in T$
19	15 11 7 18	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 V (F) \in T$
20	1 2	ltrnco4	$⊢ ((K \in HL \land W \in H) \land U (G) \in T \land V (F) \in T) \to (U (F) \circ U (G)) \circ (V (F) \circ V (G)) = (U (F) \circ V (F)) \circ (U (G) \circ V (G))$
21	15 17 19 20	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 (F) \circ U (G)) \circ (V (F) \circ V (G)) = (U (F) \circ V (F)) \circ (U (G) \circ V (G))$
22	14 21	eqtrd	$⊢ ((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))$

Metamath Proof Explorer

Theorem tendoco2

Proof