This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvhvaddval

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013)

Ref Expression
Hypothesis dvhvaddval.a 
|- .+ = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. )
Assertion dvhvaddval 
|- ( ( F e. ( T X. E ) /\ G e. ( T X. E ) ) -> ( F .+ G ) = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. )

Proof

Step Hyp Ref Expression
1 dvhvaddval.a 
 |-  .+ = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. )
2 fveq2 
 |-  ( h = F -> ( 1st ` h ) = ( 1st ` F ) )
3 2 coeq1d 
 |-  ( h = F -> ( ( 1st ` h ) o. ( 1st ` i ) ) = ( ( 1st ` F ) o. ( 1st ` i ) ) )
4 fveq2 
 |-  ( h = F -> ( 2nd ` h ) = ( 2nd ` F ) )
5 4 oveq1d 
 |-  ( h = F -> ( ( 2nd ` h ) .+^ ( 2nd ` i ) ) = ( ( 2nd ` F ) .+^ ( 2nd ` i ) ) )
6 3 5 opeq12d 
 |-  ( h = F -> <. ( ( 1st ` h ) o. ( 1st ` i ) ) , ( ( 2nd ` h ) .+^ ( 2nd ` i ) ) >. = <. ( ( 1st ` F ) o. ( 1st ` i ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` i ) ) >. )
7 fveq2 
 |-  ( i = G -> ( 1st ` i ) = ( 1st ` G ) )
8 7 coeq2d 
 |-  ( i = G -> ( ( 1st ` F ) o. ( 1st ` i ) ) = ( ( 1st ` F ) o. ( 1st ` G ) ) )
9 fveq2 
 |-  ( i = G -> ( 2nd ` i ) = ( 2nd ` G ) )
10 9 oveq2d 
 |-  ( i = G -> ( ( 2nd ` F ) .+^ ( 2nd ` i ) ) = ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) )
11 8 10 opeq12d 
 |-  ( i = G -> <. ( ( 1st ` F ) o. ( 1st ` i ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` i ) ) >. = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. )
12 1 dvhvaddcbv 
 |-  .+ = ( h e. ( T X. E ) , i e. ( T X. E ) |-> <. ( ( 1st ` h ) o. ( 1st ` i ) ) , ( ( 2nd ` h ) .+^ ( 2nd ` i ) ) >. )
13 opex 
 |-  <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. e. _V
14 6 11 12 13 ovmpo 
 |-  ( ( F e. ( T X. E ) /\ G e. ( T X. E ) ) -> ( F .+ G ) = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. )