tendoidcl

Description: The identity is a trace-preserving endomorphism. (Contributed by NM, 30-Jul-2013)

	Ref	Expression
Hypotheses	tendof.h	$⊢ H = LHyp (K)$
	tendof.t	$⊢ T = LTrn (K) (W)$
	tendof.e	$⊢ E = TEndo (K) (W)$
Assertion	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in E$

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		eqid	$⊢ \leq_{K} = \leq_{K}$
5		eqid	$⊢ trL (K) (W) = trL (K) (W)$
6		id	$⊢ (K \in HL \land W \in H) \to (K \in HL \land W \in H)$
7		f1oi	$⊢ ({I ↾}_{T}) : T \underset{1-1 onto}{⟶} T$
8		f1of	$⊢ ({I ↾}_{T}) : T \underset{1-1 onto}{⟶} T \to ({I ↾}_{T}) : T ⟶ T$
9	7 8	mp1i	$⊢ (K \in HL \land W \in H) \to ({I ↾}_{T}) : T ⟶ T$
10	1 2	ltrnco	$⊢ ((K \in HL \land W \in H) \land f \in T \land g \in T) \to f \circ g \in T$
11		fvresi	$⊢ f \circ g \in T \to ({I ↾}_{T}) (f \circ g) = f \circ g$
12	10 11	syl	$⊢ ((K \in HL \land W \in H) \land f \in T \land g \in T) \to ({I ↾}_{T}) (f \circ g) = f \circ g$
13		fvresi	$⊢ f \in T \to ({I ↾}_{T}) (f) = f$
14	13	3ad2ant2	$⊢ ((K \in HL \land W \in H) \land f \in T \land g \in T) \to ({I ↾}_{T}) (f) = f$
15		fvresi	$⊢ g \in T \to ({I ↾}_{T}) (g) = g$
16	15	3ad2ant3	$⊢ ((K \in HL \land W \in H) \land f \in T \land g \in T) \to ({I ↾}_{T}) (g) = g$
17	14 16	coeq12d	$⊢ ((K \in HL \land W \in H) \land f \in T \land g \in T) \to ({I ↾}_{T}) (f) \circ ({I ↾}_{T}) (g) = f \circ g$
18	12 17	eqtr4d	$⊢ ((K \in HL \land W \in H) \land f \in T \land g \in T) \to ({I ↾}_{T}) (f \circ g) = ({I ↾}_{T}) (f) \circ ({I ↾}_{T}) (g)$
19	13	adantl	$⊢ ((K \in HL \land W \in H) \land f \in T) \to ({I ↾}_{T}) (f) = f$
20	19	fveq2d	$⊢ ((K \in HL \land W \in H) \land f \in T) \to trL (K) (W) (({I ↾}_{T}) (f)) = trL (K) (W) (f)$
21		hllat	$⊢ K \in HL \to K \in Lat$
22	21	ad2antrr	$⊢ ((K \in HL \land W \in H) \land f \in T) \to K \in Lat$
23		eqid	$⊢ {Base}_{K} = {Base}_{K}$
24	23 1 2 5	trlcl	$⊢ ((K \in HL \land W \in H) \land f \in T) \to trL (K) (W) (f) \in {Base}_{K}$
25	23 4	latref	$⊢ (K \in Lat \land trL (K) (W) (f) \in {Base}_{K}) \to trL (K) (W) (f) \leq_{K} trL (K) (W) (f)$
26	22 24 25	syl2anc	$⊢ ((K \in HL \land W \in H) \land f \in T) \to trL (K) (W) (f) \leq_{K} trL (K) (W) (f)$
27	20 26	eqbrtrd	$⊢ ((K \in HL \land W \in H) \land f \in T) \to trL (K) (W) (({I ↾}_{T}) (f)) \leq_{K} trL (K) (W) (f)$
28	4 1 2 5 3 6 9 18 27	istendod	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in E$

Metamath Proof Explorer

Theorem tendoidcl

Proof