ldualvaddcom

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

Step	Hyp	Ref	Expression
1		ldualvaddcom.f	$⊢ F = LFnl (W)$
2		ldualvaddcom.d	$⊢ D = LDual (W)$
3		ldualvaddcom.p	$⊢ \underset{˙}{+} = +_{D}$
4		ldualvaddcom.w	$⊢ φ \to W \in LMod$
5		ldualvaddcom.x	$⊢ φ \to X \in F$
6		ldualvaddcom.y	$⊢ φ \to Y \in F$
7		eqid	$⊢ Scalar (W) = Scalar (W)$
8		eqid	$⊢ +_{Scalar (W)} = +_{Scalar (W)}$
9	7 8 1 4 5 6	lfladdcom	$⊢ φ \to X {+_{Scalar (W)}}_{f} Y = Y {+_{Scalar (W)}}_{f} X$
10	1 7 8 2 3 4 5 6	ldualvadd	$⊢ φ \to X \underset{˙}{+} Y = X {+_{Scalar (W)}}_{f} Y$
11	1 7 8 2 3 4 6 5	ldualvadd	$⊢ φ \to Y \underset{˙}{+} X = Y {+_{Scalar (W)}}_{f} X$
12	9 10 11	3eqtr4d	$⊢ φ \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Metamath Proof Explorer