Theorem hvmapclN

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

	Ref	Expression
Hypotheses	hvmap1o.h	|- H = ( LHyp ` K )
	hvmap1o.o	|- O = ( ( ocH ` K ) ` W )
	hvmap1o.u	|- U = ( ( DVecH ` K ) ` W )
	hvmap1o.v	|- V = ( Base ` U )
	hvmap1o.z	|- .0. = ( 0g ` U )
	hvmap1o.f	|- F = ( LFnl ` U )
	hvmap1o.l	|- L = ( LKer ` U )
	hvmap1o.d	|- D = ( LDual ` U )
	hvmap1o.q	|- Q = ( 0g ` D )
	hvmap1o.c	|- C = { f e. F | ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) }
	hvmap1o.m	|- M = ( ( HVMap ` K ) ` W )
	hvmap1o.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hvmapcl.x	|- ( ph -> X e. ( V \ { .0. } ) )
Assertion	hvmapclN	|- ( ph -> ( M ` X ) e. ( C \ { Q } ) )

Proof

Step	Hyp	Ref	Expression
1		hvmap1o.h	|- H = ( LHyp ` K )
2		hvmap1o.o	|- O = ( ( ocH ` K ) ` W )
3		hvmap1o.u	|- U = ( ( DVecH ` K ) ` W )
4		hvmap1o.v	|- V = ( Base ` U )
5		hvmap1o.z	|- .0. = ( 0g ` U )
6		hvmap1o.f	|- F = ( LFnl ` U )
7		hvmap1o.l	|- L = ( LKer ` U )
8		hvmap1o.d	|- D = ( LDual ` U )
9		hvmap1o.q	|- Q = ( 0g ` D )
10		hvmap1o.c	|- C = { f e. F | ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) }
11		hvmap1o.m	|- M = ( ( HVMap ` K ) ` W )
12		hvmap1o.k	|- ( ph -> ( K e. HL /\ W e. H ) )
13		hvmapcl.x	|- ( ph -> X e. ( V \ { .0. } ) )
14	1 2 3 4 5 6 7 8 9 10 11 12	hvmap1o	|- ( ph -> M : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) )
15		f1of	|- ( M : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) -> M : ( V \ { .0. } ) --> ( C \ { Q } ) )
16	14 15	syl	|- ( ph -> M : ( V \ { .0. } ) --> ( C \ { Q } ) )
17	16 13	ffvelrnd	|- ( ph -> ( M ` X ) e. ( C \ { Q } ) )