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		ofeq	$$⊢{+}_{\mathrm{Scalar}\left(w\right)}=\underset{\dot{}}{+}\to {\circ }_f{+}_{\mathrm{Scalar}\left(w\right)}={\circ }_f\underset{\dot{}}{+}$$
21	19 20	syl	$$⊢w=W\to {\circ }_f{+}_{\mathrm{Scalar}\left(w\right)}={\circ }_f\underset{\dot{}}{+}$$
22	14	sqxpeqd	$$⊢w=W\to \mathrm{LFnl}\left(w\right)\times \mathrm{LFnl}\left(w\right)=F\times F$$
23	21 22	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)}$$
24	23 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{}}{✚}$$
25	24	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{}}{✚}⟩$$
26	17	fveq2d	$$⊢w=W\to {opp}_r\left(\mathrm{Scalar}\left(w\right)\right)={opp}_r\left(R\right)$$
27	26 9	eqtr4di	$$⊢w=W\to {opp}_r\left(\mathrm{Scalar}\left(w\right)\right)=O$$
28	27	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⟩$$
29	15 25 28	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\}$$
30	17	fveq2d	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}={\mathrm{Base}}_R$$
31	30 7	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}=K$$
32	17	fveq2d	$$⊢w=W\to {\cdot }_{\mathrm{Scalar}\left(w\right)}={\cdot }_R$$
33	32 8	eqtr4di	$$⊢w=W\to {\cdot }_{\mathrm{Scalar}\left(w\right)}=\underset{\dot{}}{·}$$
34		ofeq	$$⊢{\cdot }_{\mathrm{Scalar}\left(w\right)}=\underset{\dot{}}{·}\to {\circ }_f{\cdot }_{\mathrm{Scalar}\left(w\right)}={\circ }_f\underset{\dot{}}{·}$$
35	33 34	syl	$$⊢w=W\to {\circ }_f{\cdot }_{\mathrm{Scalar}\left(w\right)}={\circ }_f\underset{\dot{}}{·}$$
36		eqidd	$$⊢w=W\to f=f$$
37		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
38	37 1	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_w=V$$
39	38	xpeq1d	$$⊢w=W\to {\mathrm{Base}}_w\times \left\{k\right\}=V\times \left\{k\right\}$$
40	35 36 39	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)$$
41	31 14 40	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)$$
42	41 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 }$$
43	42	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 }⟩$$
44	43	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\}$$
45	29 44	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\}$$
46		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)$$
47		tpex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{✚}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),O⟩\right\}\in \mathrm{V}$$
48		snex	$$⊢\left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\bullet }⟩\right\}\in \mathrm{V}$$
49	47 48	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}$$
50	45 46 49	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\}$$
51	5 50	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\}$$
52	11 12 51	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\}$$