Theorem dvhvaddcbv

Description: Change bound variables to isolate them later. (Contributed by NM, 3-Nov-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	dvhvaddcbv	|- .+ = ( h e. ( T X. E ) , i e. ( T X. E ) |-> <. ( ( 1st ` h ) o. ( 1st ` i ) ) , ( ( 2nd ` h ) .+^ ( 2nd ` i ) ) >. )

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