Theorem mapdhvmap

Description: Relationship between mapd and HVMap , which can be used to satisfy the last hypothesis of mapdpg . Equation 10 of Baer p. 48. (Contributed by NM, 29-Mar-2015)

	Ref	Expression
Hypotheses	mapdhvmap.h	|- H = ( LHyp ` K )
	mapdhvmap.u	|- U = ( ( DVecH ` K ) ` W )
	mapdhvmap.v	|- V = ( Base ` U )
	mapdhvmap.z	|- .0. = ( 0g ` U )
	mapdhvmap.n	|- N = ( LSpan ` U )
	mapdhvmap.c	|- C = ( ( LCDual ` K ) ` W )
	mapdhvmap.j	|- J = ( LSpan ` C )
	mapdhvmap.m	|- M = ( ( mapd ` K ) ` W )
	mapdhvmap.p	|- P = ( ( HVMap ` K ) ` W )
	mapdhvmap.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdhvmap.x	|- ( ph -> X e. ( V \ { .0. } ) )
Assertion	mapdhvmap	|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { ( P ` X ) } ) )

Proof

Step	Hyp	Ref	Expression
1		mapdhvmap.h	|- H = ( LHyp ` K )
2		mapdhvmap.u	|- U = ( ( DVecH ` K ) ` W )
3		mapdhvmap.v	|- V = ( Base ` U )
4		mapdhvmap.z	|- .0. = ( 0g ` U )
5		mapdhvmap.n	|- N = ( LSpan ` U )
6		mapdhvmap.c	|- C = ( ( LCDual ` K ) ` W )
7		mapdhvmap.j	|- J = ( LSpan ` C )
8		mapdhvmap.m	|- M = ( ( mapd ` K ) ` W )
9		mapdhvmap.p	|- P = ( ( HVMap ` K ) ` W )
10		mapdhvmap.k	|- ( ph -> ( K e. HL /\ W e. H ) )
11		mapdhvmap.x	|- ( ph -> X e. ( V \ { .0. } ) )
12		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
13		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
14		eqid	|- ( LKer ` U ) = ( LKer ` U )
15		eqid	|- ( LDual ` U ) = ( LDual ` U )
16		eqid	|- ( LSpan ` ( LDual ` U ) ) = ( LSpan ` ( LDual ` U ) )
17	11	eldifad	|- ( ph -> X e. V )
18	1 2 3 4 13 9 10 11	hvmaplfl	|- ( ph -> ( P ` X ) e. ( LFnl ` U ) )
19	1 12 2 3 4 14 9 10 11	hvmaplkr	|- ( ph -> ( ( LKer ` U ) ` ( P ` X ) ) = ( ( ( ocH ` K ) ` W ) ` { X } ) )
20	1 12 8 2 3 5 13 14 15 16 10 17 18 19	mapdsn3	|- ( ph -> ( M ` ( N ` { X } ) ) = ( ( LSpan ` ( LDual ` U ) ) ` { ( P ` X ) } ) )
21		eqid	|- ( Base ` C ) = ( Base ` C )
22		eqid	|- ( 0g ` C ) = ( 0g ` C )
23	1 2 3 4 6 21 22 9 10 11	hvmapcl2	|- ( ph -> ( P ` X ) e. ( ( Base ` C ) \ { ( 0g ` C ) } ) )
24	23	eldifad	|- ( ph -> ( P ` X ) e. ( Base ` C ) )
25	24	snssd	|- ( ph -> { ( P ` X ) } C_ ( Base ` C ) )
26	1 2 15 16 6 21 7 10 25	lcdlsp	|- ( ph -> ( J ` { ( P ` X ) } ) = ( ( LSpan ` ( LDual ` U ) ) ` { ( P ` X ) } ) )
27	20 26	eqtr4d	|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { ( P ` X ) } ) )