Theorem lcdvbaselfl

Description: A vector in the base set of the closed kernel dual space is a functional. (Contributed by NM, 28-Mar-2015)

	Ref	Expression
Hypotheses	lcdvbasess.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdvbasess.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdvbasess.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
	lcdvbasess.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdvbasess.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcdvbasess.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcdvbaselfl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lcdvbaselfl	⊢ ( 𝜑 → 𝑋 ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		lcdvbasess.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdvbasess.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
3		lcdvbasess.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
4		lcdvbasess.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		lcdvbasess.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6		lcdvbasess.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		lcdvbaselfl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8	1 2 3 4 5 6	lcdvbasess	⊢ ( 𝜑 → 𝑉 ⊆ 𝐹 )
9	8 7	sseldd	⊢ ( 𝜑 → 𝑋 ∈ 𝐹 )