Theorem dvhvbase

Description: The vectors (vector base set) of the constructed full vector space H are all translations (for a fiducial co-atom W ). (Contributed by NM, 2-Nov-2013) (Revised by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	dvhvbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvhvbase.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dvhvbase.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dvhvbase.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dvhvbase.v	$$⊢V={\mathrm{Base}}_U$$
Assertion	dvhvbase	$$⊢\left(K\in X\wedge W\in H\right)\to V=T\times E$$

Proof

Step	Hyp	Ref	Expression
1		dvhvbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvhvbase.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		dvhvbase.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4		dvhvbase.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		dvhvbase.v	$$⊢V={\mathrm{Base}}_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	dvhset	$$⊢\left(K\in X\wedge W\in H\right)\to U=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T\times E⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(T\times E\right),g\in \left(T\times E\right)⟼⟨1^{st}\left(f\right)\circ 1^{st}\left(g\right),\left(h\in T⟼2^{nd}\left(f\right)\left(h\right)\circ 2^{nd}\left(g\right)\left(h\right)\right)⟩\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 \left(T\times E\right)⟼⟨s\left(1^{st}\left(f\right)\right),s\circ 2^{nd}\left(f\right)⟩\right)⟩\right\}$$
8	7	fveq2d	$$⊢\left(K\in X\wedge W\in H\right)\to {\mathrm{Base}}_U={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T\times E⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(T\times E\right),g\in \left(T\times E\right)⟼⟨1^{st}\left(f\right)\circ 1^{st}\left(g\right),\left(h\in T⟼2^{nd}\left(f\right)\left(h\right)\circ 2^{nd}\left(g\right)\left(h\right)\right)⟩\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 \left(T\times E\right)⟼⟨s\left(1^{st}\left(f\right)\right),s\circ 2^{nd}\left(f\right)⟩\right)⟩\right\}\right)}$$
9	2	fvexi	$$⊢T\in \mathrm{V}$$
10	3	fvexi	$$⊢E\in \mathrm{V}$$
11	9 10	xpex	$$⊢T\times E\in \mathrm{V}$$
12		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T\times E⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(T\times E\right),g\in \left(T\times E\right)⟼⟨1^{st}\left(f\right)\circ 1^{st}\left(g\right),\left(h\in T⟼2^{nd}\left(f\right)\left(h\right)\circ 2^{nd}\left(g\right)\left(h\right)\right)⟩\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 \left(T\times E\right)⟼⟨s\left(1^{st}\left(f\right)\right),s\circ 2^{nd}\left(f\right)⟩\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T\times E⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(T\times E\right),g\in \left(T\times E\right)⟼⟨1^{st}\left(f\right)\circ 1^{st}\left(g\right),\left(h\in T⟼2^{nd}\left(f\right)\left(h\right)\circ 2^{nd}\left(g\right)\left(h\right)\right)⟩\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 \left(T\times E\right)⟼⟨s\left(1^{st}\left(f\right)\right),s\circ 2^{nd}\left(f\right)⟩\right)⟩\right\}$$
13	12	lmodbase	$$⊢T\times E\in \mathrm{V}\to T\times E={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T\times E⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(T\times E\right),g\in \left(T\times E\right)⟼⟨1^{st}\left(f\right)\circ 1^{st}\left(g\right),\left(h\in T⟼2^{nd}\left(f\right)\left(h\right)\circ 2^{nd}\left(g\right)\left(h\right)\right)⟩\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 \left(T\times E\right)⟼⟨s\left(1^{st}\left(f\right)\right),s\circ 2^{nd}\left(f\right)⟩\right)⟩\right\}\right)}$$
14	11 13	ax-mp	$$⊢T\times E={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},T\times E⟩,⟨{+}_{\mathrm{ndx}},\left(f\in \left(T\times E\right),g\in \left(T\times E\right)⟼⟨1^{st}\left(f\right)\circ 1^{st}\left(g\right),\left(h\in T⟼2^{nd}\left(f\right)\left(h\right)\circ 2^{nd}\left(g\right)\left(h\right)\right)⟩\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 \left(T\times E\right)⟼⟨s\left(1^{st}\left(f\right)\right),s\circ 2^{nd}\left(f\right)⟩\right)⟩\right\}\right)}$$
15	8 5 14	3eqtr4g	$$⊢\left(K\in X\wedge W\in H\right)\to V=T\times E$$