Theorem ldualfvs

Description: Scalar product operation 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$$
	ldualfvs.m	$$⊢\underset{\dot{}}{·}=\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)$$
Assertion	ldualfvs	$$⊢\phi \to \underset{\dot{}}{\bullet }=\underset{\dot{}}{·}$$

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		ldualfvs.m	$$⊢\underset{\dot{}}{·}=\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)$$
10		eqid	$$⊢{+}_R={+}_R$$
11		eqid	$$⊢{{\circ }_f{+}_R\upharpoonright }_{\left(F\times F\right)}={{\circ }_f{+}_R\upharpoonright }_{\left(F\times F\right)}$$
12		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
13		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)$$
14	2 10 11 1 6 3 4 5 12 13 8	ldualset	$$⊢\phi \to D=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_R\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)⟩\right\}$$
15	14	fveq2d	$$⊢\phi \to {\cdot }_D={\cdot }_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_R\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)⟩\right\}\right)}$$
16	4	fvexi	$$⊢K\in \mathrm{V}$$
17	1	fvexi	$$⊢F\in \mathrm{V}$$
18	16 17	mpoex	$$⊢\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)\in \mathrm{V}$$
19		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_R\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_R\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)⟩\right\}$$
20	19	lmodvsca	$$⊢\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)\in \mathrm{V}\to \left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)={\cdot }_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_R\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)⟩\right\}\right)}$$
21	18 20	ax-mp	$$⊢\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)={\cdot }_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_R\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)⟩\right\}\right)}$$
22	9 21	eqtri	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_R\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in K,f\in F⟼f{\underset{\dot{}}{\times }}_f\left(V\times \left\{k\right\}\right)\right)⟩\right\}\right)}$$
23	15 7 22	3eqtr4g	$$⊢\phi \to \underset{\dot{}}{\bullet }=\underset{\dot{}}{·}$$