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 = ( LHyp ` K )
	mapd1dim2.u	|- U = ( ( DVecH ` K ) ` W )
	mapd1dim2.a	|- A = ( LSAtoms ` U )
	mapd1dim2.f	|- F = ( LFnl ` U )
	mapd1dim2.l	|- L = ( LKer ` U )
	mapd1dim2.o	|- O = ( ( ocH ` K ) ` W )
	mapd1dim2.m	|- M = ( ( mapd ` K ) ` W )
	mapd1dim2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapd1dim2.t	|- ( ph -> Q e. A )
Assertion	mapd1dim2lem1N	|- ( ph -> ( M ` Q ) = { f e. F | E. v e. Q ( O ` { v } ) = ( L ` f ) } )

Proof

Step	Hyp	Ref	Expression
1		mapd1dim2.h	|- H = ( LHyp ` K )
2		mapd1dim2.u	|- U = ( ( DVecH ` K ) ` W )
3		mapd1dim2.a	|- A = ( LSAtoms ` U )
4		mapd1dim2.f	|- F = ( LFnl ` U )
5		mapd1dim2.l	|- L = ( LKer ` U )
6		mapd1dim2.o	|- O = ( ( ocH ` K ) ` W )
7		mapd1dim2.m	|- M = ( ( mapd ` K ) ` W )
8		mapd1dim2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		mapd1dim2.t	|- ( ph -> Q e. A )
10		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
11	1 2 8	dvhlmod	|- ( ph -> U e. LMod )
12	10 3 11 9	lsatlssel	|- ( ph -> Q e. ( LSubSp ` U ) )
13	1 2 10 4 5 6 7 8 12	mapdval4N	|- ( ph -> ( M ` Q ) = { f e. F | E. v e. Q ( O ` { v } ) = ( L ` f ) } )