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 ) ) >. ) |