Metamath Proof Explorer

Theorem lflsc0N

Description: The scalar product with the zero functional is the zero functional. (Contributed by NM, 7-Oct-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 lflsc0.v 
 |-  V = ( Base ` W )
2 lflsc0.d 
 |-  D = ( Scalar ` W )
3 lflsc0.k 
 |-  K = ( Base ` D )
4 lflsc0.t 
 |-  .x. = ( .r ` D )
5 lflsc0.o 
 |-  .0. = ( 0g ` D )
6 lflsc0.w 
 |-  ( ph -> W e. LMod )
7 lflsc0.x 
 |-  ( ph -> X e. K )
8 1 fvexi 
 |-  V e. _V
9 8 a1i 
 |-  ( ph -> V e. _V )
10 2 lmodring 
 |-  ( W e. LMod -> D e. Ring )
11 6 10 syl 
 |-  ( ph -> D e. Ring )
12 3 5 ring0cl 
 |-  ( D e. Ring -> .0. e. K )
13 11 12 syl 
 |-  ( ph -> .0. e. K )
14 9 13 7 ofc12 
 |-  ( ph -> ( ( V X. { .0. } ) oF .x. ( V X. { X } ) ) = ( V X. { ( .0. .x. X ) } ) )
15 3 4 5 ringlz 
 |-  ( ( D e. Ring /\ X e. K ) -> ( .0. .x. X ) = .0. )
16 11 7 15 syl2anc 
 |-  ( ph -> ( .0. .x. X ) = .0. )
17 16 sneqd 
 |-  ( ph -> { ( .0. .x. X ) } = { .0. } )
18 17 xpeq2d 
 |-  ( ph -> ( V X. { ( .0. .x. X ) } ) = ( V X. { .0. } ) )
19 14 18 eqtrd 
 |-  ( ph -> ( ( V X. { .0. } ) oF .x. ( V X. { X } ) ) = ( V X. { .0. } ) )