Metamath Proof Explorer

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 ∈ V ∧ W ∈ H ∧ U ∈ E ∧ F ∈ T ∧ G ∈ T → U ⁡ F ∘ G = U ⁡ F ∘ 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 ∈ V ∧ W ∈ H ∧ U ∈ E ∧ F ∈ T ∧ G ∈ T → K ∈ V
5 simplr ⊢ K ∈ V ∧ W ∈ H ∧ U ∈ E ∧ F ∈ T ∧ G ∈ T → W ∈ H
6 simpr1 ⊢ K ∈ V ∧ W ∈ H ∧ U ∈ E ∧ F ∈ T ∧ G ∈ T → U ∈ E
7 simpr2 ⊢ K ∈ V ∧ W ∈ H ∧ U ∈ E ∧ F ∈ T ∧ G ∈ T → F ∈ T
8 simpr3 ⊢ K ∈ V ∧ W ∈ H ∧ U ∈ E ∧ F ∈ T ∧ G ∈ T → G ∈ T
9 1 2 3 tendovalco ⊢ K ∈ V ∧ W ∈ H ∧ U ∈ E ∧ F ∈ T ∧ G ∈ T → U ⁡ F ∘ G = U ⁡ F ∘ U ⁡ G
10 4 5 6 7 8 9 syl32anc ⊢ K ∈ V ∧ W ∈ H ∧ U ∈ E ∧ F ∈ T ∧ G ∈ T → U ⁡ F ∘ G = U ⁡ F ∘ U ⁡ G