Theorem dvaplusg

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

	Ref	Expression
Hypotheses	dvafplus.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvafplus.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dvafplus.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dvafplus.u	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
	dvafplus.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
	dvafplus.p	$$⊢\underset{\dot{}}{+}={+}_F$$
Assertion	dvaplusg	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(R\in E\wedge S\in E\right)\right)\to R\underset{\dot{}}{+}S=\left(f\in T⟼R\left(f\right)\circ S\left(f\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvafplus.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvafplus.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		dvafplus.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4		dvafplus.u	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
5		dvafplus.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
6		dvafplus.p	$$⊢\underset{\dot{}}{+}={+}_F$$
7	1 2 3 4 5 6	dvafplusg	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{+}=\left(s\in E,t\in E⟼\left(g\in T⟼s\left(g\right)\circ t\left(g\right)\right)\right)$$
8	7	oveqd	$$⊢\left(K\in V\wedge W\in H\right)\to R\underset{\dot{}}{+}S=R\left(s\in E,t\in E⟼\left(g\in T⟼s\left(g\right)\circ t\left(g\right)\right)\right)S$$
9		eqid	$$⊢\left(s\in E,t\in E⟼\left(g\in T⟼s\left(g\right)\circ t\left(g\right)\right)\right)=\left(s\in E,t\in E⟼\left(g\in T⟼s\left(g\right)\circ t\left(g\right)\right)\right)$$
10	9 2	tendopl	$$⊢\left(R\in E\wedge S\in E\right)\to R\left(s\in E,t\in E⟼\left(g\in T⟼s\left(g\right)\circ t\left(g\right)\right)\right)S=\left(f\in T⟼R\left(f\right)\circ S\left(f\right)\right)$$
11	8 10	sylan9eq	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(R\in E\wedge S\in E\right)\right)\to R\underset{\dot{}}{+}S=\left(f\in T⟼R\left(f\right)\circ S\left(f\right)\right)$$