tendococl

Description: The composition of two trace-preserving endomorphisms (multiplication in the endormorphism ring) is a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013)

	Ref	Expression
Hypotheses	tendoco.h	$⊢ H = LHyp (K)$
	tendoco.e	$⊢ E = TEndo (K) (W)$
Assertion	tendococl	$⊢ ((K \in HL \land W \in H) \land S \in E \land T \in E) \to S \circ T \in E$

Proof

Step	Hyp	Ref	Expression
1		tendoco.h	$⊢ H = LHyp (K)$
2		tendoco.e	$⊢ E = TEndo (K) (W)$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
5		eqid	$⊢ trL (K) (W) = trL (K) (W)$
6		simp1	$⊢ ((K \in HL \land W \in H) \land S \in E \land T \in E) \to (K \in HL \land W \in H)$
7		simp2	$⊢ ((K \in HL \land W \in H) \land S \in E \land T \in E) \to S \in E$
8	1 4 2	tendof	$⊢ ((K \in HL \land W \in H) \land S \in E) \to S : LTrn (K) (W) ⟶ LTrn (K) (W)$
9	6 7 8	syl2anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land T \in E) \to S : LTrn (K) (W) ⟶ LTrn (K) (W)$
10		simp3	$⊢ ((K \in HL \land W \in H) \land S \in E \land T \in E) \to T \in E$
11	1 4 2	tendof	$⊢ ((K \in HL \land W \in H) \land T \in E) \to T : LTrn (K) (W) ⟶ LTrn (K) (W)$
12	6 10 11	syl2anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land T \in E) \to T : LTrn (K) (W) ⟶ LTrn (K) (W)$
13		fco	$⊢ (S : LTrn (K) (W) ⟶ LTrn (K) (W) \land T : LTrn (K) (W) ⟶ LTrn (K) (W)) \to (S \circ T) : LTrn (K) (W) ⟶ LTrn (K) (W)$
14	9 12 13	syl2anc	$⊢ ((K \in HL \land W \in H) \land S \in E \land T \in E) \to (S \circ T) : LTrn (K) (W) ⟶ LTrn (K) (W)$
15		simp11l	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to K \in HL$
16		simp11r	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to W \in H$
17		simp13	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to T \in E$
18		simp2	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to f \in LTrn (K) (W)$
19		simp3	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to g \in LTrn (K) (W)$
20	1 4 2	tendovalco	$⊢ ((K \in HL \land W \in H \land T \in E) \land (f \in LTrn (K) (W) \land g \in LTrn (K) (W))) \to T (f \circ g) = T (f) \circ T (g)$
21	15 16 17 18 19 20	syl32anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to T (f \circ g) = T (f) \circ T (g)$
22	21	fveq2d	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to S (T (f \circ g)) = S (T (f) \circ T (g))$
23		simp12	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to S \in E$
24		simp11	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to (K \in HL \land W \in H)$
25	1 4 2	tendocl	$⊢ ((K \in HL \land W \in H) \land T \in E \land f \in LTrn (K) (W)) \to T (f) \in LTrn (K) (W)$
26	24 17 18 25	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to T (f) \in LTrn (K) (W)$
27	1 4 2	tendocl	$⊢ ((K \in HL \land W \in H) \land T \in E \land g \in LTrn (K) (W)) \to T (g) \in LTrn (K) (W)$
28	24 17 19 27	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to T (g) \in LTrn (K) (W)$
29	1 4 2	tendovalco	$⊢ ((K \in HL \land W \in H \land S \in E) \land (T (f) \in LTrn (K) (W) \land T (g) \in LTrn (K) (W))) \to S (T (f) \circ T (g)) = S (T (f)) \circ S (T (g))$
30	15 16 23 26 28 29	syl32anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to S (T (f) \circ T (g)) = S (T (f)) \circ S (T (g))$
31	22 30	eqtrd	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to S (T (f \circ g)) = S (T (f)) \circ S (T (g))$
32	1 4	ltrnco	$⊢ ((K \in HL \land W \in H) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to f \circ g \in LTrn (K) (W)$
33	24 18 19 32	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to f \circ g \in LTrn (K) (W)$
34	1 4 2	tendocoval	$⊢ ((K \in HL \land W \in H) \land (S \in E \land T \in E) \land f \circ g \in LTrn (K) (W)) \to (S \circ T) (f \circ g) = S (T (f \circ g))$
35	24 23 17 33 34	syl121anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to (S \circ T) (f \circ g) = S (T (f \circ g))$
36	1 4 2	tendocoval	$⊢ ((K \in HL \land W \in H) \land (S \in E \land T \in E) \land f \in LTrn (K) (W)) \to (S \circ T) (f) = S (T (f))$
37	15 16 23 17 18 36	syl221anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to (S \circ T) (f) = S (T (f))$
38	1 4 2	tendocoval	$⊢ ((K \in HL \land W \in H) \land (S \in E \land T \in E) \land g \in LTrn (K) (W)) \to (S \circ T) (g) = S (T (g))$
39	15 16 23 17 19 38	syl221anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to (S \circ T) (g) = S (T (g))$
40	37 39	coeq12d	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to (S \circ T) (f) \circ (S \circ T) (g) = S (T (f)) \circ S (T (g))$
41	31 35 40	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W) \land g \in LTrn (K) (W)) \to (S \circ T) (f \circ g) = (S \circ T) (f) \circ (S \circ T) (g)$
42		eqid	$⊢ {Base}_{K} = {Base}_{K}$
43		simpl1l	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to K \in HL$
44	43	hllatd	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to K \in Lat$
45		simpl1	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to (K \in HL \land W \in H)$
46		simpl2	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to S \in E$
47		simpl3	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to T \in E$
48		simpr	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to f \in LTrn (K) (W)$
49	45 46 47 48 36	syl121anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to (S \circ T) (f) = S (T (f))$
50	45 47 48 25	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to T (f) \in LTrn (K) (W)$
51	1 4 2	tendocl	$⊢ ((K \in HL \land W \in H) \land S \in E \land T (f) \in LTrn (K) (W)) \to S (T (f)) \in LTrn (K) (W)$
52	45 46 50 51	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to S (T (f)) \in LTrn (K) (W)$
53	49 52	eqeltrd	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to (S \circ T) (f) \in LTrn (K) (W)$
54	42 1 4 5	trlcl	$⊢ ((K \in HL \land W \in H) \land (S \circ T) (f) \in LTrn (K) (W)) \to trL (K) (W) ((S \circ T) (f)) \in {Base}_{K}$
55	45 53 54	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to trL (K) (W) ((S \circ T) (f)) \in {Base}_{K}$
56	42 1 4 5	trlcl	$⊢ ((K \in HL \land W \in H) \land T (f) \in LTrn (K) (W)) \to trL (K) (W) (T (f)) \in {Base}_{K}$
57	45 50 56	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to trL (K) (W) (T (f)) \in {Base}_{K}$
58	42 1 4 5	trlcl	$⊢ ((K \in HL \land W \in H) \land f \in LTrn (K) (W)) \to trL (K) (W) (f) \in {Base}_{K}$
59	45 48 58	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to trL (K) (W) (f) \in {Base}_{K}$
60		simpl1r	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to W \in H$
61	43 60 46 47 48 36	syl221anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to (S \circ T) (f) = S (T (f))$
62	61	fveq2d	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to trL (K) (W) ((S \circ T) (f)) = trL (K) (W) (S (T (f)))$
63	3 1 4 5 2	tendotp	$⊢ ((K \in HL \land W \in H) \land S \in E \land T (f) \in LTrn (K) (W)) \to trL (K) (W) (S (T (f))) \leq_{K} trL (K) (W) (T (f))$
64	45 46 50 63	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to trL (K) (W) (S (T (f))) \leq_{K} trL (K) (W) (T (f))$
65	62 64	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to trL (K) (W) ((S \circ T) (f)) \leq_{K} trL (K) (W) (T (f))$
66	3 1 4 5 2	tendotp	$⊢ ((K \in HL \land W \in H) \land T \in E \land f \in LTrn (K) (W)) \to trL (K) (W) (T (f)) \leq_{K} trL (K) (W) (f)$
67	45 47 48 66	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to trL (K) (W) (T (f)) \leq_{K} trL (K) (W) (f)$
68	42 3 44 55 57 59 65 67	lattrd	$⊢ (((K \in HL \land W \in H) \land S \in E \land T \in E) \land f \in LTrn (K) (W)) \to trL (K) (W) ((S \circ T) (f)) \leq_{K} trL (K) (W) (f)$
69	3 1 4 5 2 6 14 41 68	istendod	$⊢ ((K \in HL \land W \in H) \land S \in E \land T \in E) \to S \circ T \in E$

Metamath Proof Explorer

Theorem tendococl

Proof