Theorem hdmap1val2

Description: Value of preliminary map from vectors to functionals in the closed kernel dual space, for nonzero Y . (Contributed by NM, 16-May-2015)

	Ref	Expression
Hypotheses	hdmap1val2.h	|- H = ( LHyp ` K )
	hdmap1val2.u	|- U = ( ( DVecH ` K ) ` W )
	hdmap1val2.v	|- V = ( Base ` U )
	hdmap1val2.s	|- .- = ( -g ` U )
	hdmap1val2.o	|- .0. = ( 0g ` U )
	hdmap1val2.n	|- N = ( LSpan ` U )
	hdmap1val2.c	|- C = ( ( LCDual ` K ) ` W )
	hdmap1val2.d	|- D = ( Base ` C )
	hdmap1val2.r	|- R = ( -g ` C )
	hdmap1val2.l	|- L = ( LSpan ` C )
	hdmap1val2.m	|- M = ( ( mapd ` K ) ` W )
	hdmap1val2.i	|- I = ( ( HDMap1 ` K ) ` W )
	hdmap1val2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmap1val2.x	|- ( ph -> X e. V )
	hdmap1val2.f	|- ( ph -> F e. D )
	hdmap1val2.y	|- ( ph -> Y e. ( V \ { .0. } ) )
Assertion	hdmap1val2	|- ( ph -> ( I ` <. X , F , Y >. ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap1val2.h	|- H = ( LHyp ` K )
2		hdmap1val2.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmap1val2.v	|- V = ( Base ` U )
4		hdmap1val2.s	|- .- = ( -g ` U )
5		hdmap1val2.o	|- .0. = ( 0g ` U )
6		hdmap1val2.n	|- N = ( LSpan ` U )
7		hdmap1val2.c	|- C = ( ( LCDual ` K ) ` W )
8		hdmap1val2.d	|- D = ( Base ` C )
9		hdmap1val2.r	|- R = ( -g ` C )
10		hdmap1val2.l	|- L = ( LSpan ` C )
11		hdmap1val2.m	|- M = ( ( mapd ` K ) ` W )
12		hdmap1val2.i	|- I = ( ( HDMap1 ` K ) ` W )
13		hdmap1val2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
14		hdmap1val2.x	|- ( ph -> X e. V )
15		hdmap1val2.f	|- ( ph -> F e. D )
16		hdmap1val2.y	|- ( ph -> Y e. ( V \ { .0. } ) )
17		eqid	|- ( 0g ` C ) = ( 0g ` C )
18	16	eldifad	|- ( ph -> Y e. V )
19	1 2 3 4 5 6 7 8 9 17 10 11 12 13 14 15 18	hdmap1val	|- ( ph -> ( I ` <. X , F , Y >. ) = if ( Y = .0. , ( 0g ` C ) , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) ) )
20		eldifsni	|- ( Y e. ( V \ { .0. } ) -> Y =/= .0. )
21	20	neneqd	|- ( Y e. ( V \ { .0. } ) -> -. Y = .0. )
22		iffalse	|- ( -. Y = .0. -> if ( Y = .0. , ( 0g ` C ) , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) )
23	16 21 22	3syl	|- ( ph -> if ( Y = .0. , ( 0g ` C ) , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) )
24	19 23	eqtrd	|- ( ph -> ( I ` <. X , F , Y >. ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( L ` { ( F R h ) } ) ) ) )