Theorem tendospass

Description: Associative law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013)

	Ref	Expression
Hypotheses	tendosp.h	|- H = ( LHyp ` K )
	tendosp.t	|- T = ( ( LTrn ` K ) ` W )
	tendosp.e	|- E = ( ( TEndo ` K ) ` W )
Assertion	tendospass	|- ( ( ( 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		tendosp.h	|- H = ( LHyp ` K )
2		tendosp.t	|- T = ( ( LTrn ` K ) ` W )
3		tendosp.e	|- E = ( ( TEndo ` K ) ` W )
4	1 2 3	tendof	|- ( ( ( K e. X /\ W e. H ) /\ V e. E ) -> V : T --> T )
5	4	3ad2antr2	|- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E /\ F e. T ) ) -> V : T --> T )
6		simpr3	|- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E /\ F e. T ) ) -> F e. T )
7		fvco3	|- ( ( V : T --> T /\ F e. T ) -> ( ( U o. V ) ` F ) = ( U ` ( V ` F ) ) )
8	5 6 7	syl2anc	|- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E /\ F e. T ) ) -> ( ( U o. V ) ` F ) = ( U ` ( V ` F ) ) )