Theorem ldualsca

Description: The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014)

	Ref	Expression
Hypotheses	ldualsca.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	ldualsca.o	$$⊢O={opp}_r\left(F\right)$$
	ldualsca.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualsca.r	$$⊢R=\mathrm{Scalar}\left(D\right)$$
	ldualsca.w	$$⊢\phi \to W\in X$$
Assertion	ldualsca	$$⊢\phi \to R=O$$

Proof

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