# Metamath Proof Explorer

## Theorem hvmapcl2

Description: Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015)

Ref Expression
Hypotheses hvmap1o2.h
`|- H = ( LHyp ` K )`
hvmap1o2.u
`|- U = ( ( DVecH ` K ) ` W )`
hvmap1o2.v
`|- V = ( Base ` U )`
hvmap1o2.z
`|- .0. = ( 0g ` U )`
hvmap1o2.c
`|- C = ( ( LCDual ` K ) ` W )`
hvmap1o2.f
`|- F = ( Base ` C )`
hvmap1o2.o
`|- O = ( 0g ` C )`
hvmap1o2.m
`|- M = ( ( HVMap ` K ) ` W )`
hvmap1o2.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
hvmapcl2.x
`|- ( ph -> X e. ( V \ { .0. } ) )`
Assertion hvmapcl2
`|- ( ph -> ( M ` X ) e. ( F \ { O } ) )`

### Proof

Step Hyp Ref Expression
1 hvmap1o2.h
` |-  H = ( LHyp ` K )`
2 hvmap1o2.u
` |-  U = ( ( DVecH ` K ) ` W )`
3 hvmap1o2.v
` |-  V = ( Base ` U )`
4 hvmap1o2.z
` |-  .0. = ( 0g ` U )`
5 hvmap1o2.c
` |-  C = ( ( LCDual ` K ) ` W )`
6 hvmap1o2.f
` |-  F = ( Base ` C )`
7 hvmap1o2.o
` |-  O = ( 0g ` C )`
8 hvmap1o2.m
` |-  M = ( ( HVMap ` K ) ` W )`
9 hvmap1o2.k
` |-  ( ph -> ( K e. HL /\ W e. H ) )`
10 hvmapcl2.x
` |-  ( ph -> X e. ( V \ { .0. } ) )`
11 1 2 3 4 5 6 7 8 9 hvmap1o2
` |-  ( ph -> M : ( V \ { .0. } ) -1-1-onto-> ( F \ { O } ) )`
12 f1of
` |-  ( M : ( V \ { .0. } ) -1-1-onto-> ( F \ { O } ) -> M : ( V \ { .0. } ) --> ( F \ { O } ) )`
13 11 12 syl
` |-  ( ph -> M : ( V \ { .0. } ) --> ( F \ { O } ) )`
14 13 10 ffvelrnd
` |-  ( ph -> ( M ` X ) e. ( F \ { O } ) )`