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. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )
Assertion dvhopspN 
|- ( ( R e. E /\ ( F e. T /\ U e. E ) ) -> ( R S <. F , U >. ) = <. ( R ` F ) , ( R o. U ) >. )

Proof

Step Hyp Ref Expression
1 dvhopsp.s 
 |-  S = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )
2 opelxpi 
 |-  ( ( F e. T /\ U e. E ) -> <. F , U >. e. ( T X. E ) )
3 1 dvhvscaval 
 |-  ( ( R e. E /\ <. F , U >. e. ( T X. E ) ) -> ( R S <. F , U >. ) = <. ( R ` ( 1st ` <. F , U >. ) ) , ( R o. ( 2nd ` <. F , U >. ) ) >. )
4 2 3 sylan2 
 |-  ( ( R e. E /\ ( F e. T /\ U e. E ) ) -> ( R S <. F , U >. ) = <. ( R ` ( 1st ` <. F , U >. ) ) , ( R o. ( 2nd ` <. F , U >. ) ) >. )
5 op1stg 
 |-  ( ( F e. T /\ U e. E ) -> ( 1st ` <. F , U >. ) = F )
6 5 fveq2d 
 |-  ( ( F e. T /\ U e. E ) -> ( R ` ( 1st ` <. F , U >. ) ) = ( R ` F ) )
7 op2ndg 
 |-  ( ( F e. T /\ U e. E ) -> ( 2nd ` <. F , U >. ) = U )
8 7 coeq2d 
 |-  ( ( F e. T /\ U e. E ) -> ( R o. ( 2nd ` <. F , U >. ) ) = ( R o. U ) )
9 6 8 opeq12d 
 |-  ( ( F e. T /\ U e. E ) -> <. ( R ` ( 1st ` <. F , U >. ) ) , ( R o. ( 2nd ` <. F , U >. ) ) >. = <. ( R ` F ) , ( R o. U ) >. )
10 9 adantl 
 |-  ( ( R e. E /\ ( F e. T /\ U e. E ) ) -> <. ( R ` ( 1st ` <. F , U >. ) ) , ( R o. ( 2nd ` <. F , U >. ) ) >. = <. ( R ` F ) , ( R o. U ) >. )
11 4 10 eqtrd 
 |-  ( ( R e. E /\ ( F e. T /\ U e. E ) ) -> ( R S <. F , U >. ) = <. ( R ` F ) , ( R o. U ) >. )