Metamath Proof Explorer


Theorem lflvsdi2

Description: Reverse 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 )
lfldi2.y
|- ( ph -> Y e. K )
lfldi2.g
|- ( ph -> G e. F )
Assertion lflvsdi2
|- ( ph -> ( G oF .x. ( ( V X. { X } ) oF .+ ( V X. { Y } ) ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( G oF .x. ( V X. { Y } ) ) ) )

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 lfldi2.y
 |-  ( ph -> Y e. K )
10 lfldi2.g
 |-  ( ph -> G e. F )
11 1 fvexi
 |-  V e. _V
12 11 a1i
 |-  ( ph -> V e. _V )
13 2 3 1 6 lflf
 |-  ( ( W e. LMod /\ G e. F ) -> G : V --> K )
14 7 10 13 syl2anc
 |-  ( ph -> G : V --> K )
15 fconst6g
 |-  ( X e. K -> ( V X. { X } ) : V --> K )
16 8 15 syl
 |-  ( ph -> ( V X. { X } ) : V --> K )
17 fconst6g
 |-  ( Y e. K -> ( V X. { Y } ) : V --> K )
18 9 17 syl
 |-  ( ph -> ( V X. { Y } ) : V --> K )
19 2 lmodring
 |-  ( W e. LMod -> R e. Ring )
20 7 19 syl
 |-  ( ph -> R e. Ring )
21 3 4 5 ringdi
 |-  ( ( R e. Ring /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
22 20 21 sylan
 |-  ( ( ph /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
23 12 14 16 18 22 caofdi
 |-  ( ph -> ( G oF .x. ( ( V X. { X } ) oF .+ ( V X. { Y } ) ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( G oF .x. ( V X. { Y } ) ) ) )