Metamath Proof Explorer


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 ( 𝜑 → ( 𝐹𝑋 ) ∈ 𝑅 )