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=\mathrm{LHyp}\left(K\right)$$
	hvmap1o.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	hvmap1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hvmap1o.v	$$⊢V={\mathrm{Base}}_U$$
	hvmap1o.z	$$⊢\underset{\dot{}}{0}=0_U$$
	hvmap1o.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	hvmap1o.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	hvmap1o.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	hvmap1o.q	$$⊢Q=0_D$$
	hvmap1o.c	$$⊢C=\left\{f\in F|O\left(O\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
	hvmap1o.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	hvmap1o.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	hvmap1o	$$⊢\phi \to M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}$$

Proof

Step	Hyp	Ref	Expression
1		hvmap1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hvmap1o.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		hvmap1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		hvmap1o.v	$$⊢V={\mathrm{Base}}_U$$
5		hvmap1o.z	$$⊢\underset{\dot{}}{0}=0_U$$
6		hvmap1o.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
7		hvmap1o.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
8		hvmap1o.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
9		hvmap1o.q	$$⊢Q=0_D$$
10		hvmap1o.c	$$⊢C=\left\{f\in F|O\left(O\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
11		hvmap1o.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
12		hvmap1o.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
13		eqid	$$⊢{+}_U={+}_U$$
14		eqid	$$⊢{\cdot }_U={\cdot }_U$$
15		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
16		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
17		eqid	$$⊢\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}|\exists w\in O\left(\left\{x\right\}\right)v=w{+}_U\left(k{\cdot }_{U}x\right)\right)\right)\right)=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}|\exists w\in O\left(\left\{x\right\}\right)v=w{+}_U\left(k{\cdot }_{U}x\right)\right)\right)\right)$$
18	1 2 3 4 13 14 15 16 5 6 7 8 9 10 17 12	lcf1o	$$⊢\phi \to \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}|\exists w\in O\left(\left\{x\right\}\right)v=w{+}_U\left(k{\cdot }_{U}x\right)\right)\right)\right):V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}$$
19	1 3 2 4 13 14 5 15 16 11 12	hvmapfval	$$⊢\phi \to M=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}|\exists w\in O\left(\left\{x\right\}\right)v=w{+}_U\left(k{\cdot }_{U}x\right)\right)\right)\right)$$
20	19	f1oeq1d	$$⊢\phi \to \left(M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}\leftrightarrow \left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}|\exists w\in O\left(\left\{x\right\}\right)v=w{+}_U\left(k{\cdot }_{U}x\right)\right)\right)\right):V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}\right)$$
21	18 20	mpbird	$$⊢\phi \to M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}$$