Theorem dvhvaddcbv

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

	Ref	Expression
Hypothesis	dvhvaddval.a	$$⊢\underset{\dot{}}{+}=\left(f\in \left(T\times E\right),g\in \left(T\times E\right)⟼⟨1^{st}\left(f\right)\circ 1^{st}\left(g\right),2^{nd}\left(f\right)\underset{\dot{}}{⨣}{2}^{nd}\left(g\right)⟩\right)$$
Assertion	dvhvaddcbv	$$⊢\underset{\dot{}}{+}=\left(h\in \left(T\times E\right),i\in \left(T\times E\right)⟼⟨1^{st}\left(h\right)\circ 1^{st}\left(i\right),2^{nd}\left(h\right)\underset{\dot{}}{⨣}{2}^{nd}\left(i\right)⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvhvaddval.a	$$⊢\underset{\dot{}}{+}=\left(f\in \left(T\times E\right),g\in \left(T\times E\right)⟼⟨1^{st}\left(f\right)\circ 1^{st}\left(g\right),2^{nd}\left(f\right)\underset{\dot{}}{⨣}{2}^{nd}\left(g\right)⟩\right)$$
2		fveq2	$$⊢f=h\to 1^{st}\left(f\right)=1^{st}\left(h\right)$$
3	2	coeq1d	$$⊢f=h\to 1^{st}\left(f\right)\circ 1^{st}\left(g\right)=1^{st}\left(h\right)\circ 1^{st}\left(g\right)$$
4		fveq2	$$⊢f=h\to 2^{nd}\left(f\right)=2^{nd}\left(h\right)$$
5	4	oveq1d	$$⊢f=h\to 2^{nd}\left(f\right)\underset{\dot{}}{⨣}{2}^{nd}\left(g\right)=2^{nd}\left(h\right)\underset{\dot{}}{⨣}{2}^{nd}\left(g\right)$$
6	3 5	opeq12d	$$⊢f=h\to ⟨1^{st}\left(f\right)\circ 1^{st}\left(g\right),2^{nd}\left(f\right)\underset{\dot{}}{⨣}{2}^{nd}\left(g\right)⟩=⟨1^{st}\left(h\right)\circ 1^{st}\left(g\right),2^{nd}\left(h\right)\underset{\dot{}}{⨣}{2}^{nd}\left(g\right)⟩$$
7		fveq2	$$⊢g=i\to 1^{st}\left(g\right)=1^{st}\left(i\right)$$
8	7	coeq2d	$$⊢g=i\to 1^{st}\left(h\right)\circ 1^{st}\left(g\right)=1^{st}\left(h\right)\circ 1^{st}\left(i\right)$$
9		fveq2	$$⊢g=i\to 2^{nd}\left(g\right)=2^{nd}\left(i\right)$$
10	9	oveq2d	$$⊢g=i\to 2^{nd}\left(h\right)\underset{\dot{}}{⨣}{2}^{nd}\left(g\right)=2^{nd}\left(h\right)\underset{\dot{}}{⨣}{2}^{nd}\left(i\right)$$
11	8 10	opeq12d	$$⊢g=i\to ⟨1^{st}\left(h\right)\circ 1^{st}\left(g\right),2^{nd}\left(h\right)\underset{\dot{}}{⨣}{2}^{nd}\left(g\right)⟩=⟨1^{st}\left(h\right)\circ 1^{st}\left(i\right),2^{nd}\left(h\right)\underset{\dot{}}{⨣}{2}^{nd}\left(i\right)⟩$$
12	6 11	cbvmpov	$$⊢\left(f\in \left(T\times E\right),g\in \left(T\times E\right)⟼⟨1^{st}\left(f\right)\circ 1^{st}\left(g\right),2^{nd}\left(f\right)\underset{\dot{}}{⨣}{2}^{nd}\left(g\right)⟩\right)=\left(h\in \left(T\times E\right),i\in \left(T\times E\right)⟼⟨1^{st}\left(h\right)\circ 1^{st}\left(i\right),2^{nd}\left(h\right)\underset{\dot{}}{⨣}{2}^{nd}\left(i\right)⟩\right)$$
13	1 12	eqtri	$$⊢\underset{\dot{}}{+}=\left(h\in \left(T\times E\right),i\in \left(T\times E\right)⟼⟨1^{st}\left(h\right)\circ 1^{st}\left(i\right),2^{nd}\left(h\right)\underset{\dot{}}{⨣}{2}^{nd}\left(i\right)⟩\right)$$