Metamath Proof Explorer


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 ˙ = 0 U
hvmap1o.f F = LFnl U
hvmap1o.l L = LKer U
hvmap1o.d D = LDual U
hvmap1o.q Q = 0 D
hvmap1o.c C = f F | O O L f = L f
hvmap1o.m M = HVMap K W
hvmap1o.k φ K HL W H
Assertion hvmap1o φ 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 ˙ = 0 U
6 hvmap1o.f F = LFnl U
7 hvmap1o.l L = LKer U
8 hvmap1o.d D = LDual U
9 hvmap1o.q Q = 0 D
10 hvmap1o.c C = f F | O O L f = L f
11 hvmap1o.m M = HVMap K W
12 hvmap1o.k φ K HL W H
13 eqid + U = + U
14 eqid U = U
15 eqid Scalar U = Scalar U
16 eqid Base Scalar U = Base Scalar U
17 eqid x V 0 ˙ v V ι k Base Scalar U | w O x v = w + U k U x = x V 0 ˙ v V ι k Base Scalar U | w O x v = w + U k U x
18 1 2 3 4 13 14 15 16 5 6 7 8 9 10 17 12 lcf1o φ x V 0 ˙ v V ι k Base Scalar U | w O x v = w + U k U x : V 0 ˙ 1-1 onto C Q
19 1 3 2 4 13 14 5 15 16 11 12 hvmapfval φ M = x V 0 ˙ v V ι k Base Scalar U | w O x v = w + U k U x
20 19 f1oeq1d φ M : V 0 ˙ 1-1 onto C Q x V 0 ˙ v V ι k Base Scalar U | w O x v = w + U k U x : V 0 ˙ 1-1 onto C Q
21 18 20 mpbird φ M : V 0 ˙ 1-1 onto C Q