This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lfl0sc

Description: The (right vector space) scalar product of a functional with zero is the zero functional. Note that the first occurrence of ( V X. { .0. } ) represents the zero scalar, and the second is the zero functional. (Contributed by NM, 7-Oct-2014)

Ref Expression
Hypotheses lfl0sc.v 
|- V = ( Base ` W )
lfl0sc.d 
|- D = ( Scalar ` W )
lfl0sc.f 
|- F = ( LFnl ` W )
lfl0sc.k 
|- K = ( Base ` D )
lfl0sc.t 
|- .x. = ( .r ` D )
lfl0sc.o 
|- .0. = ( 0g ` D )
lfl0sc.w 
|- ( ph -> W e. LMod )
lfl0sc.g 
|- ( ph -> G e. F )
Assertion lfl0sc 
|- ( ph -> ( G oF .x. ( V X. { .0. } ) ) = ( V X. { .0. } ) )

Proof

Step Hyp Ref Expression
1 lfl0sc.v 
 |-  V = ( Base ` W )
2 lfl0sc.d 
 |-  D = ( Scalar ` W )
3 lfl0sc.f 
 |-  F = ( LFnl ` W )
4 lfl0sc.k 
 |-  K = ( Base ` D )
5 lfl0sc.t 
 |-  .x. = ( .r ` D )
6 lfl0sc.o 
 |-  .0. = ( 0g ` D )
7 lfl0sc.w 
 |-  ( ph -> W e. LMod )
8 lfl0sc.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 2 lmodring 
 |-  ( W e. LMod -> D e. Ring )
14 7 13 syl 
 |-  ( ph -> D e. Ring )
15 4 6 ring0cl 
 |-  ( D e. Ring -> .0. e. K )
16 14 15 syl 
 |-  ( ph -> .0. e. K )
17 4 5 6 ringrz 
 |-  ( ( D e. Ring /\ k e. K ) -> ( k .x. .0. ) = .0. )
18 14 17 sylan 
 |-  ( ( ph /\ k e. K ) -> ( k .x. .0. ) = .0. )
19 10 12 16 16 18 caofid1 
 |-  ( ph -> ( G oF .x. ( V X. { .0. } ) ) = ( V X. { .0. } ) )