Theorem ldualfvadd

Description: Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014)

	Ref	Expression
Hypotheses	ldualvadd.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualvadd.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualvadd.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	ldualvadd.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualvadd.p	$$⊢\underset{\dot{}}{✚}={+}_D$$
	ldualvadd.w	$$⊢\phi \to W\in X$$
	ldualfvadd.q	$$⊢\underset{\dot{}}{⨣}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}$$
Assertion	ldualfvadd	$$⊢\phi \to \underset{\dot{}}{✚}=\underset{\dot{}}{⨣}$$

Proof

Step	Hyp	Ref	Expression
1		ldualvadd.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualvadd.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		ldualvadd.a	$$⊢\underset{\dot{}}{+}={+}_R$$
4		ldualvadd.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
5		ldualvadd.p	$$⊢\underset{\dot{}}{✚}={+}_D$$
6		ldualvadd.w	$$⊢\phi \to W\in X$$
7		ldualfvadd.q	$$⊢\underset{\dot{}}{⨣}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}$$
8		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
9		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
10		eqid	$$⊢{\cdot }_R={\cdot }_R$$
11		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
12		eqid	$$⊢\left(k\in {\mathrm{Base}}_R,f\in F⟼f{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)=\left(k\in {\mathrm{Base}}_R,f\in F⟼f{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)$$
13	8 3 7 1 4 2 9 10 11 12 6	ldualset	$$⊢\phi \to D=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_R,f\in F⟼f{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)⟩\right\}$$
14	13	fveq2d	$$⊢\phi \to {+}_D={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_R,f\in F⟼f{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)⟩\right\}\right)}$$
15	1	fvexi	$$⊢F\in \mathrm{V}$$
16		id	$$⊢F\in \mathrm{V}\to F\in \mathrm{V}$$
17	16 16	ofmresex	$$⊢F\in \mathrm{V}\to {{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}\in \mathrm{V}$$
18	15 17	ax-mp	$$⊢{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}\in \mathrm{V}$$
19	7 18	eqeltri	$$⊢\underset{\dot{}}{⨣}\in \mathrm{V}$$
20		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_R,f\in F⟼f{{\cdot }_R}_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),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_R,f\in F⟼f{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)⟩\right\}$$
21	20	lmodplusg	$$⊢\underset{\dot{}}{⨣}\in \mathrm{V}\to \underset{\dot{}}{⨣}={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_R,f\in F⟼f{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)⟩\right\}\right)}$$
22	19 21	ax-mp	$$⊢\underset{\dot{}}{⨣}={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(R\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_R,f\in F⟼f{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)⟩\right\}\right)}$$
23	14 5 22	3eqtr4g	$$⊢\phi \to \underset{\dot{}}{✚}=\underset{\dot{}}{⨣}$$