Theorem hvmap1o2

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	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 ) )
Assertion	hvmap1o2	|- ( ph -> M : ( V \ { .0. } ) -1-1-onto-> ( 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		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
11		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
12		eqid	|- ( LKer ` U ) = ( LKer ` U )
13		eqid	|- ( LDual ` U ) = ( LDual ` U )
14		eqid	|- ( 0g ` ( LDual ` U ) ) = ( 0g ` ( LDual ` U ) )
15		eqid	|- { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } = { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) }
16	1 10 2 3 4 11 12 13 14 15 8 9	hvmap1o	|- ( ph -> M : ( V \ { .0. } ) -1-1-onto-> ( { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } \ { ( 0g ` ( LDual ` U ) ) } ) )
17	1 10 5 6 2 11 12 15 9	lcdvbase	|- ( ph -> F = { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } )
18	1 2 13 14 5 7 9	lcd0v2	|- ( ph -> O = ( 0g ` ( LDual ` U ) ) )
19	18	sneqd	|- ( ph -> { O } = { ( 0g ` ( LDual ` U ) ) } )
20	17 19	difeq12d	|- ( ph -> ( F \ { O } ) = ( { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } \ { ( 0g ` ( LDual ` U ) ) } ) )
21		f1oeq3	|- ( ( F \ { O } ) = ( { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } \ { ( 0g ` ( LDual ` U ) ) } ) -> ( M : ( V \ { .0. } ) -1-1-onto-> ( F \ { O } ) <-> M : ( V \ { .0. } ) -1-1-onto-> ( { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } \ { ( 0g ` ( LDual ` U ) ) } ) ) )
22	20 21	syl	|- ( ph -> ( M : ( V \ { .0. } ) -1-1-onto-> ( F \ { O } ) <-> M : ( V \ { .0. } ) -1-1-onto-> ( { f e. ( LFnl ` U ) | ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) } \ { ( 0g ` ( LDual ` U ) ) } ) ) )
23	16 22	mpbird	|- ( ph -> M : ( V \ { .0. } ) -1-1-onto-> ( F \ { O } ) )