Theorem dvavsca

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

	Ref	Expression
Hypotheses	dvafvsca.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvafvsca.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dvafvsca.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dvafvsca.u	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
	dvafvsca.s	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
Assertion	dvavsca	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(R\in E\wedge F\in T\right)\right)\to R\underset{\dot{}}{·}F=R\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvafvsca.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvafvsca.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		dvafvsca.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4		dvafvsca.u	$$⊢U=\mathrm{DVecA}\left(K\right)\left(W\right)$$
5		dvafvsca.s	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
6	1 2 3 4 5	dvafvsca	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{·}=\left(s\in E,f\in T⟼s\left(f\right)\right)$$
7	6	oveqd	$$⊢\left(K\in V\wedge W\in H\right)\to R\underset{\dot{}}{·}F=R\left(s\in E,f\in T⟼s\left(f\right)\right)F$$
8		fveq1	$$⊢s=R\to s\left(f\right)=R\left(f\right)$$
9		fveq2	$$⊢f=F\to R\left(f\right)=R\left(F\right)$$
10		eqid	$$⊢\left(s\in E,f\in T⟼s\left(f\right)\right)=\left(s\in E,f\in T⟼s\left(f\right)\right)$$
11		fvex	$$⊢R\left(F\right)\in \mathrm{V}$$
12	8 9 10 11	ovmpo	$$⊢\left(R\in E\wedge F\in T\right)\to R\left(s\in E,f\in T⟼s\left(f\right)\right)F=R\left(F\right)$$
13	7 12	sylan9eq	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(R\in E\wedge F\in T\right)\right)\to R\underset{\dot{}}{·}F=R\left(F\right)$$