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=\mathrm{LHyp}\left(K\right)$$
	lcdv0cl.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdv0cl.v	$$⊢V={\mathrm{Base}}_C$$
	lcdv0cl.o	$$⊢O=0_C$$
	lcdv0cl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	lcd0vcl	$$⊢\phi \to O\in V$$

Proof

Step	Hyp	Ref	Expression
1		lcdv0cl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdv0cl.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
3		lcdv0cl.v	$$⊢V={\mathrm{Base}}_C$$
4		lcdv0cl.o	$$⊢O=0_C$$
5		lcdv0cl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6	1 2 5	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
7	3 4	lmod0vcl	$$⊢C\in \mathrm{LMod}\to O\in V$$
8	6 7	syl	$$⊢\phi \to O\in V$$