Theorem ldualvaddcl

Description: The value of vector addition in the dual of a vector space is a functional. (Contributed by NM, 21-Oct-2014)

	Ref	Expression
Hypotheses	ldualvaddcl.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualvaddcl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualvaddcl.p	$$⊢\underset{\dot{}}{+}={+}_D$$
	ldualvaddcl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ldualvaddcl.g	$$⊢\phi \to G\in F$$
	ldualvaddcl.h	$$⊢\phi \to H\in F$$
Assertion	ldualvaddcl	$$⊢\phi \to G\underset{\dot{}}{+}H\in F$$

Proof

Step	Hyp	Ref	Expression
1		ldualvaddcl.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualvaddcl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
3		ldualvaddcl.p	$$⊢\underset{\dot{}}{+}={+}_D$$
4		ldualvaddcl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		ldualvaddcl.g	$$⊢\phi \to G\in F$$
6		ldualvaddcl.h	$$⊢\phi \to H\in F$$
7		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
8		eqid	$$⊢{+}_{\mathrm{Scalar}\left(W\right)}={+}_{\mathrm{Scalar}\left(W\right)}$$
9	1 7 8 2 3 4 5 6	ldualvadd	$$⊢\phi \to G\underset{\dot{}}{+}H=G{{+}_{\mathrm{Scalar}\left(W\right)}}_{f}H$$
10	7 8 1 4 5 6	lfladdcl	$$⊢\phi \to G{{+}_{\mathrm{Scalar}\left(W\right)}}_{f}H\in F$$
11	9 10	eqeltrd	$$⊢\phi \to G\underset{\dot{}}{+}H\in F$$