Theorem ldualvadd

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

	Ref	Expression
Hypotheses	ldualvadd.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualvadd.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualvadd.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	ldualvadd.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualvadd.p	$$⊢\underset{\dot{}}{✚}={+}_D$$
	ldualvadd.w	$$⊢\phi \to W\in X$$
	ldualvadd.g	$$⊢\phi \to G\in F$$
	ldualvadd.h	$$⊢\phi \to H\in F$$
Assertion	ldualvadd	$$⊢\phi \to G\underset{\dot{}}{✚}H=G{\underset{\dot{}}{+}}_{f}H$$

Proof

Step	Hyp	Ref	Expression
1		ldualvadd.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualvadd.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		ldualvadd.a	$$⊢\underset{\dot{}}{+}={+}_R$$
4		ldualvadd.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
5		ldualvadd.p	$$⊢\underset{\dot{}}{✚}={+}_D$$
6		ldualvadd.w	$$⊢\phi \to W\in X$$
7		ldualvadd.g	$$⊢\phi \to G\in F$$
8		ldualvadd.h	$$⊢\phi \to H\in F$$
9		eqid	$$⊢{{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}$$
10	1 2 3 4 5 6 9	ldualfvadd	$$⊢\phi \to \underset{\dot{}}{✚}={{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}$$
11	10	oveqd	$$⊢\phi \to G\underset{\dot{}}{✚}H=G\left({{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}\right)H$$
12	7 8	ofmresval	$$⊢\phi \to G\left({{\circ }_f\underset{\dot{}}{+}\upharpoonright }_{\left(F\times F\right)}\right)H=G{\underset{\dot{}}{+}}_{f}H$$
13	11 12	eqtrd	$$⊢\phi \to G\underset{\dot{}}{✚}H=G{\underset{\dot{}}{+}}_{f}H$$