Theorem ldualvs

Description: Scalar product operation value (which is a functional) for the dual of a vector space. (Contributed by NM, 18-Oct-2014)

	Ref	Expression
Hypotheses	ldualfvs.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualfvs.v	$$⊢V={\mathrm{Base}}_W$$
	ldualfvs.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualfvs.k	$$⊢K={\mathrm{Base}}_R$$
	ldualfvs.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	ldualfvs.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualfvs.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_D$$
	ldualfvs.w	$$⊢\phi \to W\in Y$$
	ldualvs.x	$$⊢\phi \to X\in K$$
	ldualvs.g	$$⊢\phi \to G\in F$$
Assertion	ldualvs	$$⊢\phi \to X\underset{\dot{}}{\bullet }G=G{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ldualfvs.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualfvs.v	$$⊢V={\mathrm{Base}}_W$$
3		ldualfvs.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
4		ldualfvs.k	$$⊢K={\mathrm{Base}}_R$$
5		ldualfvs.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
6		ldualfvs.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
7		ldualfvs.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_D$$
8		ldualfvs.w	$$⊢\phi \to W\in Y$$
9		ldualvs.x	$$⊢\phi \to X\in K$$
10		ldualvs.g	$$⊢\phi \to G\in F$$
11		eqid	$$⊢\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)=\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)$$
12	1 2 3 4 5 6 7 8 11	ldualfvs	$$⊢\phi \to \underset{\dot{}}{\bullet }=\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)$$
13	12	oveqd	$$⊢\phi \to X\underset{\dot{}}{\bullet }G=X\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)G$$
14		sneq	$$⊢k=X\to \left\{k\right\}=\left\{X\right\}$$
15	14	xpeq2d	$$⊢k=X\to V\times \left\{k\right\}=V\times \left\{X\right\}$$
16	15	oveq2d	$$⊢k=X\to f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)=f{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)$$
17		oveq1	$$⊢f=G\to f{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)=G{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)$$
18		ovex	$$⊢G{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)\in \mathrm{V}$$
19	16 17 11 18	ovmpo	$$⊢\left(X\in K\wedge G\in F\right)\to X\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)G=G{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)$$
20	9 10 19	syl2anc	$$⊢\phi \to X\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)G=G{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)$$
21	13 20	eqtrd	$$⊢\phi \to X\underset{\dot{}}{\bullet }G=G{\underset{\dot{}}{\times }}_f\left(V\times \left\{X\right\}\right)$$