Theorem dvhfplusr

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

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

Proof

Step	Hyp	Ref	Expression
1		dvhfplusr.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvhfplusr.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		dvhfplusr.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4		dvhfplusr.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		dvhfplusr.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
6		dvhfplusr.p	$$⊢\underset{\dot{}}{+}=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$
7		dvhfplusr.s	$$⊢\underset{\dot{}}{✚}={+}_F$$
8		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
9	1 8 4 5	dvhsca	$$⊢\left(K\in V\wedge W\in H\right)\to F=\mathrm{EDRing}\left(K\right)\left(W\right)$$
10	9	fveq2d	$$⊢\left(K\in V\wedge W\in H\right)\to {+}_F={+}_{\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 8 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 {+}_F=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$
14	13 7 6	3eqtr4g	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{✚}=\underset{\dot{}}{+}$$