Description: The zero scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lcd0.h | |- H = ( LHyp ` K ) |
|
lcd0.u | |- U = ( ( DVecH ` K ) ` W ) |
||
lcd0.f | |- F = ( Scalar ` U ) |
||
lcd0.z | |- .0. = ( 0g ` F ) |
||
lcd0.c | |- C = ( ( LCDual ` K ) ` W ) |
||
lcd0.s | |- S = ( Scalar ` C ) |
||
lcd0.o | |- O = ( 0g ` S ) |
||
lcd0.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
Assertion | lcd0 | |- ( ph -> O = .0. ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcd0.h | |- H = ( LHyp ` K ) |
|
2 | lcd0.u | |- U = ( ( DVecH ` K ) ` W ) |
|
3 | lcd0.f | |- F = ( Scalar ` U ) |
|
4 | lcd0.z | |- .0. = ( 0g ` F ) |
|
5 | lcd0.c | |- C = ( ( LCDual ` K ) ` W ) |
|
6 | lcd0.s | |- S = ( Scalar ` C ) |
|
7 | lcd0.o | |- O = ( 0g ` S ) |
|
8 | lcd0.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 -> ( 0g ` S ) = ( 0g ` ( oppR ` F ) ) ) |
12 | 9 4 | oppr0 | |- .0. = ( 0g ` ( oppR ` F ) ) |
13 | 11 7 12 | 3eqtr4g | |- ( ph -> O = .0. ) |