Theorem dvhfvsca

Description: Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013) (Revised by Mario Carneiro, 23-Jun-2014)

	Ref	Expression
Hypotheses	dvhfvsca.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dvhfvsca.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dvhfvsca.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dvhfvsca.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dvhfvsca.s	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
Assertion	dvhfvsca	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{·}=\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)$$

Proof

Step	Hyp	Ref	Expression
1		dvhfvsca.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dvhfvsca.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		dvhfvsca.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4		dvhfvsca.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		dvhfvsca.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	dvhset	$$⊢\left(K\in V\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 V\wedge W\in H\right)\to {\cdot }_U={\cdot }_{\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	3	fvexi	$$⊢E\in \mathrm{V}$$
10	2	fvexi	$$⊢T\in \mathrm{V}$$
11	10 9	xpex	$$⊢T\times E\in \mathrm{V}$$
12	9 11	mpoex	$$⊢\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)\in \mathrm{V}$$
13		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\}$$
14	13	lmodvsca	$$⊢\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)\in \mathrm{V}\to \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)={\cdot }_{\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	12 14	ax-mp	$$⊢\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)={\cdot }_{\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)}$$
16	8 5 15	3eqtr4g	$$⊢\left(K\in V\wedge W\in H\right)\to \underset{\dot{}}{·}=\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)$$