Theorem dvavadd

Description: Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013)

	Ref	Expression
Hypotheses	dvafvadd.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvafvadd.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dvafvadd.u	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
	dvafvadd.v	$$⊢\underset{\dot{}}{+}={+}_U$$
Assertion	dvavadd	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(F\in T\wedge G\in T\right)\right)\to F\underset{\dot{}}{+}G=F\circ G$$

Proof

Step	Hyp	Ref	Expression
1		dvafvadd.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvafvadd.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		dvafvadd.u	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
4		dvafvadd.v	$$⊢\underset{\dot{}}{+}={+}_U$$
5	1 2 3 4	dvafvadd	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{+}=\left(f\in T,g\in T⟼f\circ g\right)$$
6	5	oveqd	$$⊢\left(K\in V\wedge W\in H\right)\to F\underset{\dot{}}{+}G=F\left(f\in T,g\in T⟼f\circ g\right)G$$
7		coexg	$$⊢\left(F\in T\wedge G\in T\right)\to F\circ G\in \mathrm{V}$$
8		coeq1	$$⊢f=F\to f\circ g=F\circ g$$
9		coeq2	$$⊢g=G\to F\circ g=F\circ G$$
10		eqid	$$⊢\left(f\in T,g\in T⟼f\circ g\right)=\left(f\in T,g\in T⟼f\circ g\right)$$
11	8 9 10	ovmpog	$$⊢\left(F\in T\wedge G\in T\wedge F\circ G\in \mathrm{V}\right)\to F\left(f\in T,g\in T⟼f\circ g\right)G=F\circ G$$
12	7 11	mpd3an3	$$⊢\left(F\in T\wedge G\in T\right)\to F\left(f\in T,g\in T⟼f\circ g\right)G=F\circ G$$
13	6 12	sylan9eq	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(F\in T\wedge G\in T\right)\right)\to F\underset{\dot{}}{+}G=F\circ G$$