Metamath Proof Explorer

Theorem ldualvsdi1

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

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

Proof

Step Hyp Ref Expression
1 ldualvsdi1.f 
 |-  F = ( LFnl ` W )
2 ldualvsdi1.r 
 |-  R = ( Scalar ` W )
3 ldualvsdi1.k 
 |-  K = ( Base ` R )
4 ldualvsdi1.d 
 |-  D = ( LDual ` W )
5 ldualvsdi1.p 
 |-  .+ = ( +g ` D )
6 ldualvsdi1.s 
 |-  .x. = ( .s ` D )
7 ldualvsdi1.w 
 |-  ( ph -> W e. LMod )
8 ldualvsdi1.x 
 |-  ( ph -> X e. K )
9 ldualvsdi1.g 
 |-  ( ph -> G e. F )
10 ldualvsdi1.h 
 |-  ( ph -> H e. F )
11 eqid 
 |-  ( Base ` W ) = ( Base ` W )
12 eqid 
 |-  ( .r ` R ) = ( .r ` R )
13 1 11 2 3 12 4 6 7 8 9 ldualvs 
 |-  ( ph -> ( X .x. G ) = ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) )
14 1 11 2 3 12 4 6 7 8 10 ldualvs 
 |-  ( ph -> ( X .x. H ) = ( H oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) )
15 13 14 oveq12d 
 |-  ( ph -> ( ( X .x. G ) oF ( +g ` R ) ( X .x. H ) ) = ( ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) oF ( +g ` R ) ( H oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) ) )
16 eqid 
 |-  ( +g ` R ) = ( +g ` R )
17 1 2 3 4 6 7 8 9 ldualvscl 
 |-  ( ph -> ( X .x. G ) e. F )
18 1 2 3 4 6 7 8 10 ldualvscl 
 |-  ( ph -> ( X .x. H ) e. F )
19 1 2 16 4 5 7 17 18 ldualvadd 
 |-  ( ph -> ( ( X .x. G ) .+ ( X .x. H ) ) = ( ( X .x. G ) oF ( +g ` R ) ( X .x. H ) ) )
20 1 4 5 7 9 10 ldualvaddcl 
 |-  ( ph -> ( G .+ H ) e. F )
21 1 11 2 3 12 4 6 7 8 20 ldualvs 
 |-  ( ph -> ( X .x. ( G .+ H ) ) = ( ( G .+ H ) oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) )
22 1 2 16 4 5 7 9 10 ldualvadd 
 |-  ( ph -> ( G .+ H ) = ( G oF ( +g ` R ) H ) )
23 22 oveq1d 
 |-  ( ph -> ( ( G .+ H ) oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) = ( ( G oF ( +g ` R ) H ) oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) )
24 11 2 3 16 12 1 7 8 9 10 lflvsdi1 
 |-  ( ph -> ( ( G oF ( +g ` R ) H ) oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) = ( ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) oF ( +g ` R ) ( H oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) ) )
25 21 23 24 3eqtrd 
 |-  ( ph -> ( X .x. ( G .+ H ) ) = ( ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) oF ( +g ` R ) ( H oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) ) )
26 15 19 25 3eqtr4rd 
 |-  ( ph -> ( X .x. ( G .+ H ) ) = ( ( X .x. G ) .+ ( X .x. H ) ) )