Theorem lcdvaddval

Description: The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015)

	Ref	Expression
Hypotheses	lcdvaddval.h	|- H = ( LHyp ` K )
	lcdvaddval.u	|- U = ( ( DVecH ` K ) ` W )
	lcdvaddval.v	|- V = ( Base ` U )
	lcdvaddval.r	|- R = ( Scalar ` U )
	lcdvaddval.a	|- .+ = ( +g ` R )
	lcdvaddval.c	|- C = ( ( LCDual ` K ) ` W )
	lcdvaddval.d	|- D = ( Base ` C )
	lcdvaddval.p	|- .+b = ( +g ` C )
	lcdvaddval.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcdvaddval.f	|- ( ph -> F e. D )
	lcdvaddval.g	|- ( ph -> G e. D )
	lcdvaddval.x	|- ( ph -> X e. V )
Assertion	lcdvaddval	|- ( ph -> ( ( F .+b G ) ` X ) = ( ( F ` X ) .+ ( G ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcdvaddval.h	|- H = ( LHyp ` K )
2		lcdvaddval.u	|- U = ( ( DVecH ` K ) ` W )
3		lcdvaddval.v	|- V = ( Base ` U )
4		lcdvaddval.r	|- R = ( Scalar ` U )
5		lcdvaddval.a	|- .+ = ( +g ` R )
6		lcdvaddval.c	|- C = ( ( LCDual ` K ) ` W )
7		lcdvaddval.d	|- D = ( Base ` C )
8		lcdvaddval.p	|- .+b = ( +g ` C )
9		lcdvaddval.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		lcdvaddval.f	|- ( ph -> F e. D )
11		lcdvaddval.g	|- ( ph -> G e. D )
12		lcdvaddval.x	|- ( ph -> X e. V )
13		eqid	|- ( LDual ` U ) = ( LDual ` U )
14		eqid	|- ( +g ` ( LDual ` U ) ) = ( +g ` ( LDual ` U ) )
15	1 2 13 14 6 8 9	lcdvadd	|- ( ph -> .+b = ( +g ` ( LDual ` U ) ) )
16	15	oveqd	|- ( ph -> ( F .+b G ) = ( F ( +g ` ( LDual ` U ) ) G ) )
17	16	fveq1d	|- ( ph -> ( ( F .+b G ) ` X ) = ( ( F ( +g ` ( LDual ` U ) ) G ) ` X ) )
18		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
19	1 2 9	dvhlmod	|- ( ph -> U e. LMod )
20	1 6 7 2 18 9 10	lcdvbaselfl	|- ( ph -> F e. ( LFnl ` U ) )
21	1 6 7 2 18 9 11	lcdvbaselfl	|- ( ph -> G e. ( LFnl ` U ) )
22	3 4 5 18 13 14 19 20 21 12	ldualvaddval	|- ( ph -> ( ( F ( +g ` ( LDual ` U ) ) G ) ` X ) = ( ( F ` X ) .+ ( G ` X ) ) )
23	17 22	eqtrd	|- ( ph -> ( ( F .+b G ) ` X ) = ( ( F ` X ) .+ ( G ` X ) ) )