Description: The (right vector space) scalar product of a functional with one is the functional. (Contributed by NM, 21-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lfl1sc.v | |- V = ( Base ` W ) |
|
lfl1sc.d | |- D = ( Scalar ` W ) |
||
lfl1sc.f | |- F = ( LFnl ` W ) |
||
lfl1sc.k | |- K = ( Base ` D ) |
||
lfl1sc.t | |- .x. = ( .r ` D ) |
||
lfl1sc.i | |- .1. = ( 1r ` D ) |
||
lfl1sc.w | |- ( ph -> W e. LMod ) |
||
lfl1sc.g | |- ( ph -> G e. F ) |
||
Assertion | lfl1sc | |- ( ph -> ( G oF .x. ( V X. { .1. } ) ) = G ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lfl1sc.v | |- V = ( Base ` W ) |
|
2 | lfl1sc.d | |- D = ( Scalar ` W ) |
|
3 | lfl1sc.f | |- F = ( LFnl ` W ) |
|
4 | lfl1sc.k | |- K = ( Base ` D ) |
|
5 | lfl1sc.t | |- .x. = ( .r ` D ) |
|
6 | lfl1sc.i | |- .1. = ( 1r ` D ) |
|
7 | lfl1sc.w | |- ( ph -> W e. LMod ) |
|
8 | lfl1sc.g | |- ( ph -> G e. F ) |
|
9 | 1 | fvexi | |- V e. _V |
10 | 9 | a1i | |- ( ph -> V e. _V ) |
11 | 2 4 1 3 | lflf | |- ( ( W e. LMod /\ G e. F ) -> G : V --> K ) |
12 | 7 8 11 | syl2anc | |- ( ph -> G : V --> K ) |
13 | 6 | fvexi | |- .1. e. _V |
14 | 13 | a1i | |- ( ph -> .1. e. _V ) |
15 | 2 | lmodring | |- ( W e. LMod -> D e. Ring ) |
16 | 7 15 | syl | |- ( ph -> D e. Ring ) |
17 | 4 5 6 | ringridm | |- ( ( D e. Ring /\ k e. K ) -> ( k .x. .1. ) = k ) |
18 | 16 17 | sylan | |- ( ( ph /\ k e. K ) -> ( k .x. .1. ) = k ) |
19 | 10 12 14 18 | caofid0r | |- ( ph -> ( G oF .x. ( V X. { .1. } ) ) = G ) |