Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Opposite rings and dual vector spaces
ldual0vcl
Next ⟩
lduallmodlem
Metamath Proof Explorer
Ascii
Unicode
Theorem
ldual0vcl
Description:
The dual zero vector is a functional.
(Contributed by
NM
, 5-Mar-2015)
Ref
Expression
Hypotheses
ldualv0cl.f
⊢
F
=
LFnl
⁡
W
ldualv0cl.d
⊢
D
=
LDual
⁡
W
ldualv0cl.o
⊢
0
˙
=
0
D
ldualv0cl.w
⊢
φ
→
W
∈
LMod
Assertion
ldual0vcl
⊢
φ
→
0
˙
∈
F
Proof
Step
Hyp
Ref
Expression
1
ldualv0cl.f
⊢
F
=
LFnl
⁡
W
2
ldualv0cl.d
⊢
D
=
LDual
⁡
W
3
ldualv0cl.o
⊢
0
˙
=
0
D
4
ldualv0cl.w
⊢
φ
→
W
∈
LMod
5
eqid
⊢
Base
W
=
Base
W
6
eqid
⊢
Scalar
⁡
W
=
Scalar
⁡
W
7
eqid
⊢
0
Scalar
⁡
W
=
0
Scalar
⁡
W
8
5
6
7
2
3
4
ldual0v
⊢
φ
→
0
˙
=
Base
W
×
0
Scalar
⁡
W
9
6
7
5
1
lfl0f
⊢
W
∈
LMod
→
Base
W
×
0
Scalar
⁡
W
∈
F
10
4
9
syl
⊢
φ
→
Base
W
×
0
Scalar
⁡
W
∈
F
11
8
10
eqeltrd
⊢
φ
→
0
˙
∈
F