tendo0tp

Description: Trace-preserving property of endomorphism additive identity. (Contributed by NM, 11-Jun-2013)

	Ref	Expression
Hypotheses	tendo0.b	$⊢ B = {Base}_{K}$
	tendo0.h	$⊢ H = LHyp (K)$
	tendo0.t	$⊢ T = LTrn (K) (W)$
	tendo0.e	$⊢ E = TEndo (K) (W)$
	tendo0.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
	tendo0tp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	tendo0tp.r	$⊢ R = trL (K) (W)$
Assertion	tendo0tp	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (O (F)) \underset{˙}{\leq} R (F)$

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		tendo0tp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
7		tendo0tp.r	$⊢ R = trL (K) (W)$
8	5 1	tendo02	$⊢ F \in T \to O (F) = {I ↾}_{B}$
9	8	adantl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to O (F) = {I ↾}_{B}$
10	9	fveq2d	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (O (F)) = R ({I ↾}_{B})$
11		eqid	$⊢ 0. (K) = 0. (K)$
12	1 11 2 7	trlid0	$⊢ (K \in HL \land W \in H) \to R ({I ↾}_{B}) = 0. (K)$
13	12	adantr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R ({I ↾}_{B}) = 0. (K)$
14	10 13	eqtrd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (O (F)) = 0. (K)$
15		hlop	$⊢ K \in HL \to K \in OP$
16	15	ad2antrr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to K \in OP$
17	1 2 3 7	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in B$
18	1 6 11	op0le	$⊢ (K \in OP \land R (F) \in B) \to 0. (K) \underset{˙}{\leq} R (F)$
19	16 17 18	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T) \to 0. (K) \underset{˙}{\leq} R (F)$
20	14 19	eqbrtrd	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (O (F)) \underset{˙}{\leq} R (F)$

Metamath Proof Explorer