| 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 |
|- ( f = h -> ( 1st ` f ) = ( 1st ` h ) ) |
| 3 |
2
|
coeq1d |
|- ( f = h -> ( ( 1st ` f ) o. ( 1st ` g ) ) = ( ( 1st ` h ) o. ( 1st ` g ) ) ) |
| 4 |
|
fveq2 |
|- ( f = h -> ( 2nd ` f ) = ( 2nd ` h ) ) |
| 5 |
4
|
oveq1d |
|- ( f = h -> ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) = ( ( 2nd ` h ) .+^ ( 2nd ` g ) ) ) |
| 6 |
3 5
|
opeq12d |
|- ( f = h -> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. = <. ( ( 1st ` h ) o. ( 1st ` g ) ) , ( ( 2nd ` h ) .+^ ( 2nd ` g ) ) >. ) |
| 7 |
|
fveq2 |
|- ( g = i -> ( 1st ` g ) = ( 1st ` i ) ) |
| 8 |
7
|
coeq2d |
|- ( g = i -> ( ( 1st ` h ) o. ( 1st ` g ) ) = ( ( 1st ` h ) o. ( 1st ` i ) ) ) |
| 9 |
|
fveq2 |
|- ( g = i -> ( 2nd ` g ) = ( 2nd ` i ) ) |
| 10 |
9
|
oveq2d |
|- ( g = i -> ( ( 2nd ` h ) .+^ ( 2nd ` g ) ) = ( ( 2nd ` h ) .+^ ( 2nd ` i ) ) ) |
| 11 |
8 10
|
opeq12d |
|- ( g = i -> <. ( ( 1st ` h ) o. ( 1st ` g ) ) , ( ( 2nd ` h ) .+^ ( 2nd ` g ) ) >. = <. ( ( 1st ` h ) o. ( 1st ` i ) ) , ( ( 2nd ` h ) .+^ ( 2nd ` i ) ) >. ) |
| 12 |
6 11
|
cbvmpov |
|- ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) = ( h e. ( T X. E ) , i e. ( T X. E ) |-> <. ( ( 1st ` h ) o. ( 1st ` i ) ) , ( ( 2nd ` h ) .+^ ( 2nd ` i ) ) >. ) |
| 13 |
1 12
|
eqtri |
|- .+ = ( h e. ( T X. E ) , i e. ( T X. E ) |-> <. ( ( 1st ` h ) o. ( 1st ` i ) ) , ( ( 2nd ` h ) .+^ ( 2nd ` i ) ) >. ) |