# Metamath Proof Explorer

## Theorem tendocoval

Description: Value of composition of endomorphisms in 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 tendocoval ${⊢}\left(\left({K}\in {X}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\wedge {F}\in {T}\right)\to \left({U}\circ {V}\right)\left({F}\right)={U}\left({V}\left({F}\right)\right)$

### 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 simp1 ${⊢}\left(\left({K}\in {X}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\wedge {F}\in {T}\right)\to \left({K}\in {X}\wedge {W}\in {H}\right)$
5 simp2r ${⊢}\left(\left({K}\in {X}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\wedge {F}\in {T}\right)\to {V}\in {E}$
6 1 2 3 tendof ${⊢}\left(\left({K}\in {X}\wedge {W}\in {H}\right)\wedge {V}\in {E}\right)\to {V}:{T}⟶{T}$
7 4 5 6 syl2anc ${⊢}\left(\left({K}\in {X}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\wedge {F}\in {T}\right)\to {V}:{T}⟶{T}$
8 simp3 ${⊢}\left(\left({K}\in {X}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\wedge {F}\in {T}\right)\to {F}\in {T}$
9 fvco3 ${⊢}\left({V}:{T}⟶{T}\wedge {F}\in {T}\right)\to \left({U}\circ {V}\right)\left({F}\right)={U}\left({V}\left({F}\right)\right)$
10 7 8 9 syl2anc ${⊢}\left(\left({K}\in {X}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\wedge {F}\in {T}\right)\to \left({U}\circ {V}\right)\left({F}\right)={U}\left({V}\left({F}\right)\right)$