Theorem hdmap1eu

Description: Convert mapdh9a to use the HDMap1 notation. (Contributed by NM, 15-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		hdmap1eu.h	|- H = ( LHyp ` K )
2		hdmap1eu.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmap1eu.v	|- V = ( Base ` U )
4		hdmap1eu.o	|- .0. = ( 0g ` U )
5		hdmap1eu.n	|- N = ( LSpan ` U )
6		hdmap1eu.c	|- C = ( ( LCDual ` K ) ` W )
7		hdmap1eu.d	|- D = ( Base ` C )
8		hdmap1eu.l	|- L = ( LSpan ` C )
9		hdmap1eu.m	|- M = ( ( mapd ` K ) ` W )
10		hdmap1eu.i	|- I = ( ( HDMap1 ` K ) ` W )
11		hdmap1eu.k	|- ( ph -> ( K e. HL /\ W e. H ) )
12		hdmap1eu.mn	|- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )
13		hdmap1eu.x	|- ( ph -> X e. ( V \ { .0. } ) )
14		hdmap1eu.f	|- ( ph -> F e. D )
15		hdmap1eu.t	|- ( ph -> T e. V )
16		eqid	|- ( -g ` U ) = ( -g ` U )
17		eqid	|- ( -g ` C ) = ( -g ` C )
18		eqid	|- ( 0g ` C ) = ( 0g ` C )
19		eqid	|- ( x e. _V |-> if ( ( 2nd ` x ) = .0. , ( 0g ` C ) , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` U ) ( 2nd ` x ) ) } ) ) = ( L ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` C ) h ) } ) ) ) ) ) = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , ( 0g ` C ) , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` U ) ( 2nd ` x ) ) } ) ) = ( L ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` C ) h ) } ) ) ) ) )
20	19	hdmap1cbv	|- ( x e. _V |-> if ( ( 2nd ` x ) = .0. , ( 0g ` C ) , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( L ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) ( -g ` U ) ( 2nd ` x ) ) } ) ) = ( L ` { ( ( 2nd ` ( 1st ` x ) ) ( -g ` C ) h ) } ) ) ) ) ) = ( w e. _V |-> if ( ( 2nd ` w ) = .0. , ( 0g ` C ) , ( iota_ g e. D ( ( M ` ( N ` { ( 2nd ` w ) } ) ) = ( L ` { g } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` w ) ) ( -g ` U ) ( 2nd ` w ) ) } ) ) = ( L ` { ( ( 2nd ` ( 1st ` w ) ) ( -g ` C ) g ) } ) ) ) ) )
21	1 2 3 16 4 5 6 7 17 18 8 9 10 11 12 13 14 15 20	hdmap1eulem	|- ( ph -> E! y e. D A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )