# Metamath Proof Explorer

## Theorem tendoidcl

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

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

### Proof

Step Hyp Ref Expression
1 tendof.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 tendof.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
3 tendof.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
4 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
5 eqid ${⊢}\mathrm{trL}\left({K}\right)\left({W}\right)=\mathrm{trL}\left({K}\right)\left({W}\right)$
6 id ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 f1oi ${⊢}\left({\mathrm{I}↾}_{{T}}\right):{T}\underset{1-1 onto}{⟶}{T}$
8 f1of ${⊢}\left({\mathrm{I}↾}_{{T}}\right):{T}\underset{1-1 onto}{⟶}{T}\to \left({\mathrm{I}↾}_{{T}}\right):{T}⟶{T}$
9 7 8 mp1i ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({\mathrm{I}↾}_{{T}}\right):{T}⟶{T}$
10 1 2 ltrnco ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\wedge {g}\in {T}\right)\to {f}\circ {g}\in {T}$
11 fvresi ${⊢}{f}\circ {g}\in {T}\to \left({\mathrm{I}↾}_{{T}}\right)\left({f}\circ {g}\right)={f}\circ {g}$
12 10 11 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\wedge {g}\in {T}\right)\to \left({\mathrm{I}↾}_{{T}}\right)\left({f}\circ {g}\right)={f}\circ {g}$
13 fvresi ${⊢}{f}\in {T}\to \left({\mathrm{I}↾}_{{T}}\right)\left({f}\right)={f}$
14 13 3ad2ant2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\wedge {g}\in {T}\right)\to \left({\mathrm{I}↾}_{{T}}\right)\left({f}\right)={f}$
15 fvresi ${⊢}{g}\in {T}\to \left({\mathrm{I}↾}_{{T}}\right)\left({g}\right)={g}$
16 15 3ad2ant3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\wedge {g}\in {T}\right)\to \left({\mathrm{I}↾}_{{T}}\right)\left({g}\right)={g}$
17 14 16 coeq12d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\wedge {g}\in {T}\right)\to \left({\mathrm{I}↾}_{{T}}\right)\left({f}\right)\circ \left({\mathrm{I}↾}_{{T}}\right)\left({g}\right)={f}\circ {g}$
18 12 17 eqtr4d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\wedge {g}\in {T}\right)\to \left({\mathrm{I}↾}_{{T}}\right)\left({f}\circ {g}\right)=\left({\mathrm{I}↾}_{{T}}\right)\left({f}\right)\circ \left({\mathrm{I}↾}_{{T}}\right)\left({g}\right)$
19 13 adantl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to \left({\mathrm{I}↾}_{{T}}\right)\left({f}\right)={f}$
20 19 fveq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left(\left({\mathrm{I}↾}_{{T}}\right)\left({f}\right)\right)=\mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)$
21 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
22 21 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to {K}\in \mathrm{Lat}$
23 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
24 23 1 2 5 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)\in {\mathrm{Base}}_{{K}}$
25 23 4 latref ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right){\le }_{{K}}\mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)$
26 22 24 25 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right){\le }_{{K}}\mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)$
27 20 26 eqbrtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left(\left({\mathrm{I}↾}_{{T}}\right)\left({f}\right)\right){\le }_{{K}}\mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)$
28 4 1 2 5 3 6 9 18 27 istendod ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{T}}\in {E}$