Metamath Proof Explorer


Theorem ldualvaddcom

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

Ref Expression
Hypotheses ldualvaddcom.f F = LFnl W
ldualvaddcom.d D = LDual W
ldualvaddcom.p + ˙ = + D
ldualvaddcom.w φ W LMod
ldualvaddcom.x φ X F
ldualvaddcom.y φ Y F
Assertion ldualvaddcom φ X + ˙ Y = Y + ˙ X

Proof

Step Hyp Ref Expression
1 ldualvaddcom.f F = LFnl W
2 ldualvaddcom.d D = LDual W
3 ldualvaddcom.p + ˙ = + D
4 ldualvaddcom.w φ W LMod
5 ldualvaddcom.x φ X F
6 ldualvaddcom.y φ Y F
7 eqid Scalar W = Scalar W
8 eqid + Scalar W = + Scalar W
9 7 8 1 4 5 6 lfladdcom φ X + Scalar W f Y = Y + Scalar W f X
10 1 7 8 2 3 4 5 6 ldualvadd φ X + ˙ Y = X + Scalar W f Y
11 1 7 8 2 3 4 6 5 ldualvadd φ Y + ˙ X = Y + Scalar W f X
12 9 10 11 3eqtr4d φ X + ˙ Y = Y + ˙ X