tendodi1

Description: Endomorphism composition distributes over sum. (Contributed by NM, 13-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	tendodi1	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to S \circ (U P V) = (S \circ U) P (S \circ V)$

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		simpl	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to (K \in HL \land W \in H)$
6		simpr1	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to S \in E$
7		simpr2	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to U \in E$
8		simpr3	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to V \in E$
9	1 2 3 4	tendoplcl	$⊢ ((K \in HL \land W \in H) \land U \in E \land V \in E) \to U P V \in E$
10	5 7 8 9	syl3anc	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to U P V \in E$
11	1 3	tendococl	$⊢ ((K \in HL \land W \in H) \land S \in E \land U P V \in E) \to S \circ (U P V) \in E$
12	5 6 10 11	syl3anc	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to S \circ (U P V) \in E$
13	1 3	tendococl	$⊢ ((K \in HL \land W \in H) \land S \in E \land U \in E) \to S \circ U \in E$
14	5 6 7 13	syl3anc	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to S \circ U \in E$
15	1 3	tendococl	$⊢ ((K \in HL \land W \in H) \land S \in E \land V \in E) \to S \circ V \in E$
16	5 6 8 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to S \circ V \in E$
17	1 2 3 4	tendoplcl	$⊢ ((K \in HL \land W \in H) \land S \circ U \in E \land S \circ V \in E) \to (S \circ U) P (S \circ V) \in E$
18	5 14 16 17	syl3anc	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to (S \circ U) P (S \circ V) \in E$
19		simplll	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to K \in HL$
20		simpllr	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to W \in H$
21		simplr1	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to S \in E$
22		simpll	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to (K \in HL \land W \in H)$
23		simplr2	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to U \in E$
24		simpr	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to g \in T$
25	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land g \in T) \to U (g) \in T$
26	22 23 24 25	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to U (g) \in T$
27		simplr3	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to V \in E$
28	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land V \in E \land g \in T) \to V (g) \in T$
29	22 27 24 28	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to V (g) \in T$
30	1 2 3	tendovalco	$⊢ ((K \in HL \land W \in H \land S \in E) \land (U (g) \in T \land V (g) \in T)) \to S (U (g) \circ V (g)) = S (U (g)) \circ S (V (g))$
31	19 20 21 26 29 30	syl32anc	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to S (U (g) \circ V (g)) = S (U (g)) \circ S (V (g))$
32	4 2	tendopl2	$⊢ (U \in E \land V \in E \land g \in T) \to (U P V) (g) = U (g) \circ V (g)$
33	23 27 24 32	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to (U P V) (g) = U (g) \circ V (g)$
34	33	fveq2d	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to S ((U P V) (g)) = S (U (g) \circ V (g))$
35	1 2 3	tendocoval	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E) \land g \in T) \to (S \circ U) (g) = S (U (g))$
36	19 20 21 23 24 35	syl221anc	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to (S \circ U) (g) = S (U (g))$
37	1 2 3	tendocoval	$⊢ ((K \in HL \land W \in H) \land (S \in E \land V \in E) \land g \in T) \to (S \circ V) (g) = S (V (g))$
38	19 20 21 27 24 37	syl221anc	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to (S \circ V) (g) = S (V (g))$
39	36 38	coeq12d	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to (S \circ U) (g) \circ (S \circ V) (g) = S (U (g)) \circ S (V (g))$
40	31 34 39	3eqtr4rd	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to (S \circ U) (g) \circ (S \circ V) (g) = S ((U P V) (g))$
41	22 21 23 13	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to S \circ U \in E$
42	22 21 27 15	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to S \circ V \in E$
43	4 2	tendopl2	$⊢ (S \circ U \in E \land S \circ V \in E \land g \in T) \to ((S \circ U) P (S \circ V)) (g) = (S \circ U) (g) \circ (S \circ V) (g)$
44	41 42 24 43	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to ((S \circ U) P (S \circ V)) (g) = (S \circ U) (g) \circ (S \circ V) (g)$
45	22 23 27 9	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to U P V \in E$
46	1 2 3	tendocoval	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U P V \in E) \land g \in T) \to (S \circ (U P V)) (g) = S ((U P V) (g))$
47	22 21 45 24 46	syl121anc	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to (S \circ (U P V)) (g) = S ((U P V) (g))$
48	40 44 47	3eqtr4rd	$⊢ (((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \land g \in T) \to (S \circ (U P V)) (g) = ((S \circ U) P (S \circ V)) (g)$
49	48	ralrimiva	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to \forall g \in T (S \circ (U P V)) (g) = ((S \circ U) P (S \circ V)) (g)$
50	1 2 3	tendoeq1	$⊢ ((K \in HL \land W \in H) \land (S \circ (U P V) \in E \land (S \circ U) P (S \circ V) \in E) \land \forall g \in T (S \circ (U P V)) (g) = ((S \circ U) P (S \circ V)) (g)) \to S \circ (U P V) = (S \circ U) P (S \circ V)$
51	5 12 18 49 50	syl121anc	$⊢ ((K \in HL \land W \in H) \land (S \in E \land U \in E \land V \in E)) \to S \circ (U P V) = (S \circ U) P (S \circ V)$

Metamath Proof Explorer

Theorem tendodi1

Proof