tendo0cl

Description: The additive identity is a trace-preserving endormorphism. (Contributed by NM, 12-Jun-2013)

Step	Hyp	Ref	Expression
1		tendo0.b	$⊢ B = {Base}_{K}$
2		tendo0.h	$⊢ H = LHyp (K)$
3		tendo0.t	$⊢ T = LTrn (K) (W)$
4		tendo0.e	$⊢ E = TEndo (K) (W)$
5		tendo0.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
6		eqid	$⊢ \leq_{K} = \leq_{K}$
7		eqid	$⊢ trL (K) (W) = trL (K) (W)$
8		id	$⊢ (K \in HL \land W \in H) \to (K \in HL \land W \in H)$
9	1 2 3	idltrn	$⊢ (K \in HL \land W \in H) \to {I ↾}_{B} \in T$
10	9	adantr	$⊢ ((K \in HL \land W \in H) \land g \in T) \to {I ↾}_{B} \in T$
11	5	tendo0cbv	$⊢ O = (g \in T ⟼ {I ↾}_{B})$
12	10 11	fmptd	$⊢ (K \in HL \land W \in H) \to O : T ⟶ T$
13	1 2 3 4 5	tendo0co2	$⊢ ((K \in HL \land W \in H) \land g \in T \land h \in T) \to O (g \circ h) = O (g) \circ O (h)$
14	1 2 3 4 5 6 7	tendo0tp	$⊢ ((K \in HL \land W \in H) \land g \in T) \to trL (K) (W) (O (g)) \leq_{K} trL (K) (W) (g)$
15	6 2 3 7 4 8 12 13 14	istendod	$⊢ (K \in HL \land W \in H) \to O \in E$

Metamath Proof Explorer