# Metamath Proof Explorer

## Theorem tendo1mulr

Description: Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-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 tendo1mulr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\in {E}\right)\to {U}\circ \left({\mathrm{I}↾}_{{T}}\right)={U}$

### 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 1 2 3 tendof ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\in {E}\right)\to {U}:{T}⟶{T}$
5 fcoi1 ${⊢}{U}:{T}⟶{T}\to {U}\circ \left({\mathrm{I}↾}_{{T}}\right)={U}$
6 4 5 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\in {E}\right)\to {U}\circ \left({\mathrm{I}↾}_{{T}}\right)={U}$