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. = ( 0g ` D )
	ldualv0cl.w	|- ( ph -> W e. LMod )
Assertion	ldual0vcl	|- ( ph -> .0. e. F )

Proof

Step	Hyp	Ref	Expression
1		ldualv0cl.f	|- F = ( LFnl ` W )
2		ldualv0cl.d	|- D = ( LDual ` W )
3		ldualv0cl.o	|- .0. = ( 0g ` D )
4		ldualv0cl.w	|- ( ph -> W e. LMod )
5		eqid	|- ( Base ` W ) = ( Base ` W )
6		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
7		eqid	|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
8	5 6 7 2 3 4	ldual0v	|- ( ph -> .0. = ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) )
9	6 7 5 1	lfl0f	|- ( W e. LMod -> ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) e. F )
10	4 9	syl	|- ( ph -> ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) e. F )
11	8 10	eqeltrd	|- ( ph -> .0. e. F )