Description: Base set of scalar ring for the closed kernel dual of a vector space. (Contributed by NM, 18-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lcdsbase.h | |- H = ( LHyp ` K ) |
|
lcdsbase.u | |- U = ( ( DVecH ` K ) ` W ) |
||
lcdsbase.f | |- F = ( Scalar ` U ) |
||
lcdsbase.l | |- L = ( Base ` F ) |
||
lcdsbase.c | |- C = ( ( LCDual ` K ) ` W ) |
||
lcdsbase.s | |- S = ( Scalar ` C ) |
||
lcdsbase.r | |- R = ( Base ` S ) |
||
lcdsbase.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
Assertion | lcdsbase | |- ( ph -> R = L ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcdsbase.h | |- H = ( LHyp ` K ) |
|
2 | lcdsbase.u | |- U = ( ( DVecH ` K ) ` W ) |
|
3 | lcdsbase.f | |- F = ( Scalar ` U ) |
|
4 | lcdsbase.l | |- L = ( Base ` F ) |
|
5 | lcdsbase.c | |- C = ( ( LCDual ` K ) ` W ) |
|
6 | lcdsbase.s | |- S = ( Scalar ` C ) |
|
7 | lcdsbase.r | |- R = ( Base ` S ) |
|
8 | lcdsbase.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 -> ( Base ` S ) = ( Base ` ( oppR ` F ) ) ) |
12 | 9 4 | opprbas | |- L = ( Base ` ( oppR ` F ) ) |
13 | 11 7 12 | 3eqtr4g | |- ( ph -> R = L ) |