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 = ( LHyp ` K )
	mapdsn3.o	|- O = ( ( ocH ` K ) ` W )
	mapdsn3.m	|- M = ( ( mapd ` K ) ` W )
	mapdsn3.u	|- U = ( ( DVecH ` K ) ` W )
	mapdsn3.v	|- V = ( Base ` U )
	mapdsn3.n	|- N = ( LSpan ` U )
	mapdsn3.f	|- F = ( LFnl ` U )
	mapdsn3.l	|- L = ( LKer ` U )
	mapdsn3.d	|- D = ( LDual ` U )
	mapdsn3.p	|- P = ( LSpan ` D )
	mapdsn3.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdsn3.x	|- ( ph -> X e. V )
	mapdsn3.g	|- ( ph -> G e. F )
	mapdsn3.e	|- ( ph -> ( L ` G ) = ( O ` { X } ) )
Assertion	mapdsn3	|- ( ph -> ( M ` ( N ` { X } ) ) = ( P ` { G } ) )

Proof

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