Metamath Proof Explorer


Theorem hvmapclN

Description: Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015) (New usage is discouraged.)

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
hvmapcl.x φ X V 0 ˙
Assertion hvmapclN φ M X 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 hvmapcl.x φ X V 0 ˙
14 1 2 3 4 5 6 7 8 9 10 11 12 hvmap1o φ M : V 0 ˙ 1-1 onto C Q
15 f1of M : V 0 ˙ 1-1 onto C Q M : V 0 ˙ C Q
16 14 15 syl φ M : V 0 ˙ C Q
17 16 13 ffvelrnd φ M X C Q