Description: Connect the value of the preliminary map from vectors to functionals I to the hypothesis L used by earlier theorems. Note: the X e. ( V \ { .0. } ) hypothesis could be the more general X e. V but the former will be easier to use. TODO: use the I function directly in those theorems, so this theorem becomes unnecessary? TODO: The hdmap1cbv is probably unnecessary, but it would mean different $d's later on. (Contributed by NM, 15-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hdmap1valc.h | |- H = ( LHyp ` K ) |
|
| hdmap1valc.u | |- U = ( ( DVecH ` K ) ` W ) |
||
| hdmap1valc.v | |- V = ( Base ` U ) |
||
| hdmap1valc.s | |- .- = ( -g ` U ) |
||
| hdmap1valc.o | |- .0. = ( 0g ` U ) |
||
| hdmap1valc.n | |- N = ( LSpan ` U ) |
||
| hdmap1valc.c | |- C = ( ( LCDual ` K ) ` W ) |
||
| hdmap1valc.d | |- D = ( Base ` C ) |
||
| hdmap1valc.r | |- R = ( -g ` C ) |
||
| hdmap1valc.q | |- Q = ( 0g ` C ) |
||
| hdmap1valc.j | |- J = ( LSpan ` C ) |
||
| hdmap1valc.m | |- M = ( ( mapd ` K ) ` W ) |
||
| hdmap1valc.i | |- I = ( ( HDMap1 ` K ) ` W ) |
||
| hdmap1valc.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
| hdmap1valc.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
||
| hdmap1valc.f | |- ( ph -> F e. D ) |
||
| hdmap1valc.y | |- ( ph -> Y e. V ) |
||
| hdmap1valc.l | |- L = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) |
||
| Assertion | hdmap1valc | |- ( ph -> ( I ` <. X , F , Y >. ) = ( L ` <. X , F , Y >. ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hdmap1valc.h | |- H = ( LHyp ` K ) |
|
| 2 | hdmap1valc.u | |- U = ( ( DVecH ` K ) ` W ) |
|
| 3 | hdmap1valc.v | |- V = ( Base ` U ) |
|
| 4 | hdmap1valc.s | |- .- = ( -g ` U ) |
|
| 5 | hdmap1valc.o | |- .0. = ( 0g ` U ) |
|
| 6 | hdmap1valc.n | |- N = ( LSpan ` U ) |
|
| 7 | hdmap1valc.c | |- C = ( ( LCDual ` K ) ` W ) |
|
| 8 | hdmap1valc.d | |- D = ( Base ` C ) |
|
| 9 | hdmap1valc.r | |- R = ( -g ` C ) |
|
| 10 | hdmap1valc.q | |- Q = ( 0g ` C ) |
|
| 11 | hdmap1valc.j | |- J = ( LSpan ` C ) |
|
| 12 | hdmap1valc.m | |- M = ( ( mapd ` K ) ` W ) |
|
| 13 | hdmap1valc.i | |- I = ( ( HDMap1 ` K ) ` W ) |
|
| 14 | hdmap1valc.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
| 15 | hdmap1valc.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
|
| 16 | hdmap1valc.f | |- ( ph -> F e. D ) |
|
| 17 | hdmap1valc.y | |- ( ph -> Y e. V ) |
|
| 18 | hdmap1valc.l | |- L = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) |
|
| 19 | 15 | eldifad | |- ( ph -> X e. V ) |
| 20 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 19 16 17 | hdmap1val | |- ( ph -> ( I ` <. X , F , Y >. ) = if ( Y = .0. , Q , ( iota_ g e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { g } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R g ) } ) ) ) ) ) |
| 21 | 18 | hdmap1cbv | |- L = ( w e. _V |-> if ( ( 2nd ` w ) = .0. , Q , ( iota_ g e. D ( ( M ` ( N ` { ( 2nd ` w ) } ) ) = ( J ` { g } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` w ) ) .- ( 2nd ` w ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` w ) ) R g ) } ) ) ) ) ) |
| 22 | 10 21 19 16 17 | mapdhval | |- ( ph -> ( L ` <. X , F , Y >. ) = if ( Y = .0. , Q , ( iota_ g e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { g } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R g ) } ) ) ) ) ) |
| 23 | 20 22 | eqtr4d | |- ( ph -> ( I ` <. X , F , Y >. ) = ( L ` <. X , F , Y >. ) ) |