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

Metamath Proof Explorer

Theorem ldualvadd

Description: Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014)

Ref Expression
Hypotheses ldualvadd.f 
|- F = ( LFnl ` W )
ldualvadd.r 
|- R = ( Scalar ` W )
ldualvadd.a 
|- .+ = ( +g ` R )
ldualvadd.d 
|- D = ( LDual ` W )
ldualvadd.p 
|- .+b = ( +g ` D )
ldualvadd.w 
|- ( ph -> W e. X )
ldualvadd.g 
|- ( ph -> G e. F )
ldualvadd.h 
|- ( ph -> H e. F )
Assertion ldualvadd 
|- ( ph -> ( G .+b H ) = ( G oF .+ H ) )

Proof

Step Hyp Ref Expression
1 ldualvadd.f 
 |-  F = ( LFnl ` W )
2 ldualvadd.r 
 |-  R = ( Scalar ` W )
3 ldualvadd.a 
 |-  .+ = ( +g ` R )
4 ldualvadd.d 
 |-  D = ( LDual ` W )
5 ldualvadd.p 
 |-  .+b = ( +g ` D )
6 ldualvadd.w 
 |-  ( ph -> W e. X )
7 ldualvadd.g 
 |-  ( ph -> G e. F )
8 ldualvadd.h 
 |-  ( ph -> H e. F )
9 eqid 
 |-  ( oF .+ |` ( F X. F ) ) = ( oF .+ |` ( F X. F ) )
10 1 2 3 4 5 6 9 ldualfvadd 
 |-  ( ph -> .+b = ( oF .+ |` ( F X. F ) ) )
11 10 oveqd 
 |-  ( ph -> ( G .+b H ) = ( G ( oF .+ |` ( F X. F ) ) H ) )
12 7 8 ofmresval 
 |-  ( ph -> ( G ( oF .+ |` ( F X. F ) ) H ) = ( G oF .+ H ) )
13 11 12 eqtrd 
 |-  ( ph -> ( G .+b H ) = ( G oF .+ H ) )