# 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
`|- H = ( LHyp ` K )`
hvmaplfl.u
`|- U = ( ( DVecH ` K ) ` W )`
hvmaplfl.v
`|- V = ( Base ` U )`
hvmaplfl.z
`|- .0. = ( 0g ` U )`
hvmaplfl.f
`|- F = ( LFnl ` U )`
hvmaplfl.m
`|- M = ( ( HVMap ` K ) ` W )`
hvmaplfl.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
hvmaplfl.x
`|- ( ph -> X e. ( V \ { .0. } ) )`
Assertion hvmaplfl
`|- ( ph -> ( M ` X ) e. F )`

### Proof

Step Hyp Ref Expression
1 hvmaplfl.h
` |-  H = ( LHyp ` K )`
2 hvmaplfl.u
` |-  U = ( ( DVecH ` K ) ` W )`
3 hvmaplfl.v
` |-  V = ( Base ` U )`
4 hvmaplfl.z
` |-  .0. = ( 0g ` U )`
5 hvmaplfl.f
` |-  F = ( LFnl ` U )`
6 hvmaplfl.m
` |-  M = ( ( HVMap ` K ) ` W )`
7 hvmaplfl.k
` |-  ( ph -> ( K e. HL /\ W e. H ) )`
8 hvmaplfl.x
` |-  ( ph -> X e. ( V \ { .0. } ) )`
9 eqid
` |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )`
10 eqid
` |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )`
11 eqid
` |-  ( 0g ` ( ( LCDual ` K ) ` W ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) )`
12 1 2 3 4 9 10 11 6 7 8 hvmapcl2
` |-  ( ph -> ( M ` X ) e. ( ( Base ` ( ( LCDual ` K ) ` W ) ) \ { ( 0g ` ( ( LCDual ` K ) ` W ) ) } ) )`
` |-  ( ph -> ( M ` X ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )`
` |-  ( ph -> ( M ` X ) e. F )`