Theorem lcdvbasecl

Description: Closure of the value of a vector (functional) in the closed kernel dual space. (Contributed by NM, 28-Mar-2015)

	Ref	Expression
Hypotheses	lcdvbasecl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdvbasecl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdvbasecl.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcdvbasecl.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcdvbasecl.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lcdvbasecl.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdvbasecl.e	⊢ 𝐸 = ( Base ‘ 𝐶 )
	lcdvbasecl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcdvbasecl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐸 )
	lcdvbasecl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lcdvbasecl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		lcdvbasecl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdvbasecl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdvbasecl.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		lcdvbasecl.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
5		lcdvbasecl.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
6		lcdvbasecl.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7		lcdvbasecl.e	⊢ 𝐸 = ( Base ‘ 𝐶 )
8		lcdvbasecl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		lcdvbasecl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐸 )
10		lcdvbasecl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11	1 2 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
12		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
13	1 6 7 2 12 8 9	lcdvbaselfl	⊢ ( 𝜑 → 𝐹 ∈ ( LFnl ‘ 𝑈 ) )
14	4 5 3 12	lflcl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐹 ∈ ( LFnl ‘ 𝑈 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑅 )
15	11 13 10 14	syl3anc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ 𝑅 )