Theorem dvhvadd

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 11-Feb-2014) (Revised by Mario Carneiro, 23-Jun-2014)

	Ref	Expression
Hypotheses	dvhvadd.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvhvadd.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dvhvadd.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dvhvadd.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dvhvadd.f	$$⊢D=\mathrm{Scalar}\left(U\right)$$
	dvhvadd.s	$$⊢\underset{\dot{}}{+}={+}_U$$
	dvhvadd.p	$$⊢\underset{\dot{}}{⨣}={+}_D$$
Assertion	dvhvadd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(F\in \left(T\times E\right)\wedge G\in \left(T\times E\right)\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		dvhvadd.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvhvadd.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		dvhvadd.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4		dvhvadd.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		dvhvadd.f	$$⊢D=\mathrm{Scalar}\left(U\right)$$
6		dvhvadd.s	$$⊢\underset{\dot{}}{+}={+}_U$$
7		dvhvadd.p	$$⊢\underset{\dot{}}{⨣}={+}_D$$
8		eqid	$$⊢\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(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)$$
9	1 2 3 4 5 7 8 6	dvhfvadd	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \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)$$
10	9	oveqd	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to F\underset{\dot{}}{+}G=F\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)G$$
11	8	dvhvaddval	$$⊢\left(F\in \left(T\times E\right)\wedge G\in \left(T\times E\right)\right)\to F\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)G=⟨1^{st}\left(F\right)\circ 1^{st}\left(G\right),2^{nd}\left(F\right)\underset{\dot{}}{⨣}{2}^{nd}\left(G\right)⟩$$
12	10 11	sylan9eq	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(F\in \left(T\times E\right)\wedge G\in \left(T\times E\right)\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)⟩$$