tendoid

Description: The identity value of a trace-preserving endomorphism. (Contributed by NM, 21-Jun-2013)

	Ref	Expression
Hypotheses	tendoid.b	$⊢ B = {Base}_{K}$
	tendoid.h	$⊢ H = LHyp (K)$
	tendoid.e	$⊢ E = TEndo (K) (W)$
Assertion	tendoid	$⊢ ((K \in HL \land W \in H) \land S \in E) \to S ({I ↾}_{B}) = {I ↾}_{B}$

Proof

Step	Hyp	Ref	Expression
1		tendoid.b	$⊢ B = {Base}_{K}$
2		tendoid.h	$⊢ H = LHyp (K)$
3		tendoid.e	$⊢ E = TEndo (K) (W)$
4		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
5	1 2 4	idltrn	$⊢ (K \in HL \land W \in H) \to {I ↾}_{B} \in LTrn (K) (W)$
6	5	adantr	$⊢ ((K \in HL \land W \in H) \land S \in E) \to {I ↾}_{B} \in LTrn (K) (W)$
7		eqid	$⊢ \leq_{K} = \leq_{K}$
8		eqid	$⊢ trL (K) (W) = trL (K) (W)$
9	7 2 4 8 3	tendotp	$⊢ ((K \in HL \land W \in H) \land S \in E \land {I ↾}_{B} \in LTrn (K) (W)) \to trL (K) (W) (S ({I ↾}_{B})) \leq_{K} trL (K) (W) ({I ↾}_{B})$
10	6 9	mpd3an3	$⊢ ((K \in HL \land W \in H) \land S \in E) \to trL (K) (W) (S ({I ↾}_{B})) \leq_{K} trL (K) (W) ({I ↾}_{B})$
11		eqid	$⊢ 0. (K) = 0. (K)$
12	1 11 2 8	trlid0	$⊢ (K \in HL \land W \in H) \to trL (K) (W) ({I ↾}_{B}) = 0. (K)$
13	12	adantr	$⊢ ((K \in HL \land W \in H) \land S \in E) \to trL (K) (W) ({I ↾}_{B}) = 0. (K)$
14	10 13	breqtrd	$⊢ ((K \in HL \land W \in H) \land S \in E) \to trL (K) (W) (S ({I ↾}_{B})) \leq_{K} 0. (K)$
15		hlop	$⊢ K \in HL \to K \in OP$
16	15	ad2antrr	$⊢ ((K \in HL \land W \in H) \land S \in E) \to K \in OP$
17	2 4 3	tendocl	$⊢ ((K \in HL \land W \in H) \land S \in E \land {I ↾}_{B} \in LTrn (K) (W)) \to S ({I ↾}_{B}) \in LTrn (K) (W)$
18	6 17	mpd3an3	$⊢ ((K \in HL \land W \in H) \land S \in E) \to S ({I ↾}_{B}) \in LTrn (K) (W)$
19	1 2 4 8	trlcl	$⊢ ((K \in HL \land W \in H) \land S ({I ↾}_{B}) \in LTrn (K) (W)) \to trL (K) (W) (S ({I ↾}_{B})) \in B$
20	18 19	syldan	$⊢ ((K \in HL \land W \in H) \land S \in E) \to trL (K) (W) (S ({I ↾}_{B})) \in B$
21	1 7 11	ople0	$⊢ (K \in OP \land trL (K) (W) (S ({I ↾}_{B})) \in B) \to (trL (K) (W) (S ({I ↾}_{B})) \leq_{K} 0. (K) \leftrightarrow trL (K) (W) (S ({I ↾}_{B})) = 0. (K))$
22	16 20 21	syl2anc	$⊢ ((K \in HL \land W \in H) \land S \in E) \to (trL (K) (W) (S ({I ↾}_{B})) \leq_{K} 0. (K) \leftrightarrow trL (K) (W) (S ({I ↾}_{B})) = 0. (K))$
23	14 22	mpbid	$⊢ ((K \in HL \land W \in H) \land S \in E) \to trL (K) (W) (S ({I ↾}_{B})) = 0. (K)$
24	1 11 2 4 8	trlid0b	$⊢ ((K \in HL \land W \in H) \land S ({I ↾}_{B}) \in LTrn (K) (W)) \to (S ({I ↾}_{B}) = {I ↾}_{B} \leftrightarrow trL (K) (W) (S ({I ↾}_{B})) = 0. (K))$
25	18 24	syldan	$⊢ ((K \in HL \land W \in H) \land S \in E) \to (S ({I ↾}_{B}) = {I ↾}_{B} \leftrightarrow trL (K) (W) (S ({I ↾}_{B})) = 0. (K))$
26	23 25	mpbird	$⊢ ((K \in HL \land W \in H) \land S \in E) \to S ({I ↾}_{B}) = {I ↾}_{B}$

Metamath Proof Explorer

Theorem tendoid

Proof