Theorem mapd1dim2lem1N

Description: Value of the map defined by df-mapd at an atom. (Contributed by NM, 10-Feb-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapd1dim2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapd1dim2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapd1dim2.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	mapd1dim2.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	mapd1dim2.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	mapd1dim2.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	mapd1dim2.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapd1dim2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapd1dim2.t	$$⊢\phi \to Q\in A$$
Assertion	mapd1dim2lem1N	$$⊢\phi \to M\left(Q\right)=\left\{f\in F|\exists v\in QO\left(\left\{v\right\}\right)=L\left(f\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mapd1dim2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapd1dim2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		mapd1dim2.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
4		mapd1dim2.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
5		mapd1dim2.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
6		mapd1dim2.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
7		mapd1dim2.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
8		mapd1dim2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		mapd1dim2.t	$$⊢\phi \to Q\in A$$
10		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
11	1 2 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
12	10 3 11 9	lsatlssel	$$⊢\phi \to Q\in \mathrm{LSubSp}\left(U\right)$$
13	1 2 10 4 5 6 7 8 12	mapdval4N	$$⊢\phi \to M\left(Q\right)=\left\{f\in F|\exists v\in QO\left(\left\{v\right\}\right)=L\left(f\right)\right\}$$