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

Metamath Proof Explorer

Theorem ldualvsdi2

Description: Reverse distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014)

Ref Expression
Hypotheses ldualvsdi2.f 
|- F = ( LFnl ` W )
ldualvsdi2.r 
|- R = ( Scalar ` W )
ldualvsdi2.a 
|- .+ = ( +g ` R )
ldualvsdi2.k 
|- K = ( Base ` R )
ldualvsdi2.d 
|- D = ( LDual ` W )
ldualvsdi2.p 
|- .+b = ( +g ` D )
ldualvsdi2.s 
|- .x. = ( .s ` D )
ldualvsdi2.w 
|- ( ph -> W e. LMod )
ldualvsdi2.x 
|- ( ph -> X e. K )
ldualvsdi2.y 
|- ( ph -> Y e. K )
ldualvsdi2.g 
|- ( ph -> G e. F )
Assertion ldualvsdi2 
|- ( ph -> ( ( X .+ Y ) .x. G ) = ( ( X .x. G ) .+b ( Y .x. G ) ) )

Proof

Step Hyp Ref Expression
1 ldualvsdi2.f 
 |-  F = ( LFnl ` W )
2 ldualvsdi2.r 
 |-  R = ( Scalar ` W )
3 ldualvsdi2.a 
 |-  .+ = ( +g ` R )
4 ldualvsdi2.k 
 |-  K = ( Base ` R )
5 ldualvsdi2.d 
 |-  D = ( LDual ` W )
6 ldualvsdi2.p 
 |-  .+b = ( +g ` D )
7 ldualvsdi2.s 
 |-  .x. = ( .s ` D )
8 ldualvsdi2.w 
 |-  ( ph -> W e. LMod )
9 ldualvsdi2.x 
 |-  ( ph -> X e. K )
10 ldualvsdi2.y 
 |-  ( ph -> Y e. K )
11 ldualvsdi2.g 
 |-  ( ph -> G e. F )
12 eqid 
 |-  ( Base ` W ) = ( Base ` W )
13 eqid 
 |-  ( .r ` R ) = ( .r ` R )
14 2 4 3 lmodacl 
 |-  ( ( W e. LMod /\ X e. K /\ Y e. K ) -> ( X .+ Y ) e. K )
15 8 9 10 14 syl3anc 
 |-  ( ph -> ( X .+ Y ) e. K )
16 1 12 2 4 13 5 7 8 15 11 ldualvs 
 |-  ( ph -> ( ( X .+ Y ) .x. G ) = ( G oF ( .r ` R ) ( ( Base ` W ) X. { ( X .+ Y ) } ) ) )
17 12 2 4 3 13 1 8 9 10 11 lflvsdi2a 
 |-  ( ph -> ( G oF ( .r ` R ) ( ( Base ` W ) X. { ( X .+ Y ) } ) ) = ( ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) oF .+ ( G oF ( .r ` R ) ( ( Base ` W ) X. { Y } ) ) ) )
18 1 2 4 5 7 8 9 11 ldualvscl 
 |-  ( ph -> ( X .x. G ) e. F )
19 1 2 4 5 7 8 10 11 ldualvscl 
 |-  ( ph -> ( Y .x. G ) e. F )
20 1 2 3 5 6 8 18 19 ldualvadd 
 |-  ( ph -> ( ( X .x. G ) .+b ( Y .x. G ) ) = ( ( X .x. G ) oF .+ ( Y .x. G ) ) )
21 1 12 2 4 13 5 7 8 9 11 ldualvs 
 |-  ( ph -> ( X .x. G ) = ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) )
22 1 12 2 4 13 5 7 8 10 11 ldualvs 
 |-  ( ph -> ( Y .x. G ) = ( G oF ( .r ` R ) ( ( Base ` W ) X. { Y } ) ) )
23 21 22 oveq12d 
 |-  ( ph -> ( ( X .x. G ) oF .+ ( Y .x. G ) ) = ( ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) oF .+ ( G oF ( .r ` R ) ( ( Base ` W ) X. { Y } ) ) ) )
24 20 23 eqtr2d 
 |-  ( ph -> ( ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) oF .+ ( G oF ( .r ` R ) ( ( Base ` W ) X. { Y } ) ) ) = ( ( X .x. G ) .+b ( Y .x. G ) ) )
25 16 17 24 3eqtrd 
 |-  ( ph -> ( ( X .+ Y ) .x. G ) = ( ( X .x. G ) .+b ( Y .x. G ) ) )