Theorem mapdsn2

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

	Ref	Expression
Hypotheses	mapdsn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdsn.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	mapdsn.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdsn.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdsn.v	$$⊢V={\mathrm{Base}}_U$$
	mapdsn.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdsn.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	mapdsn.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	mapdsn.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdsn.x	$$⊢\phi \to X\in V$$
	mapdsn2.e	$$⊢\phi \to L\left(G\right)=O\left(\left\{X\right\}\right)$$
Assertion	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\}$$

Proof

Step	Hyp	Ref	Expression
1		mapdsn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdsn.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		mapdsn.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
4		mapdsn.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		mapdsn.v	$$⊢V={\mathrm{Base}}_U$$
6		mapdsn.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		mapdsn.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
8		mapdsn.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
9		mapdsn.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		mapdsn.x	$$⊢\phi \to X\in V$$
11		mapdsn2.e	$$⊢\phi \to L\left(G\right)=O\left(\left\{X\right\}\right)$$
12	1 2 3 4 5 6 7 8 9 10	mapdsn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=\left\{f\in F|O\left(\left\{X\right\}\right)\subseteq L\left(f\right)\right\}$$
13	11	sseq1d	$$⊢\phi \to \left(L\left(G\right)\subseteq L\left(f\right)\leftrightarrow O\left(\left\{X\right\}\right)\subseteq L\left(f\right)\right)$$
14	13	rabbidv	$$⊢\phi \to \left\{f\in F|L\left(G\right)\subseteq L\left(f\right)\right\}=\left\{f\in F|O\left(\left\{X\right\}\right)\subseteq L\left(f\right)\right\}$$
15	12 14	eqtr4d	$$⊢\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\}$$