dvhvsca

Description: Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013)

	Ref	Expression
Hypotheses	dvhfvsca.h	$⊢ H = LHyp (K)$
	dvhfvsca.t	$⊢ T = LTrn (K) (W)$
	dvhfvsca.e	$⊢ E = TEndo (K) (W)$
	dvhfvsca.u	$⊢ U = DVecH (K) (W)$
	dvhfvsca.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
Assertion	dvhvsca	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in (T \times E))) \to R \underset{˙}{\cdot} F = ⟨R (1^{st} (F)), R \circ 2^{nd} (F)⟩$

Step	Hyp	Ref	Expression
1		dvhfvsca.h	$⊢ H = LHyp (K)$
2		dvhfvsca.t	$⊢ T = LTrn (K) (W)$
3		dvhfvsca.e	$⊢ E = TEndo (K) (W)$
4		dvhfvsca.u	$⊢ U = DVecH (K) (W)$
5		dvhfvsca.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
6	1 2 3 4 5	dvhfvsca	$⊢ (K \in V \land W \in H) \to \underset{˙}{\cdot} = (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)$
7	6	oveqd	$⊢ (K \in V \land W \in H) \to R \underset{˙}{\cdot} F = R (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩) F$
8		eqid	$⊢ (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩) = (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)$
9	8	dvhvscaval	$⊢ (R \in E \land F \in (T \times E)) \to R (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩) F = ⟨R (1^{st} (F)), R \circ 2^{nd} (F)⟩$
10	7 9	sylan9eq	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in (T \times E))) \to R \underset{˙}{\cdot} F = ⟨R (1^{st} (F)), R \circ 2^{nd} (F)⟩$

Metamath Proof Explorer