Metamath Proof Explorer

Theorem lflvsdi1

Description: Distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014)

Ref Expression
Hypotheses lfldi.v 
|- V = ( Base ` W )
lfldi.r 
|- R = ( Scalar ` W )
lfldi.k 
|- K = ( Base ` R )
lfldi.p 
|- .+ = ( +g ` R )
lfldi.t 
|- .x. = ( .r ` R )
lfldi.f 
|- F = ( LFnl ` W )
lfldi.w 
|- ( ph -> W e. LMod )
lfldi.x 
|- ( ph -> X e. K )
lfldi1.g 
|- ( ph -> G e. F )
lfldi1.h 
|- ( ph -> H e. F )
Assertion lflvsdi1 
|- ( ph -> ( ( G oF .+ H ) oF .x. ( V X. { X } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( H oF .x. ( V X. { X } ) ) ) )

Proof

Step Hyp Ref Expression
1 lfldi.v 
 |-  V = ( Base ` W )
2 lfldi.r 
 |-  R = ( Scalar ` W )
3 lfldi.k 
 |-  K = ( Base ` R )
4 lfldi.p 
 |-  .+ = ( +g ` R )
5 lfldi.t 
 |-  .x. = ( .r ` R )
6 lfldi.f 
 |-  F = ( LFnl ` W )
7 lfldi.w 
 |-  ( ph -> W e. LMod )
8 lfldi.x 
 |-  ( ph -> X e. K )
9 lfldi1.g 
 |-  ( ph -> G e. F )
10 lfldi1.h 
 |-  ( ph -> H e. F )
11 1 fvexi 
 |-  V e. _V
12 11 a1i 
 |-  ( ph -> V e. _V )
13 fconst6g 
 |-  ( X e. K -> ( V X. { X } ) : V --> K )
14 8 13 syl 
 |-  ( ph -> ( V X. { X } ) : V --> K )
15 2 3 1 6 lflf 
 |-  ( ( W e. LMod /\ G e. F ) -> G : V --> K )
16 7 9 15 syl2anc 
 |-  ( ph -> G : V --> K )
17 2 3 1 6 lflf 
 |-  ( ( W e. LMod /\ H e. F ) -> H : V --> K )
18 7 10 17 syl2anc 
 |-  ( ph -> H : V --> K )
19 2 lmodring 
 |-  ( W e. LMod -> R e. Ring )
20 7 19 syl 
 |-  ( ph -> R e. Ring )
21 3 4 5 ringdir 
 |-  ( ( R e. Ring /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
22 20 21 sylan 
 |-  ( ( ph /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
23 12 14 16 18 22 caofdir 
 |-  ( ph -> ( ( G oF .+ H ) oF .x. ( V X. { X } ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( H oF .x. ( V X. { X } ) ) ) )