This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
Assertion tendospdi2 ⊢ U ∈ E ∧ V ∈ E ∧ F ∈ T → U P V ⁡ F = U ⁡ F ∘ V ⁡ F

Proof

Step Hyp Ref Expression
1 tendospd.t ⊢ T = LTrn ⁡ K ⁡ W
2 tendosp.p ⊢ P = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
3 2 1 tendopl2 ⊢ U ∈ E ∧ V ∈ E ∧ F ∈ T → U P V ⁡ F = U ⁡ F ∘ V ⁡ F