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={\mathrm{Base}}_W$$
	ldualvaddval.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualvaddval.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	ldualvaddval.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualvaddval.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualvaddval.p	$$⊢\underset{\dot{}}{✚}={+}_D$$
	ldualvaddval.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ldualvaddval.g	$$⊢\phi \to G\in F$$
	ldualvaddval.h	$$⊢\phi \to H\in F$$
	ldualvaddval.x	$$⊢\phi \to X\in V$$
Assertion	ldualvaddval	$$⊢\phi \to \left(G\underset{\dot{}}{✚}H\right)\left(X\right)=G\left(X\right)\underset{\dot{}}{+}H\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		ldualvaddval.v	$$⊢V={\mathrm{Base}}_W$$
2		ldualvaddval.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		ldualvaddval.a	$$⊢\underset{\dot{}}{+}={+}_R$$
4		ldualvaddval.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
5		ldualvaddval.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
6		ldualvaddval.p	$$⊢\underset{\dot{}}{✚}={+}_D$$
7		ldualvaddval.w	$$⊢\phi \to W\in \mathrm{LMod}$$
8		ldualvaddval.g	$$⊢\phi \to G\in F$$
9		ldualvaddval.h	$$⊢\phi \to H\in F$$
10		ldualvaddval.x	$$⊢\phi \to X\in V$$
11	4 2 3 5 6 7 8 9	ldualvadd	$$⊢\phi \to G\underset{\dot{}}{✚}H=G{\underset{\dot{}}{+}}_{f}H$$
12	11	fveq1d	$$⊢\phi \to \left(G\underset{\dot{}}{✚}H\right)\left(X\right)=\left(G{\underset{\dot{}}{+}}_{f}H\right)\left(X\right)$$
13		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
14	2 13 1 4	lflf	$$⊢\left(W\in \mathrm{LMod}\wedge G\in F\right)\to G:V⟶{\mathrm{Base}}_R$$
15	14	ffnd	$$⊢\left(W\in \mathrm{LMod}\wedge G\in F\right)\to GFnV$$
16	7 8 15	syl2anc	$$⊢\phi \to GFnV$$
17	2 13 1 4	lflf	$$⊢\left(W\in \mathrm{LMod}\wedge H\in F\right)\to H:V⟶{\mathrm{Base}}_R$$
18	17	ffnd	$$⊢\left(W\in \mathrm{LMod}\wedge H\in F\right)\to HFnV$$
19	7 9 18	syl2anc	$$⊢\phi \to HFnV$$
20	1	fvexi	$$⊢V\in \mathrm{V}$$
21	20	a1i	$$⊢\phi \to V\in \mathrm{V}$$
22		inidm	$$⊢V\cap V=V$$
23		eqidd	$$⊢\left(\phi \wedge X\in V\right)\to G\left(X\right)=G\left(X\right)$$
24		eqidd	$$⊢\left(\phi \wedge X\in V\right)\to H\left(X\right)=H\left(X\right)$$
25	16 19 21 21 22 23 24	ofval	$$⊢\left(\phi \wedge X\in V\right)\to \left(G{\underset{\dot{}}{+}}_{f}H\right)\left(X\right)=G\left(X\right)\underset{\dot{}}{+}H\left(X\right)$$
26	10 25	mpdan	$$⊢\phi \to \left(G{\underset{\dot{}}{+}}_{f}H\right)\left(X\right)=G\left(X\right)\underset{\dot{}}{+}H\left(X\right)$$
27	12 26	eqtrd	$$⊢\phi \to \left(G\underset{\dot{}}{✚}H\right)\left(X\right)=G\left(X\right)\underset{\dot{}}{+}H\left(X\right)$$