Theorem hvmap1o

Description: The vector to functional map provides a bijection from nonzero vectors V to nonzero functionals with closed kernels C . (Contributed by NM, 27-Mar-2015)

	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 ) )
Assertion	hvmap1o	|- ( ph -> M : ( V \ { .0. } ) -1-1-onto-> ( 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		eqid	|- ( +g ` U ) = ( +g ` U )
14		eqid	|- ( .s ` U ) = ( .s ` U )
15		eqid	|- ( Scalar ` U ) = ( Scalar ` U )
16		eqid	|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
17		eqid	|- ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. ( Base ` ( Scalar ` U ) ) E. w e. ( O ` { x } ) v = ( w ( +g ` U ) ( k ( .s ` U ) x ) ) ) ) ) = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. ( Base ` ( Scalar ` U ) ) E. w e. ( O ` { x } ) v = ( w ( +g ` U ) ( k ( .s ` U ) x ) ) ) ) )
18	1 2 3 4 13 14 15 16 5 6 7 8 9 10 17 12	lcf1o	|- ( ph -> ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. ( Base ` ( Scalar ` U ) ) E. w e. ( O ` { x } ) v = ( w ( +g ` U ) ( k ( .s ` U ) x ) ) ) ) ) : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) )
19	1 3 2 4 13 14 5 15 16 11 12	hvmapfval	|- ( ph -> M = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. ( Base ` ( Scalar ` U ) ) E. w e. ( O ` { x } ) v = ( w ( +g ` U ) ( k ( .s ` U ) x ) ) ) ) ) )
20	19	f1oeq1d	|- ( ph -> ( M : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) <-> ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. ( Base ` ( Scalar ` U ) ) E. w e. ( O ` { x } ) v = ( w ( +g ` U ) ( k ( .s ` U ) x ) ) ) ) ) : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) ) )
21	18 20	mpbird	|- ( ph -> M : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) )