Theorem ldualvbase

Description: The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014)

	Ref	Expression
Hypotheses	ldualvbase.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualvbase.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualvbase.v	$$⊢V={\mathrm{Base}}_D$$
	ldualvbase.w	$$⊢\phi \to W\in X$$
Assertion	ldualvbase	$$⊢\phi \to V=F$$

Proof

Step	Hyp	Ref	Expression
1		ldualvbase.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualvbase.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
3		ldualvbase.v	$$⊢V={\mathrm{Base}}_D$$
4		ldualvbase.w	$$⊢\phi \to W\in X$$
5		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
6		eqid	$$⊢{+}_{\mathrm{Scalar}\left(W\right)}={+}_{\mathrm{Scalar}\left(W\right)}$$
7		eqid	$$⊢{{\circ }_f{+}_{\mathrm{Scalar}\left(W\right)}\upharpoonright }_{\left(F\times F\right)}={{\circ }_f{+}_{\mathrm{Scalar}\left(W\right)}\upharpoonright }_{\left(F\times F\right)}$$
8		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
9		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
10		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(W\right)}={\cdot }_{\mathrm{Scalar}\left(W\right)}$$
11		eqid	$$⊢{opp}_r\left(\mathrm{Scalar}\left(W\right)\right)={opp}_r\left(\mathrm{Scalar}\left(W\right)\right)$$
12		eqid	$$⊢\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)},f\in F⟼f{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)=\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)},f\in F⟼f{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)$$
13	5 6 7 1 2 8 9 10 11 12 4	ldualset	$$⊢\phi \to D=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(W\right)}\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(W\right)\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)},f\in F⟼f{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)⟩\right\}$$
14	13	fveq2d	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(W\right)}\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(W\right)\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)},f\in F⟼f{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)⟩\right\}\right)}$$
15	1	fvexi	$$⊢F\in \mathrm{V}$$
16		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(W\right)}\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(W\right)\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)},f\in F⟼f{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(W\right)}\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(W\right)\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)},f\in F⟼f{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)⟩\right\}$$
17	16	lmodbase	$$⊢F\in \mathrm{V}\to F={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(W\right)}\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(W\right)\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)},f\in F⟼f{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)⟩\right\}\right)}$$
18	15 17	ax-mp	$$⊢F={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(W\right)}\upharpoonright }_{\left(F\times F\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(W\right)\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)},f\in F⟼f{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)⟩\right\}\right)}$$
19	14 3 18	3eqtr4g	$$⊢\phi \to V=F$$