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 \in V \land W \in H) \land (U \in E \land F \in T \land G \in T)) \to U (F \circ G) = U (F) \circ U (G)$

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 \in V \land W \in H) \land (U \in E \land F \in T \land G \in T)) \to K \in V$
5		simplr	$⊢ ((K \in V \land W \in H) \land (U \in E \land F \in T \land G \in T)) \to W \in H$
6		simpr1	$⊢ ((K \in V \land W \in H) \land (U \in E \land F \in T \land G \in T)) \to U \in E$
7		simpr2	$⊢ ((K \in V \land W \in H) \land (U \in E \land F \in T \land G \in T)) \to F \in T$
8		simpr3	$⊢ ((K \in V \land W \in H) \land (U \in E \land F \in T \land G \in T)) \to G \in T$
9	1 2 3	tendovalco	$⊢ ((K \in V \land W \in H \land U \in E) \land (F \in T \land G \in T)) \to U (F \circ G) = U (F) \circ U (G)$
10	4 5 6 7 8 9	syl32anc	$⊢ ((K \in V \land W \in H) \land (U \in E \land F \in T \land G \in T)) \to U (F \circ G) = U (F) \circ U (G)$

Metamath Proof Explorer