Metamath Proof Explorer


Theorem lfl1sc

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 )

Proof

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 )