Theorem ldualvaddcom

Description: Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015)

	Ref	Expression
Hypotheses	ldualvaddcom.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualvaddcom.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualvaddcom.p	$$⊢\underset{\dot{}}{+}={+}_D$$
	ldualvaddcom.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ldualvaddcom.x	$$⊢\phi \to X\in F$$
	ldualvaddcom.y	$$⊢\phi \to Y\in F$$
Assertion	ldualvaddcom	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$

Proof

Step	Hyp	Ref	Expression
1		ldualvaddcom.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualvaddcom.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
3		ldualvaddcom.p	$$⊢\underset{\dot{}}{+}={+}_D$$
4		ldualvaddcom.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		ldualvaddcom.x	$$⊢\phi \to X\in F$$
6		ldualvaddcom.y	$$⊢\phi \to Y\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	7 8 1 4 5 6	lfladdcom	$$⊢\phi \to X{{+}_{\mathrm{Scalar}\left(W\right)}}_{f}Y=Y{{+}_{\mathrm{Scalar}\left(W\right)}}_{f}X$$
10	1 7 8 2 3 4 5 6	ldualvadd	$$⊢\phi \to X\underset{\dot{}}{+}Y=X{{+}_{\mathrm{Scalar}\left(W\right)}}_{f}Y$$
11	1 7 8 2 3 4 6 5	ldualvadd	$$⊢\phi \to Y\underset{\dot{}}{+}X=Y{{+}_{\mathrm{Scalar}\left(W\right)}}_{f}X$$
12	9 10 11	3eqtr4d	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$