dvhopspN

Description: Scalar product of DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	dvhopsp.s	$⊢ S = (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)$
	Assertion	dvhopspN	$⊢ (R \in E \land (F \in T \land U \in E)) \to R S ⟨F, U⟩ = ⟨R (F), R \circ U⟩$

Step	Hyp	Ref	Expression
1		dvhopsp.s	$⊢ S = (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)$
2		opelxpi	$⊢ (F \in T \land U \in E) \to ⟨F, U⟩ \in (T \times E)$
3	1	dvhvscaval	$⊢ (R \in E \land ⟨F, U⟩ \in (T \times E)) \to R S ⟨F, U⟩ = ⟨R (1^{st} (⟨F, U⟩)), R \circ 2^{nd} (⟨F, U⟩)⟩$
4	2 3	sylan2	$⊢ (R \in E \land (F \in T \land U \in E)) \to R S ⟨F, U⟩ = ⟨R (1^{st} (⟨F, U⟩)), R \circ 2^{nd} (⟨F, U⟩)⟩$
5		op1stg	$⊢ (F \in T \land U \in E) \to 1^{st} (⟨F, U⟩) = F$
6	5	fveq2d	$⊢ (F \in T \land U \in E) \to R (1^{st} (⟨F, U⟩)) = R (F)$
7		op2ndg	$⊢ (F \in T \land U \in E) \to 2^{nd} (⟨F, U⟩) = U$
8	7	coeq2d	$⊢ (F \in T \land U \in E) \to R \circ 2^{nd} (⟨F, U⟩) = R \circ U$
9	6 8	opeq12d	$⊢ (F \in T \land U \in E) \to ⟨R (1^{st} (⟨F, U⟩)), R \circ 2^{nd} (⟨F, U⟩)⟩ = ⟨R (F), R \circ U⟩$
10	9	adantl	$⊢ (R \in E \land (F \in T \land U \in E)) \to ⟨R (1^{st} (⟨F, U⟩)), R \circ 2^{nd} (⟨F, U⟩)⟩ = ⟨R (F), R \circ U⟩$
11	4 10	eqtrd	$⊢ (R \in E \land (F \in T \land U \in E)) \to R S ⟨F, U⟩ = ⟨R (F), R \circ U⟩$

Metamath Proof Explorer