Metamath Proof Explorer


Theorem dvhvaddcbv

Description: Change bound variables to isolate them later. (Contributed by NM, 3-Nov-2013)

Ref Expression
Hypothesis dvhvaddval.a +˙=fT×E,gT×E1stf1stg2ndf˙2ndg
Assertion dvhvaddcbv +˙=hT×E,iT×E1sth1sti2ndh˙2ndi

Proof

Step Hyp Ref Expression
1 dvhvaddval.a +˙=fT×E,gT×E1stf1stg2ndf˙2ndg
2 fveq2 f=h1stf=1sth
3 2 coeq1d f=h1stf1stg=1sth1stg
4 fveq2 f=h2ndf=2ndh
5 4 oveq1d f=h2ndf˙2ndg=2ndh˙2ndg
6 3 5 opeq12d f=h1stf1stg2ndf˙2ndg=1sth1stg2ndh˙2ndg
7 fveq2 g=i1stg=1sti
8 7 coeq2d g=i1sth1stg=1sth1sti
9 fveq2 g=i2ndg=2ndi
10 9 oveq2d g=i2ndh˙2ndg=2ndh˙2ndi
11 8 10 opeq12d g=i1sth1stg2ndh˙2ndg=1sth1sti2ndh˙2ndi
12 6 11 cbvmpov fT×E,gT×E1stf1stg2ndf˙2ndg=hT×E,iT×E1sth1sti2ndh˙2ndi
13 1 12 eqtri +˙=hT×E,iT×E1sth1sti2ndh˙2ndi