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 ) )