Metamath Proof Explorer

Theorem dvhvscaval

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

Ref Expression
Hypothesis dvhvscaval.s 
|- .x. = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )
Assertion dvhvscaval 
|- ( ( U e. E /\ F e. ( T X. E ) ) -> ( U .x. F ) = <. ( U ` ( 1st ` F ) ) , ( U o. ( 2nd ` F ) ) >. )

Proof

Step Hyp Ref Expression
1 dvhvscaval.s 
 |-  .x. = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )
2 fveq1 
 |-  ( t = U -> ( t ` ( 1st ` g ) ) = ( U ` ( 1st ` g ) ) )
3 coeq1 
 |-  ( t = U -> ( t o. ( 2nd ` g ) ) = ( U o. ( 2nd ` g ) ) )
4 2 3 opeq12d 
 |-  ( t = U -> <. ( t ` ( 1st ` g ) ) , ( t o. ( 2nd ` g ) ) >. = <. ( U ` ( 1st ` g ) ) , ( U o. ( 2nd ` g ) ) >. )
5 2fveq3 
 |-  ( g = F -> ( U ` ( 1st ` g ) ) = ( U ` ( 1st ` F ) ) )
6 fveq2 
 |-  ( g = F -> ( 2nd ` g ) = ( 2nd ` F ) )
7 6 coeq2d 
 |-  ( g = F -> ( U o. ( 2nd ` g ) ) = ( U o. ( 2nd ` F ) ) )
8 5 7 opeq12d 
 |-  ( g = F -> <. ( U ` ( 1st ` g ) ) , ( U o. ( 2nd ` g ) ) >. = <. ( U ` ( 1st ` F ) ) , ( U o. ( 2nd ` F ) ) >. )
9 1 dvhvscacbv 
 |-  .x. = ( t e. E , g e. ( T X. E ) |-> <. ( t ` ( 1st ` g ) ) , ( t o. ( 2nd ` g ) ) >. )
10 opex 
 |-  <. ( U ` ( 1st ` F ) ) , ( U o. ( 2nd ` F ) ) >. e. _V
11 4 8 9 10 ovmpo 
 |-  ( ( U e. E /\ F e. ( T X. E ) ) -> ( U .x. F ) = <. ( U ` ( 1st ` F ) ) , ( U o. ( 2nd ` F ) ) >. )