Theorem dvhvscaval

Description: The scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Nov-2013)

	Ref	Expression
Hypothesis	dvhvscaval.s	$$⊢\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)$$
Assertion	dvhvscaval	$$⊢\left(U\in E\wedge F\in \left(T\times E\right)\right)\to U\underset{\dot{}}{·}F=⟨U\left(1^{st}\left(F\right)\right),U\circ 2^{nd}\left(F\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		dvhvscaval.s	$$⊢\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)$$
2		fveq1	$$⊢t=U\to t\left(1^{st}\left(g\right)\right)=U\left(1^{st}\left(g\right)\right)$$
3		coeq1	$$⊢t=U\to t\circ 2^{nd}\left(g\right)=U\circ 2^{nd}\left(g\right)$$
4	2 3	opeq12d	$$⊢t=U\to ⟨t\left(1^{st}\left(g\right)\right),t\circ 2^{nd}\left(g\right)⟩=⟨U\left(1^{st}\left(g\right)\right),U\circ 2^{nd}\left(g\right)⟩$$
5		2fveq3	$$⊢g=F\to U\left(1^{st}\left(g\right)\right)=U\left(1^{st}\left(F\right)\right)$$
6		fveq2	$$⊢g=F\to 2^{nd}\left(g\right)=2^{nd}\left(F\right)$$
7	6	coeq2d	$$⊢g=F\to U\circ 2^{nd}\left(g\right)=U\circ 2^{nd}\left(F\right)$$
8	5 7	opeq12d	$$⊢g=F\to ⟨U\left(1^{st}\left(g\right)\right),U\circ 2^{nd}\left(g\right)⟩=⟨U\left(1^{st}\left(F\right)\right),U\circ 2^{nd}\left(F\right)⟩$$
9	1	dvhvscacbv	$$⊢\underset{\dot{}}{·}=\left(t\in E,g\in \left(T\times E\right)⟼⟨t\left(1^{st}\left(g\right)\right),t\circ 2^{nd}\left(g\right)⟩\right)$$
10		opex	$$⊢⟨U\left(1^{st}\left(F\right)\right),U\circ 2^{nd}\left(F\right)⟩\in \mathrm{V}$$
11	4 8 9 10	ovmpo	$$⊢\left(U\in E\wedge F\in \left(T\times E\right)\right)\to U\underset{\dot{}}{·}F=⟨U\left(1^{st}\left(F\right)\right),U\circ 2^{nd}\left(F\right)⟩$$