Theorem tendospdi2

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

	Ref	Expression
Hypotheses	tendospd.t	|- T = ( ( LTrn ` K ) ` W )
	tendosp.p	|- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
Assertion	tendospdi2	|- ( ( U e. E /\ V e. E /\ F e. T ) -> ( ( U P V ) ` F ) = ( ( U ` F ) o. ( V ` F ) ) )

Proof

Step	Hyp	Ref	Expression
1		tendospd.t	|- T = ( ( LTrn ` K ) ` W )
2		tendosp.p	|- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
3	2 1	tendopl2	|- ( ( U e. E /\ V e. E /\ F e. T ) -> ( ( U P V ) ` F ) = ( ( U ` F ) o. ( V ` F ) ) )