Metamath Proof Explorer


Theorem 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 E , f T × E s 1 st f s 2 nd f
Assertion dvhopspN R E F T U E R S F U = R F R U

Proof

Step Hyp Ref Expression
1 dvhopsp.s S = s E , f T × E s 1 st f s 2 nd f
2 opelxpi F T U E F U T × E
3 1 dvhvscaval R E F U T × E R S F U = R 1 st F U R 2 nd F U
4 2 3 sylan2 R E F T U E R S F U = R 1 st F U R 2 nd F U
5 op1stg F T U E 1 st F U = F
6 5 fveq2d F T U E R 1 st F U = R F
7 op2ndg F T U E 2 nd F U = U
8 7 coeq2d F T U E R 2 nd F U = R U
9 6 8 opeq12d F T U E R 1 st F U R 2 nd F U = R F R U
10 9 adantl R E F T U E R 1 st F U R 2 nd F U = R F R U
11 4 10 eqtrd R E F T U E R S F U = R F R U