Theorem dvafplusg

Description: Ring addition operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

	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	dvafplusg	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{+}=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\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		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
8	1 7 4 5	dvasca	$$⊢\left(K\in V\wedge W\in H\right)\to F=\mathrm{EDRing}\left(K\right)\left(W\right)$$
9	8	fveq2d	$$⊢\left(K\in V\wedge W\in H\right)\to {+}_F={+}_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
10	6 9	syl5eq	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{+}={+}_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
11		eqid	$$⊢{+}_{\mathrm{EDRing}\left(K\right)\left(W\right)}={+}_{\mathrm{EDRing}\left(K\right)\left(W\right)}$$
12	1 2 3 7 11	erngfplus	$$⊢\left(K\in V\wedge W\in H\right)\to {+}_{\mathrm{EDRing}\left(K\right)\left(W\right)}=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$
13	10 12	eqtrd	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{+}=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$