Theorem ldualsaddN

Description: Scalar addition for the dual of a vector space. (Contributed by NM, 24-Oct-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ldualsadd.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	ldualsadd.q	$$⊢\underset{\dot{}}{+}={+}_F$$
	ldualsadd.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualsadd.r	$$⊢R=\mathrm{Scalar}\left(D\right)$$
	ldualsadd.p	$$⊢\underset{\dot{}}{✚}={+}_R$$
	ldualsadd.w	$$⊢\phi \to W\in V$$
Assertion	ldualsaddN	$$⊢\phi \to \underset{\dot{}}{✚}=\underset{\dot{}}{+}$$

Proof

Step	Hyp	Ref	Expression
1		ldualsadd.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		ldualsadd.q	$$⊢\underset{\dot{}}{+}={+}_F$$
3		ldualsadd.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
4		ldualsadd.r	$$⊢R=\mathrm{Scalar}\left(D\right)$$
5		ldualsadd.p	$$⊢\underset{\dot{}}{✚}={+}_R$$
6		ldualsadd.w	$$⊢\phi \to W\in V$$
7		eqid	$$⊢{opp}_r\left(F\right)={opp}_r\left(F\right)$$
8	1 7 3 4 6	ldualsca	$$⊢\phi \to R={opp}_r\left(F\right)$$
9	8	fveq2d	$$⊢\phi \to {+}_R={+}_{{opp}_r\left(F\right)}$$
10	7 2	oppradd	$$⊢\underset{\dot{}}{+}={+}_{{opp}_r\left(F\right)}$$
11	9 5 10	3eqtr4g	$$⊢\phi \to \underset{\dot{}}{✚}=\underset{\dot{}}{+}$$