# Metamath Proof Explorer

## Theorem tendocl

Description: Closure of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-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 tendocl ${⊢}\left(\left({K}\in {V}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {F}\in {T}\right)\to {S}\left({F}\right)\in {T}$

### 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 {V}\wedge {W}\in {H}\right)\wedge {S}\in {E}\right)\to {S}:{T}⟶{T}$
5 4 3adant3 ${⊢}\left(\left({K}\in {V}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {F}\in {T}\right)\to {S}:{T}⟶{T}$
6 simp3 ${⊢}\left(\left({K}\in {V}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {F}\in {T}\right)\to {F}\in {T}$
7 5 6 ffvelrnd ${⊢}\left(\left({K}\in {V}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {F}\in {T}\right)\to {S}\left({F}\right)\in {T}$