tendoplcl

Description: Endomorphism sum is a trace-preserving endomorphism. (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	tendoplcl	$⊢ ((K \in HL \land W \in H) \land U \in E \land V \in E) \to U P V \in E$

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		eqid	$⊢ \leq_{K} = \leq_{K}$
6		eqid	$⊢ trL (K) (W) = trL (K) (W)$
7		simp1	$⊢ ((K \in HL \land W \in H) \land U \in E \land V \in E) \to (K \in HL \land W \in H)$
8		simpl1	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land g \in T) \to (K \in HL \land W \in H)$
9		simpl2	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land g \in T) \to U \in E$
10		simpr	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land g \in T) \to g \in T$
11	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land g \in T) \to U (g) \in T$
12	8 9 10 11	syl3anc	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land g \in T) \to U (g) \in T$
13		simpl3	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land g \in T) \to V \in E$
14	1 2 3	tendocl	$⊢ ((K \in HL \land W \in H) \land V \in E \land g \in T) \to V (g) \in T$
15	8 13 10 14	syl3anc	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land g \in T) \to V (g) \in T$
16	1 2	ltrnco	$⊢ ((K \in HL \land W \in H) \land U (g) \in T \land V (g) \in T) \to U (g) \circ V (g) \in T$
17	8 12 15 16	syl3anc	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land g \in T) \to U (g) \circ V (g) \in T$
18	17	fmpttd	$⊢ ((K \in HL \land W \in H) \land U \in E \land V \in E) \to (g \in T ⟼ U (g) \circ V (g)) : T ⟶ T$
19	4 2	tendopl	$⊢ (U \in E \land V \in E) \to U P V = (g \in T ⟼ U (g) \circ V (g))$
20	19	3adant1	$⊢ ((K \in HL \land W \in H) \land U \in E \land V \in E) \to U P V = (g \in T ⟼ U (g) \circ V (g))$
21	20	feq1d	$⊢ ((K \in HL \land W \in H) \land U \in E \land V \in E) \to ((U P V) : T ⟶ T \leftrightarrow (g \in T ⟼ U (g) \circ V (g)) : T ⟶ T)$
22	18 21	mpbird	$⊢ ((K \in HL \land W \in H) \land U \in E \land V \in E) \to (U P V) : T ⟶ T$
23		simp11	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land h \in T \land i \in T) \to (K \in HL \land W \in H)$
24		simp12	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land h \in T \land i \in T) \to U \in E$
25		simp13	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land h \in T \land i \in T) \to V \in E$
26		3simpc	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land h \in T \land i \in T) \to (h \in T \land i \in T)$
27	1 2 3 4	tendoplco2	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (h \in T \land i \in T)) \to (U P V) (h \circ i) = (U P V) (h) \circ (U P V) (i)$
28	23 24 25 26 27	syl121anc	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land h \in T \land i \in T) \to (U P V) (h \circ i) = (U P V) (h) \circ (U P V) (i)$
29		simpl1	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land h \in T) \to (K \in HL \land W \in H)$
30		simpl2	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land h \in T) \to U \in E$
31		simpl3	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land h \in T) \to V \in E$
32		simpr	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land h \in T) \to h \in T$
33	1 2 3 4 5 6	tendopltp	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land h \in T) \to trL (K) (W) ((U P V) (h)) \leq_{K} trL (K) (W) (h)$
34	29 30 31 32 33	syl121anc	$⊢ (((K \in HL \land W \in H) \land U \in E \land V \in E) \land h \in T) \to trL (K) (W) ((U P V) (h)) \leq_{K} trL (K) (W) (h)$
35	5 1 2 6 3 7 22 28 34	istendod	$⊢ ((K \in HL \land W \in H) \land U \in E \land V \in E) \to U P V \in E$

Metamath Proof Explorer

Theorem tendoplcl

Proof