Theorem dvafvadd

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

	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	dvafvadd	$$⊢\left(K\in X\wedge W\in H\right)\to \underset{\dot{}}{+}=\left(f\in T,g\in T⟼f\circ g\right)$$

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		eqid	$$⊢\mathrm{TEndo}\left(K\right)\left(W\right)=\mathrm{TEndo}\left(K\right)\left(W\right)$$
6		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
7	1 2 5 6 3	dvaset	$$⊢\left(K\in X\wedge W\in H\right)\to U=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(K\right)\left(W\right),f\in T⟼s\left(f\right)\right)⟩\right\}$$
8	7	fveq2d	$$⊢\left(K\in X\wedge W\in H\right)\to {+}_U={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(K\right)\left(W\right),f\in T⟼s\left(f\right)\right)⟩\right\}\right)}$$
9	2	fvexi	$$⊢T\in \mathrm{V}$$
10	9 9	mpoex	$$⊢\left(f\in T,g\in T⟼f\circ g\right)\in \mathrm{V}$$
11		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(K\right)\left(W\right),f\in T⟼s\left(f\right)\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(K\right)\left(W\right),f\in T⟼s\left(f\right)\right)⟩\right\}$$
12	11	lmodplusg	$$⊢\left(f\in T,g\in T⟼f\circ g\right)\in \mathrm{V}\to \left(f\in T,g\in T⟼f\circ g\right)={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(K\right)\left(W\right),f\in T⟼s\left(f\right)\right)⟩\right\}\right)}$$
13	10 12	ax-mp	$$⊢\left(f\in T,g\in T⟼f\circ g\right)={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T⟩,⟨{+}_{\mathrm{ndx}},\left(f\in T,g\in T⟼f\circ g\right)⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(K\right)\left(W\right),f\in T⟼s\left(f\right)\right)⟩\right\}\right)}$$
14	8 4 13	3eqtr4g	$$⊢\left(K\in X\wedge W\in H\right)\to \underset{\dot{}}{+}=\left(f\in T,g\in T⟼f\circ g\right)$$