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 } ) )