Description: The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lcd1.h | |- H = ( LHyp ` K ) |
|
lcd1.u | |- U = ( ( DVecH ` K ) ` W ) |
||
lcd1.f | |- F = ( Scalar ` U ) |
||
lcd1.j | |- .1. = ( 1r ` F ) |
||
lcd1.c | |- C = ( ( LCDual ` K ) ` W ) |
||
lcd1.s | |- S = ( Scalar ` C ) |
||
lcd1.i | |- I = ( 1r ` S ) |
||
lcd1.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
Assertion | lcd1 | |- ( ph -> I = .1. ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcd1.h | |- H = ( LHyp ` K ) |
|
2 | lcd1.u | |- U = ( ( DVecH ` K ) ` W ) |
|
3 | lcd1.f | |- F = ( Scalar ` U ) |
|
4 | lcd1.j | |- .1. = ( 1r ` F ) |
|
5 | lcd1.c | |- C = ( ( LCDual ` K ) ` W ) |
|
6 | lcd1.s | |- S = ( Scalar ` C ) |
|
7 | lcd1.i | |- I = ( 1r ` S ) |
|
8 | lcd1.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
9 | eqid | |- ( oppR ` F ) = ( oppR ` F ) |
|
10 | 1 2 3 9 5 6 8 | lcdsca | |- ( ph -> S = ( oppR ` F ) ) |
11 | 10 | fveq2d | |- ( ph -> ( 1r ` S ) = ( 1r ` ( oppR ` F ) ) ) |
12 | 9 4 | oppr1 | |- .1. = ( 1r ` ( oppR ` F ) ) |
13 | 11 7 12 | 3eqtr4g | |- ( ph -> I = .1. ) |