Metamath Proof Explorer


Theorem hvmaplfl

Description: The vector to functional map value is a functional. (Contributed by NM, 28-Mar-2015)

Ref Expression
Hypotheses hvmaplfl.h 𝐻 = ( LHyp ‘ 𝐾 )
hvmaplfl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hvmaplfl.v 𝑉 = ( Base ‘ 𝑈 )
hvmaplfl.z 0 = ( 0g𝑈 )
hvmaplfl.f 𝐹 = ( LFnl ‘ 𝑈 )
hvmaplfl.m 𝑀 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
hvmaplfl.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hvmaplfl.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion hvmaplfl ( 𝜑 → ( 𝑀𝑋 ) ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 hvmaplfl.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hvmaplfl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hvmaplfl.v 𝑉 = ( Base ‘ 𝑈 )
4 hvmaplfl.z 0 = ( 0g𝑈 )
5 hvmaplfl.f 𝐹 = ( LFnl ‘ 𝑈 )
6 hvmaplfl.m 𝑀 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
7 hvmaplfl.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
8 hvmaplfl.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
9 eqid ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
10 eqid ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
11 eqid ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
12 1 2 3 4 9 10 11 6 7 8 hvmapcl2 ( 𝜑 → ( 𝑀𝑋 ) ∈ ( ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) } ) )
13 12 eldifad ( 𝜑 → ( 𝑀𝑋 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
14 1 9 10 2 5 7 13 lcdvbaselfl ( 𝜑 → ( 𝑀𝑋 ) ∈ 𝐹 )