Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Opposite rings and dual vector spaces
ldualvaddcom
Next ⟩
ldualvsass
Metamath Proof Explorer
Ascii
Unicode
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