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=\mathrm{LHyp}\left(K\right)$$
	lcdvaddval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdvaddval.v	$$⊢V={\mathrm{Base}}_U$$
	lcdvaddval.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	lcdvaddval.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	lcdvaddval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdvaddval.d	$$⊢D={\mathrm{Base}}_C$$
	lcdvaddval.p	$$⊢\underset{\dot{}}{✚}={+}_C$$
	lcdvaddval.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcdvaddval.f	$$⊢\phi \to F\in D$$
	lcdvaddval.g	$$⊢\phi \to G\in D$$
	lcdvaddval.x	$$⊢\phi \to X\in V$$
Assertion	lcdvaddval	$$⊢\phi \to \left(F\underset{\dot{}}{✚}G\right)\left(X\right)=F\left(X\right)\underset{\dot{}}{+}G\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcdvaddval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdvaddval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdvaddval.v	$$⊢V={\mathrm{Base}}_U$$
4		lcdvaddval.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
5		lcdvaddval.a	$$⊢\underset{\dot{}}{+}={+}_R$$
6		lcdvaddval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
7		lcdvaddval.d	$$⊢D={\mathrm{Base}}_C$$
8		lcdvaddval.p	$$⊢\underset{\dot{}}{✚}={+}_C$$
9		lcdvaddval.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		lcdvaddval.f	$$⊢\phi \to F\in D$$
11		lcdvaddval.g	$$⊢\phi \to G\in D$$
12		lcdvaddval.x	$$⊢\phi \to X\in V$$
13		eqid	$$⊢\mathrm{LDual}\left(U\right)=\mathrm{LDual}\left(U\right)$$
14		eqid	$$⊢{+}_{\mathrm{LDual}\left(U\right)}={+}_{\mathrm{LDual}\left(U\right)}$$
15	1 2 13 14 6 8 9	lcdvadd	$$⊢\phi \to \underset{\dot{}}{✚}={+}_{\mathrm{LDual}\left(U\right)}$$
16	15	oveqd	$$⊢\phi \to F\underset{\dot{}}{✚}G=F{+}_{\mathrm{LDual}\left(U\right)}G$$
17	16	fveq1d	$$⊢\phi \to \left(F\underset{\dot{}}{✚}G\right)\left(X\right)=\left(F{+}_{\mathrm{LDual}\left(U\right)}G\right)\left(X\right)$$
18		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
19	1 2 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
20	1 6 7 2 18 9 10	lcdvbaselfl	$$⊢\phi \to F\in \mathrm{LFnl}\left(U\right)$$
21	1 6 7 2 18 9 11	lcdvbaselfl	$$⊢\phi \to G\in \mathrm{LFnl}\left(U\right)$$
22	3 4 5 18 13 14 19 20 21 12	ldualvaddval	$$⊢\phi \to \left(F{+}_{\mathrm{LDual}\left(U\right)}G\right)\left(X\right)=F\left(X\right)\underset{\dot{}}{+}G\left(X\right)$$
23	17 22	eqtrd	$$⊢\phi \to \left(F\underset{\dot{}}{✚}G\right)\left(X\right)=F\left(X\right)\underset{\dot{}}{+}G\left(X\right)$$