Theorem hdmap1val0

Description: Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 .) (Contributed by NM, 17-May-2015)

	Ref	Expression
Hypotheses	hdmap1val0.h	|- H = ( LHyp ` K )
	hdmap1val0.u	|- U = ( ( DVecH ` K ) ` W )
	hdmap1val0.v	|- V = ( Base ` U )
	hdmap1val0.o	|- .0. = ( 0g ` U )
	hdmap1val0.c	|- C = ( ( LCDual ` K ) ` W )
	hdmap1val0.d	|- D = ( Base ` C )
	hdmap1val0.q	|- Q = ( 0g ` C )
	hdmap1val0.s	|- I = ( ( HDMap1 ` K ) ` W )
	hdmap1val0.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmap1val0.f	|- ( ph -> F e. D )
	hdmap1val0.x	|- ( ph -> X e. V )
Assertion	hdmap1val0	|- ( ph -> ( I ` <. X , F , .0. >. ) = Q )

Proof

Step	Hyp	Ref	Expression
1		hdmap1val0.h	|- H = ( LHyp ` K )
2		hdmap1val0.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmap1val0.v	|- V = ( Base ` U )
4		hdmap1val0.o	|- .0. = ( 0g ` U )
5		hdmap1val0.c	|- C = ( ( LCDual ` K ) ` W )
6		hdmap1val0.d	|- D = ( Base ` C )
7		hdmap1val0.q	|- Q = ( 0g ` C )
8		hdmap1val0.s	|- I = ( ( HDMap1 ` K ) ` W )
9		hdmap1val0.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		hdmap1val0.f	|- ( ph -> F e. D )
11		hdmap1val0.x	|- ( ph -> X e. V )
12		eqid	|- ( -g ` U ) = ( -g ` U )
13		eqid	|- ( LSpan ` U ) = ( LSpan ` U )
14		eqid	|- ( -g ` C ) = ( -g ` C )
15		eqid	|- ( LSpan ` C ) = ( LSpan ` C )
16		eqid	|- ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )
17	1 2 9	dvhlmod	|- ( ph -> U e. LMod )
18	3 4	lmod0vcl	|- ( U e. LMod -> .0. e. V )
19	17 18	syl	|- ( ph -> .0. e. V )
20	1 2 3 12 4 13 5 6 14 7 15 16 8 9 11 10 19	hdmap1val	|- ( ph -> ( I ` <. X , F , .0. >. ) = if ( .0. = .0. , Q , ( iota_ h e. D ( ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { .0. } ) ) = ( ( LSpan ` C ) ` { h } ) /\ ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { ( X ( -g ` U ) .0. ) } ) ) = ( ( LSpan ` C ) ` { ( F ( -g ` C ) h ) } ) ) ) ) )
21		eqid	|- .0. = .0.
22	21	iftruei	|- if ( .0. = .0. , Q , ( iota_ h e. D ( ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { .0. } ) ) = ( ( LSpan ` C ) ` { h } ) /\ ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { ( X ( -g ` U ) .0. ) } ) ) = ( ( LSpan ` C ) ` { ( F ( -g ` C ) h ) } ) ) ) ) = Q
23	20 22	eqtrdi	|- ( ph -> ( I ` <. X , F , .0. >. ) = Q )