Theorem mapdsn3

Description: Value of the map defined by df-mapd at the span of a singleton. (Contributed by NM, 17-Feb-2015)

	Ref	Expression
Hypotheses	mapdsn3.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdsn3.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	mapdsn3.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdsn3.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdsn3.v	$$⊢V={\mathrm{Base}}_U$$
	mapdsn3.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdsn3.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	mapdsn3.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	mapdsn3.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	mapdsn3.p	$$⊢P=\mathrm{LSpan}\left(D\right)$$
	mapdsn3.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdsn3.x	$$⊢\phi \to X\in V$$
	mapdsn3.g	$$⊢\phi \to G\in F$$
	mapdsn3.e	$$⊢\phi \to L\left(G\right)=O\left(\left\{X\right\}\right)$$
Assertion	mapdsn3	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=P\left(\left\{G\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapdsn3.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdsn3.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		mapdsn3.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
4		mapdsn3.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		mapdsn3.v	$$⊢V={\mathrm{Base}}_U$$
6		mapdsn3.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		mapdsn3.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
8		mapdsn3.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
9		mapdsn3.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
10		mapdsn3.p	$$⊢P=\mathrm{LSpan}\left(D\right)$$
11		mapdsn3.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		mapdsn3.x	$$⊢\phi \to X\in V$$
13		mapdsn3.g	$$⊢\phi \to G\in F$$
14		mapdsn3.e	$$⊢\phi \to L\left(G\right)=O\left(\left\{X\right\}\right)$$
15	1 2 3 4 5 6 7 8 11 12 14	mapdsn2	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=\left\{f\in F|L\left(G\right)\subseteq L\left(f\right)\right\}$$
16	1 4 11	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
17	7 8 9 10 16 13	ldual1dim	$$⊢\phi \to P\left(\left\{G\right\}\right)=\left\{f\in F|L\left(G\right)\subseteq L\left(f\right)\right\}$$
18	15 17	eqtr4d	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=P\left(\left\{G\right\}\right)$$