# Metamath Proof Explorer

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