Description: The value of vector addition in the dual of a vector space is a functional. (Contributed by NM, 21-Oct-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ldualvaddcl.f | |- F = ( LFnl ` W ) |
|
| ldualvaddcl.d | |- D = ( LDual ` W ) |
||
| ldualvaddcl.p | |- .+ = ( +g ` D ) |
||
| ldualvaddcl.w | |- ( ph -> W e. LMod ) |
||
| ldualvaddcl.g | |- ( ph -> G e. F ) |
||
| ldualvaddcl.h | |- ( ph -> H e. F ) |
||
| Assertion | ldualvaddcl | |- ( ph -> ( G .+ H ) e. F ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ldualvaddcl.f | |- F = ( LFnl ` W ) |
|
| 2 | ldualvaddcl.d | |- D = ( LDual ` W ) |
|
| 3 | ldualvaddcl.p | |- .+ = ( +g ` D ) |
|
| 4 | ldualvaddcl.w | |- ( ph -> W e. LMod ) |
|
| 5 | ldualvaddcl.g | |- ( ph -> G e. F ) |
|
| 6 | ldualvaddcl.h | |- ( ph -> H e. F ) |
|
| 7 | eqid | |- ( Scalar ` W ) = ( Scalar ` W ) |
|
| 8 | eqid | |- ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) ) |
|
| 9 | 1 7 8 2 3 4 5 6 | ldualvadd | |- ( ph -> ( G .+ H ) = ( G oF ( +g ` ( Scalar ` W ) ) H ) ) |
| 10 | 7 8 1 4 5 6 | lfladdcl | |- ( ph -> ( G oF ( +g ` ( Scalar ` W ) ) H ) e. F ) |
| 11 | 9 10 | eqeltrd | |- ( ph -> ( G .+ H ) e. F ) |