Theorem ldualvaddval

Description: The value of the value of vector addition in the dual of a vector space. (Contributed by NM, 7-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ldualvaddval.v	|- V = ( Base ` W )
2		ldualvaddval.r	|- R = ( Scalar ` W )
3		ldualvaddval.a	|- .+ = ( +g ` R )
4		ldualvaddval.f	|- F = ( LFnl ` W )
5		ldualvaddval.d	|- D = ( LDual ` W )
6		ldualvaddval.p	|- .+b = ( +g ` D )
7		ldualvaddval.w	|- ( ph -> W e. LMod )
8		ldualvaddval.g	|- ( ph -> G e. F )
9		ldualvaddval.h	|- ( ph -> H e. F )
10		ldualvaddval.x	|- ( ph -> X e. V )
11	4 2 3 5 6 7 8 9	ldualvadd	|- ( ph -> ( G .+b H ) = ( G oF .+ H ) )
12	11	fveq1d	|- ( ph -> ( ( G .+b H ) ` X ) = ( ( G oF .+ H ) ` X ) )
13		eqid	|- ( Base ` R ) = ( Base ` R )
14	2 13 1 4	lflf	|- ( ( W e. LMod /\ G e. F ) -> G : V --> ( Base ` R ) )
15	14	ffnd	|- ( ( W e. LMod /\ G e. F ) -> G Fn V )
16	7 8 15	syl2anc	|- ( ph -> G Fn V )
17	2 13 1 4	lflf	|- ( ( W e. LMod /\ H e. F ) -> H : V --> ( Base ` R ) )
18	17	ffnd	|- ( ( W e. LMod /\ H e. F ) -> H Fn V )
19	7 9 18	syl2anc	|- ( ph -> H Fn V )
20	1	fvexi	|- V e. _V
21	20	a1i	|- ( ph -> V e. _V )
22		inidm	|- ( V i^i V ) = V
23		eqidd	|- ( ( ph /\ X e. V ) -> ( G ` X ) = ( G ` X ) )
24		eqidd	|- ( ( ph /\ X e. V ) -> ( H ` X ) = ( H ` X ) )
25	16 19 21 21 22 23 24	ofval	|- ( ( ph /\ X e. V ) -> ( ( G oF .+ H ) ` X ) = ( ( G ` X ) .+ ( H ` X ) ) )
26	10 25	mpdan	|- ( ph -> ( ( G oF .+ H ) ` X ) = ( ( G ` X ) .+ ( H ` X ) ) )
27	12 26	eqtrd	|- ( ph -> ( ( G .+b H ) ` X ) = ( ( G ` X ) .+ ( H ` X ) ) )