Theorem ldualset

Description: Define the (left) dual of a left vector space (or module) in which the vectors are functionals. In many texts, this is defined as a right vector space, but by reversing the multiplication we achieve a left vector space, as is done in definition of dual vector space in Holland95 p. 218. This allows us to reuse our existing collection of left vector space theorems. Note the operation reversal in the scalar product to allow us to use the original scalar ring instead of the oppR ring, for convenience. (Contributed by NM, 18-Oct-2014)

	Ref	Expression
Hypotheses	ldualset.v	$$⊢V={\mathrm{Base}}_W$$
	ldualset.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	ldualset.p	$$⊢\underset{\dot{}}{✚}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}$$
	ldualset.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualset.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualset.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualset.k	$$⊢K={\mathrm{Base}}_R$$
	ldualset.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	ldualset.o	$$⊢O={opp}_r\left(R\right)$$
	ldualset.s	$$⊢\underset{\dot{}}{\bullet }=\left(k\in K,f\in F⟼f{\underset{\dot{}}{·}}_f\left(V\times \left\{k\right\}\right)\right)$$
	ldualset.w	$$⊢\phi \to W\in X$$
Assertion	ldualset	$$⊢\phi \to D=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{✚}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),O⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\bullet }⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ldualset.v	$$⊢V={\mathrm{Base}}_W$$
2		ldualset.a	$$⊢\underset{\dot{}}{+}={+}_R$$
3		ldualset.p	$$⊢\underset{\dot{}}{✚}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}$$
4		ldualset.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
5		ldualset.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
6		ldualset.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
7		ldualset.k	$$⊢K={\mathrm{Base}}_R$$
8		ldualset.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
9		ldualset.o	$$⊢O={opp}_r\left(R\right)$$
10		ldualset.s	$$⊢\underset{\dot{}}{\bullet }=\left(k\in K,f\in F⟼f{\underset{\dot{}}{·}}_f\left(V\times \left\{k\right\}\right)\right)$$
11		ldualset.w	$$⊢\phi \to W\in X$$
12		elex	$$⊢W\in X\to W\in \mathrm{V}$$
13		fveq2	$$⊢w=W\to \mathrm{LFnl}\left(w\right)=\mathrm{LFnl}\left(W\right)$$
14	13 4	eqtr4di	$$⊢w=W\to \mathrm{LFnl}\left(w\right)=F$$
15	14	opeq2d	$$⊢w=W\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{LFnl}\left(w\right)⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩$$
16		fveq2	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=\mathrm{Scalar}\left(W\right)$$
17	16 6	eqtr4di	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=R$$
18	17	fveq2d	$$⊢w=W\to {+}_{\mathrm{Scalar}\left(w\right)}={+}_R$$
19	18 2	eqtr4di	$$⊢w=W\to {+}_{\mathrm{Scalar}\left(w\right)}=\underset{\dot{}}{+}$$
20	19	ofeqd	$$⊢w=W\to {\circ }_f{+}_{\mathrm{Scalar}\left(w\right)}={\circ }_f\underset{\dot{}}{+}$$
21	14	sqxpeqd	$$⊢w=W\to \mathrm{LFnl}\left(w\right)\times \mathrm{LFnl}\left(w\right)=F\times F$$
22	20 21	reseq12d	$$⊢w=W\to {{\circ }_f{+}_{\mathrm{Scalar}\left(w\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(w\right)\times \mathrm{LFnl}\left(w\right)\right)}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}$$
23	22 3	eqtr4di	$$⊢w=W\to {{\circ }_f{+}_{\mathrm{Scalar}\left(w\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(w\right)\times \mathrm{LFnl}\left(w\right)\right)}=\underset{\dot{}}{✚}$$
24	23	opeq2d	$$⊢w=W\to ⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(w\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(w\right)\times \mathrm{LFnl}\left(w\right)\right)}⟩=⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{✚}⟩$$
25	17	fveq2d	$$⊢w=W\to {opp}_r\left(\mathrm{Scalar}\left(w\right)\right)={opp}_r\left(R\right)$$
26	25 9	eqtr4di	$$⊢w=W\to {opp}_r\left(\mathrm{Scalar}\left(w\right)\right)=O$$
27	26	opeq2d	$$⊢w=W\to ⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(w\right)\right)⟩=⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),O⟩$$
28	15 24 27	tpeq123d	$$⊢w=W\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{LFnl}\left(w\right)⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(w\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(w\right)\times \mathrm{LFnl}\left(w\right)\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(w\right)\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{✚}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),O⟩\right\}$$
29	17	fveq2d	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}={\mathrm{Base}}_R$$
30	29 7	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}=K$$
31	17	fveq2d	$$⊢w=W\to {\cdot }_{\mathrm{Scalar}\left(w\right)}={\cdot }_R$$
32	31 8	eqtr4di	$$⊢w=W\to {\cdot }_{\mathrm{Scalar}\left(w\right)}=\underset{\dot{}}{·}$$
33	32	ofeqd	$$⊢w=W\to {\circ }_f{\cdot }_{\mathrm{Scalar}\left(w\right)}={\circ }_f\underset{\dot{}}{·}$$
34		eqidd	$$⊢w=W\to f=f$$
35		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
36	35 1	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_w=V$$
37	36	xpeq1d	$$⊢w=W\to {\mathrm{Base}}_w\times \left\{k\right\}=V\times \left\{k\right\}$$
38	33 34 37	oveq123d	$$⊢w=W\to f{{\cdot }_{\mathrm{Scalar}\left(w\right)}}_f\left({\mathrm{Base}}_w\times \left\{k\right\}\right)=f{\underset{\dot{}}{·}}_f\left(V\times \left\{k\right\}\right)$$
39	30 14 38	mpoeq123dv	$$⊢w=W\to \left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)},f\in \mathrm{LFnl}\left(w\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(w\right)}}_f\left({\mathrm{Base}}_w\times \left\{k\right\}\right)\right)=\left(k\in K,f\in F⟼f{\underset{\dot{}}{·}}_f\left(V\times \left\{k\right\}\right)\right)$$
40	39 10	eqtr4di	$$⊢w=W\to \left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)},f\in \mathrm{LFnl}\left(w\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(w\right)}}_f\left({\mathrm{Base}}_w\times \left\{k\right\}\right)\right)=\underset{\dot{}}{\bullet }$$
41	40	opeq2d	$$⊢w=W\to ⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)},f\in \mathrm{LFnl}\left(w\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(w\right)}}_f\left({\mathrm{Base}}_w\times \left\{k\right\}\right)\right)⟩=⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\bullet }⟩$$
42	41	sneqd	$$⊢w=W\to \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)},f\in \mathrm{LFnl}\left(w\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(w\right)}}_f\left({\mathrm{Base}}_w\times \left\{k\right\}\right)\right)⟩\right\}=\left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\bullet }⟩\right\}$$
43	28 42	uneq12d	$$⊢w=W\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{LFnl}\left(w\right)⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(w\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(w\right)\times \mathrm{LFnl}\left(w\right)\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 \mathrm{LFnl}\left(w\right)⟼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}},\underset{\dot{}}{✚}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),O⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\bullet }⟩\right\}$$
44		df-ldual	$$⊢\mathrm{LDual}=\left(w\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{LFnl}\left(w\right)⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(w\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(w\right)\times \mathrm{LFnl}\left(w\right)\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 \mathrm{LFnl}\left(w\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(w\right)}}_f\left({\mathrm{Base}}_w\times \left\{k\right\}\right)\right)⟩\right\}\right)$$
45		tpex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{✚}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),O⟩\right\}\in \mathrm{V}$$
46		snex	$$⊢\left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\bullet }⟩\right\}\in \mathrm{V}$$
47	45 46	unex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{✚}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),O⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\bullet }⟩\right\}\in \mathrm{V}$$
48	43 44 47	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{LDual}\left(W\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{✚}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),O⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\bullet }⟩\right\}$$
49	5 48	syl5eq	$$⊢W\in \mathrm{V}\to D=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{✚}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),O⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\bullet }⟩\right\}$$
50	11 12 49	3syl	$$⊢\phi \to D=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{✚}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),O⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\bullet }⟩\right\}$$