Theorem dvafvsca

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	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	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)$$

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		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
7	1 2 3 6 4	dvaset	$$⊢\left(K\in V\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 E,f\in T⟼s\left(f\right)\right)⟩\right\}$$
8	7	fveq2d	$$⊢\left(K\in V\wedge W\in H\right)\to {\cdot }_U={\cdot }_{\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 E,f\in T⟼s\left(f\right)\right)⟩\right\}\right)}$$
9	3	fvexi	$$⊢E\in \mathrm{V}$$
10	2	fvexi	$$⊢T\in \mathrm{V}$$
11	9 10	mpoex	$$⊢\left(s\in E,f\in T⟼s\left(f\right)\right)\in \mathrm{V}$$
12		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 E,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 E,f\in T⟼s\left(f\right)\right)⟩\right\}$$
13	12	lmodvsca	$$⊢\left(s\in E,f\in T⟼s\left(f\right)\right)\in \mathrm{V}\to \left(s\in E,f\in T⟼s\left(f\right)\right)={\cdot }_{\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 E,f\in T⟼s\left(f\right)\right)⟩\right\}\right)}$$
14	11 13	ax-mp	$$⊢\left(s\in E,f\in T⟼s\left(f\right)\right)={\cdot }_{\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 E,f\in T⟼s\left(f\right)\right)⟩\right\}\right)}$$
15	8 5 14	3eqtr4g	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{·}=\left(s\in E,f\in T⟼s\left(f\right)\right)$$