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 = ( LHyp ` K )`
tendof.t
`|- T = ( ( LTrn ` K ) ` W )`
tendof.e
`|- E = ( ( TEndo ` K ) ` W )`
Assertion tendocoval
`|- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( ( U o. V ) ` F ) = ( U ` ( V ` F ) ) )`

Proof

Step Hyp Ref Expression
1 tendof.h
` |-  H = ( LHyp ` K )`
2 tendof.t
` |-  T = ( ( LTrn ` K ) ` W )`
3 tendof.e
` |-  E = ( ( TEndo ` K ) ` W )`
4 simp1
` |-  ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( K e. X /\ W e. H ) )`
5 simp2r
` |-  ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> V e. E )`
6 1 2 3 tendof
` |-  ( ( ( K e. X /\ W e. H ) /\ V e. E ) -> V : T --> T )`
7 4 5 6 syl2anc
` |-  ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> V : T --> T )`
8 simp3
` |-  ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> F e. T )`
9 fvco3
` |-  ( ( V : T --> T /\ F e. T ) -> ( ( U o. V ) ` F ) = ( U ` ( V ` F ) ) )`
10 7 8 9 syl2anc
` |-  ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( ( U o. V ) ` F ) = ( U ` ( V ` F ) ) )`