Metamath Proof Explorer


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