tendospass

Description: Associative 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	tendospass	$⊢ ((K \in X \land W \in H) \land (U \in E \land V \in E \land F \in T)) \to (U \circ V) (F) = U (V (F))$

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	1 2 3	tendof	$⊢ ((K \in X \land W \in H) \land V \in E) \to V : T ⟶ T$
5	4	3ad2antr2	$⊢ ((K \in X \land W \in H) \land (U \in E \land V \in E \land F \in T)) \to V : T ⟶ T$
6		simpr3	$⊢ ((K \in X \land W \in H) \land (U \in E \land V \in E \land F \in T)) \to F \in T$
7		fvco3	$⊢ (V : T ⟶ T \land F \in T) \to (U \circ V) (F) = U (V (F))$
8	5 6 7	syl2anc	$⊢ ((K \in X \land W \in H) \land (U \in E \land V \in E \land F \in T)) \to (U \circ V) (F) = U (V (F))$

Metamath Proof Explorer