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