Metamath Proof Explorer


Theorem dvhvaddcbv

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

Ref Expression
Hypothesis dvhvaddval.a + ˙ = f T × E , g T × E 1 st f 1 st g 2 nd f ˙ 2 nd g
Assertion dvhvaddcbv + ˙ = h T × E , i T × E 1 st h 1 st i 2 nd h ˙ 2 nd i

Proof

Step Hyp Ref Expression
1 dvhvaddval.a + ˙ = f T × E , g T × E 1 st f 1 st g 2 nd f ˙ 2 nd g
2 fveq2 f = h 1 st f = 1 st h
3 2 coeq1d f = h 1 st f 1 st g = 1 st h 1 st g
4 fveq2 f = h 2 nd f = 2 nd h
5 4 oveq1d f = h 2 nd f ˙ 2 nd g = 2 nd h ˙ 2 nd g
6 3 5 opeq12d f = h 1 st f 1 st g 2 nd f ˙ 2 nd g = 1 st h 1 st g 2 nd h ˙ 2 nd g
7 fveq2 g = i 1 st g = 1 st i
8 7 coeq2d g = i 1 st h 1 st g = 1 st h 1 st i
9 fveq2 g = i 2 nd g = 2 nd i
10 9 oveq2d g = i 2 nd h ˙ 2 nd g = 2 nd h ˙ 2 nd i
11 8 10 opeq12d g = i 1 st h 1 st g 2 nd h ˙ 2 nd g = 1 st h 1 st i 2 nd h ˙ 2 nd i
12 6 11 cbvmpov f T × E , g T × E 1 st f 1 st g 2 nd f ˙ 2 nd g = h T × E , i T × E 1 st h 1 st i 2 nd h ˙ 2 nd i
13 1 12 eqtri + ˙ = h T × E , i T × E 1 st h 1 st i 2 nd h ˙ 2 nd i