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

Metamath Proof Explorer

Theorem ldualvaddcom

Description: Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015)

Ref Expression
Hypotheses ldualvaddcom.f 
|- F = ( LFnl ` W )
ldualvaddcom.d 
|- D = ( LDual ` W )
ldualvaddcom.p 
|- .+ = ( +g ` D )
ldualvaddcom.w 
|- ( ph -> W e. LMod )
ldualvaddcom.x 
|- ( ph -> X e. F )
ldualvaddcom.y 
|- ( ph -> Y e. F )
Assertion ldualvaddcom 
|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )

Proof

Step Hyp Ref Expression
1 ldualvaddcom.f 
 |-  F = ( LFnl ` W )
2 ldualvaddcom.d 
 |-  D = ( LDual ` W )
3 ldualvaddcom.p 
 |-  .+ = ( +g ` D )
4 ldualvaddcom.w 
 |-  ( ph -> W e. LMod )
5 ldualvaddcom.x 
 |-  ( ph -> X e. F )
6 ldualvaddcom.y 
 |-  ( ph -> Y e. F )
7 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
8 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
9 7 8 1 4 5 6 lfladdcom 
 |-  ( ph -> ( X oF ( +g ` ( Scalar ` W ) ) Y ) = ( Y oF ( +g ` ( Scalar ` W ) ) X ) )
10 1 7 8 2 3 4 5 6 ldualvadd 
 |-  ( ph -> ( X .+ Y ) = ( X oF ( +g ` ( Scalar ` W ) ) Y ) )
11 1 7 8 2 3 4 6 5 ldualvadd 
 |-  ( ph -> ( Y .+ X ) = ( Y oF ( +g ` ( Scalar ` W ) ) X ) )
12 9 10 11 3eqtr4d 
 |-  ( ph -> ( X .+ Y ) = ( Y .+ X ) )