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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdv0cl.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdv0cl.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
	lcdv0cl.o	⊢ 𝑂 = ( 0g ‘ 𝐶 )
	lcdv0cl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	lcd0vcl	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lcdv0cl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdv0cl.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
3		lcdv0cl.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
4		lcdv0cl.o	⊢ 𝑂 = ( 0g ‘ 𝐶 )
5		lcdv0cl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6	1 2 5	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
7	3 4	lmod0vcl	⊢ ( 𝐶 ∈ LMod → 𝑂 ∈ 𝑉 )
8	6 7	syl	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )