Theorem tendospdi1

Description: Forward distributive 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	tendospdi1	|- ( ( ( K e. V /\ W e. H ) /\ ( U e. E /\ F e. T /\ G e. T ) ) -> ( U ` ( F o. G ) ) = ( ( U ` F ) o. ( U ` G ) ) )

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		simpll	|- ( ( ( K e. V /\ W e. H ) /\ ( U e. E /\ F e. T /\ G e. T ) ) -> K e. V )
5		simplr	|- ( ( ( K e. V /\ W e. H ) /\ ( U e. E /\ F e. T /\ G e. T ) ) -> W e. H )
6		simpr1	|- ( ( ( K e. V /\ W e. H ) /\ ( U e. E /\ F e. T /\ G e. T ) ) -> U e. E )
7		simpr2	|- ( ( ( K e. V /\ W e. H ) /\ ( U e. E /\ F e. T /\ G e. T ) ) -> F e. T )
8		simpr3	|- ( ( ( K e. V /\ W e. H ) /\ ( U e. E /\ F e. T /\ G e. T ) ) -> G e. T )
9	1 2 3	tendovalco	|- ( ( ( K e. V /\ W e. H /\ U e. E ) /\ ( F e. T /\ G e. T ) ) -> ( U ` ( F o. G ) ) = ( ( U ` F ) o. ( U ` G ) ) )
10	4 5 6 7 8 9	syl32anc	|- ( ( ( K e. V /\ W e. H ) /\ ( U e. E /\ F e. T /\ G e. T ) ) -> ( U ` ( F o. G ) ) = ( ( U ` F ) o. ( U ` G ) ) )