Theorem tendospdi2

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

	Ref	Expression
Hypotheses	tendospd.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	tendosp.p	⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
Assertion	tendospdi2	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tendospd.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
2		tendosp.p	⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
3	2 1	tendopl2	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )