Theorem dvhvaddval

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-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	dvhvaddval	$$⊢\left(F\in \left(T\times E\right)\wedge G\in \left(T\times E\right)\right)\to F\underset{\dot{}}{+}G=⟨1^{st}\left(F\right)\circ 1^{st}\left(G\right),2^{nd}\left(F\right)\underset{\dot{}}{⨣}{2}^{nd}\left(G\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	$$⊢h=F\to 1^{st}\left(h\right)=1^{st}\left(F\right)$$
3	2	coeq1d	$$⊢h=F\to 1^{st}\left(h\right)\circ 1^{st}\left(i\right)=1^{st}\left(F\right)\circ 1^{st}\left(i\right)$$
4		fveq2	$$⊢h=F\to 2^{nd}\left(h\right)=2^{nd}\left(F\right)$$
5	4	oveq1d	$$⊢h=F\to 2^{nd}\left(h\right)\underset{\dot{}}{⨣}{2}^{nd}\left(i\right)=2^{nd}\left(F\right)\underset{\dot{}}{⨣}{2}^{nd}\left(i\right)$$
6	3 5	opeq12d	$$⊢h=F\to ⟨1^{st}\left(h\right)\circ 1^{st}\left(i\right),2^{nd}\left(h\right)\underset{\dot{}}{⨣}{2}^{nd}\left(i\right)⟩=⟨1^{st}\left(F\right)\circ 1^{st}\left(i\right),2^{nd}\left(F\right)\underset{\dot{}}{⨣}{2}^{nd}\left(i\right)⟩$$
7		fveq2	$$⊢i=G\to 1^{st}\left(i\right)=1^{st}\left(G\right)$$
8	7	coeq2d	$$⊢i=G\to 1^{st}\left(F\right)\circ 1^{st}\left(i\right)=1^{st}\left(F\right)\circ 1^{st}\left(G\right)$$
9		fveq2	$$⊢i=G\to 2^{nd}\left(i\right)=2^{nd}\left(G\right)$$
10	9	oveq2d	$$⊢i=G\to 2^{nd}\left(F\right)\underset{\dot{}}{⨣}{2}^{nd}\left(i\right)=2^{nd}\left(F\right)\underset{\dot{}}{⨣}{2}^{nd}\left(G\right)$$
11	8 10	opeq12d	$$⊢i=G\to ⟨1^{st}\left(F\right)\circ 1^{st}\left(i\right),2^{nd}\left(F\right)\underset{\dot{}}{⨣}{2}^{nd}\left(i\right)⟩=⟨1^{st}\left(F\right)\circ 1^{st}\left(G\right),2^{nd}\left(F\right)\underset{\dot{}}{⨣}{2}^{nd}\left(G\right)⟩$$
12	1	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)$$
13		opex	$$⊢⟨1^{st}\left(F\right)\circ 1^{st}\left(G\right),2^{nd}\left(F\right)\underset{\dot{}}{⨣}{2}^{nd}\left(G\right)⟩\in \mathrm{V}$$
14	6 11 12 13	ovmpo	$$⊢\left(F\in \left(T\times E\right)\wedge G\in \left(T\times E\right)\right)\to F\underset{\dot{}}{+}G=⟨1^{st}\left(F\right)\circ 1^{st}\left(G\right),2^{nd}\left(F\right)\underset{\dot{}}{⨣}{2}^{nd}\left(G\right)⟩$$