Theorem lcd0vcl

Description: Closure of the zero functional in the set of functionals with closed kernels. (Contributed by NM, 15-Mar-2015)

	Ref	Expression
Hypotheses	lcdv0cl.h	|- H = ( LHyp ` K )
	lcdv0cl.c	|- C = ( ( LCDual ` K ) ` W )
	lcdv0cl.v	|- V = ( Base ` C )
	lcdv0cl.o	|- O = ( 0g ` C )
	lcdv0cl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	lcd0vcl	|- ( ph -> O e. V )

Proof

Step	Hyp	Ref	Expression
1		lcdv0cl.h	|- H = ( LHyp ` K )
2		lcdv0cl.c	|- C = ( ( LCDual ` K ) ` W )
3		lcdv0cl.v	|- V = ( Base ` C )
4		lcdv0cl.o	|- O = ( 0g ` C )
5		lcdv0cl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
6	1 2 5	lcdlmod	|- ( ph -> C e. LMod )
7	3 4	lmod0vcl	|- ( C e. LMod -> O e. V )
8	6 7	syl	|- ( ph -> O e. V )