Metamath Proof Explorer

Theorem tendo0cl

Description: The additive identity is a trace-preserving endormorphism. (Contributed by NM, 12-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 ∈ T ⟼ I ↾ B
Assertion tendo0cl ⊢ K ∈ HL ∧ W ∈ H → O ∈ E

Proof

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 ∈ T ⟼ I ↾ B
6 eqid ⊢ ≤ K = ≤ K
7 eqid ⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W
8 id ⊢ K ∈ HL ∧ W ∈ H → K ∈ HL ∧ W ∈ H
9 1 2 3 idltrn ⊢ K ∈ HL ∧ W ∈ H → I ↾ B ∈ T
10 9 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T → I ↾ B ∈ T
11 5 tendo0cbv ⊢ O = g ∈ T ⟼ I ↾ B
12 10 11 fmptd ⊢ K ∈ HL ∧ W ∈ H → O : T ⟶ T
13 1 2 3 4 5 tendo0co2 ⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T ∧ h ∈ T → O ⁡ g ∘ h = O ⁡ g ∘ O ⁡ h
14 1 2 3 4 5 6 7 tendo0tp ⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T → trL ⁡ K ⁡ W ⁡ O ⁡ g ≤ K trL ⁡ K ⁡ W ⁡ g
15 6 2 3 7 4 8 12 13 14 istendod ⊢ K ∈ HL ∧ W ∈ H → O ∈ E