ldual0vcl

Description: The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015)

Step	Hyp	Ref	Expression
1		ldualv0cl.f	$⊢ F = LFnl (W)$
2		ldualv0cl.d	$⊢ D = LDual (W)$
3		ldualv0cl.o	$⊢ \underset{˙}{0} = 0_{D}$
4		ldualv0cl.w	$⊢ φ \to W \in 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	$⊢ φ \to \underset{˙}{0} = {Base}_{W} \times \{0_{Scalar (W)}\}$
9	6 7 5 1	lfl0f	$⊢ W \in LMod \to {Base}_{W} \times \{0_{Scalar (W)}\} \in F$
10	4 9	syl	$⊢ φ \to {Base}_{W} \times \{0_{Scalar (W)}\} \in F$
11	8 10	eqeltrd	$⊢ φ \to \underset{˙}{0} \in F$

Metamath Proof Explorer