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 ) ) )