Theorem ldual1dim

Description: Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014)

	Ref	Expression
Hypotheses	ldual1dim.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldual1dim.l	$$⊢L=\mathrm{LKer}\left(W\right)$$
	ldual1dim.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldual1dim.n	$$⊢N=\mathrm{LSpan}\left(D\right)$$
	ldual1dim.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	ldual1dim.g	$$⊢\phi \to G\in F$$
Assertion	ldual1dim	$$⊢\phi \to N\left(\left\{G\right\}\right)=\left\{g\in F|L\left(G\right)\subseteq L\left(g\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ldual1dim.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldual1dim.l	$$⊢L=\mathrm{LKer}\left(W\right)$$
3		ldual1dim.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
4		ldual1dim.n	$$⊢N=\mathrm{LSpan}\left(D\right)$$
5		ldual1dim.w	$$⊢\phi \to W\in \mathrm{LVec}$$
6		ldual1dim.g	$$⊢\phi \to G\in F$$
7		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
8		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
9		eqid	$$⊢\mathrm{Scalar}\left(D\right)=\mathrm{Scalar}\left(D\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
11	7 8 3 9 10 5	ldualsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
12	11	eleq2d	$$⊢\phi \to \left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\leftrightarrow k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)$$
13	12	anbi1d	$$⊢\phi \to \left(\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\wedge g=k{\cdot }_{D}G\right)\leftrightarrow \left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge g=k{\cdot }_{D}G\right)\right)$$
14		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
15		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(W\right)}={\cdot }_{\mathrm{Scalar}\left(W\right)}$$
16		eqid	$$⊢{\cdot }_D={\cdot }_D$$
17	5	adantr	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to W\in \mathrm{LVec}$$
18		simpr	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
19	6	adantr	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to G\in F$$
20	1 14 7 8 15 3 16 17 18 19	ldualvs	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to k{\cdot }_{D}G=G{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)$$
21	20	eqeq2d	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to \left(g=k{\cdot }_{D}G\leftrightarrow g=G{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)$$
22	21	pm5.32da	$$⊢\phi \to \left(\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge g=k{\cdot }_{D}G\right)\leftrightarrow \left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge g=G{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)\right)$$
23	13 22	bitrd	$$⊢\phi \to \left(\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\wedge g=k{\cdot }_{D}G\right)\leftrightarrow \left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge g=G{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)\right)$$
24	23	rexbidv2	$$⊢\phi \to \left(\exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}g=k{\cdot }_{D}G\leftrightarrow \exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}g=G{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right)$$
25	24	abbidv	$$⊢\phi \to \left\{g|\exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}g=k{\cdot }_{D}G\right\}=\left\{g|\exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}g=G{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right\}$$
26		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
27	3 26	lduallmod	$$⊢W\in \mathrm{LVec}\to D\in \mathrm{LMod}$$
28	5 27	syl	$$⊢\phi \to D\in \mathrm{LMod}$$
29		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
30	1 3 29 5 6	ldualelvbase	$$⊢\phi \to G\in {\mathrm{Base}}_D$$
31	9 10 29 16 4	lspsn	$$⊢\left(D\in \mathrm{LMod}\wedge G\in {\mathrm{Base}}_D\right)\to N\left(\left\{G\right\}\right)=\left\{g|\exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}g=k{\cdot }_{D}G\right\}$$
32	28 30 31	syl2anc	$$⊢\phi \to N\left(\left\{G\right\}\right)=\left\{g|\exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}g=k{\cdot }_{D}G\right\}$$
33	14 7 1 2 8 15 5 6	lfl1dim	$$⊢\phi \to \left\{g\in F|L\left(G\right)\subseteq L\left(g\right)\right\}=\left\{g|\exists k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}g=G{{\cdot }_{\mathrm{Scalar}\left(W\right)}}_f\left({\mathrm{Base}}_W\times \left\{k\right\}\right)\right\}$$
34	25 32 33	3eqtr4d	$$⊢\phi \to N\left(\left\{G\right\}\right)=\left\{g\in F|L\left(G\right)\subseteq L\left(g\right)\right\}$$