# 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 𝐻 = ( LHyp ‘ 𝐾 )
hvmap1o2.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hvmap1o2.v 𝑉 = ( Base ‘ 𝑈 )
hvmap1o2.z 0 = ( 0g𝑈 )
hvmap1o2.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hvmap1o2.f 𝐹 = ( Base ‘ 𝐶 )
hvmap1o2.o 𝑂 = ( 0g𝐶 )
hvmap1o2.m 𝑀 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
hvmap1o2.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
Assertion hvmap1o2 ( 𝜑𝑀 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐹 ∖ { 𝑂 } ) )

### Proof

Step Hyp Ref Expression
1 hvmap1o2.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hvmap1o2.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hvmap1o2.v 𝑉 = ( Base ‘ 𝑈 )
4 hvmap1o2.z 0 = ( 0g𝑈 )
5 hvmap1o2.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 hvmap1o2.f 𝐹 = ( Base ‘ 𝐶 )
7 hvmap1o2.o 𝑂 = ( 0g𝐶 )
8 hvmap1o2.m 𝑀 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
9 hvmap1o2.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 eqid ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
11 eqid ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
12 eqid ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
13 eqid ( LDual ‘ 𝑈 ) = ( LDual ‘ 𝑈 )
14 eqid ( 0g ‘ ( LDual ‘ 𝑈 ) ) = ( 0g ‘ ( LDual ‘ 𝑈 ) )
15 eqid { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) }
16 1 10 2 3 4 11 12 13 14 15 8 9 hvmap1o ( 𝜑𝑀 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∖ { ( 0g ‘ ( LDual ‘ 𝑈 ) ) } ) )
17 1 10 5 6 2 11 12 15 9 lcdvbase ( 𝜑𝐹 = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } )
18 1 2 13 14 5 7 9 lcd0v2 ( 𝜑𝑂 = ( 0g ‘ ( LDual ‘ 𝑈 ) ) )
19 18 sneqd ( 𝜑 → { 𝑂 } = { ( 0g ‘ ( LDual ‘ 𝑈 ) ) } )
20 17 19 difeq12d ( 𝜑 → ( 𝐹 ∖ { 𝑂 } ) = ( { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∖ { ( 0g ‘ ( LDual ‘ 𝑈 ) ) } ) )
21 f1oeq3 ( ( 𝐹 ∖ { 𝑂 } ) = ( { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∖ { ( 0g ‘ ( LDual ‘ 𝑈 ) ) } ) → ( 𝑀 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐹 ∖ { 𝑂 } ) ↔ 𝑀 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∖ { ( 0g ‘ ( LDual ‘ 𝑈 ) ) } ) ) )
22 20 21 syl ( 𝜑 → ( 𝑀 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐹 ∖ { 𝑂 } ) ↔ 𝑀 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∖ { ( 0g ‘ ( LDual ‘ 𝑈 ) ) } ) ) )
23 16 22 mpbird ( 𝜑𝑀 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐹 ∖ { 𝑂 } ) )