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=\mathrm{LHyp}\left(K\right)$$
	hvmap1o2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hvmap1o2.v	$$⊢V={\mathrm{Base}}_U$$
	hvmap1o2.z	$$⊢\underset{\dot{}}{0}=0_U$$
	hvmap1o2.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hvmap1o2.f	$$⊢F={\mathrm{Base}}_C$$
	hvmap1o2.o	$$⊢O=0_C$$
	hvmap1o2.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	hvmap1o2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	hvmap1o2	$$⊢\phi \to M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}F\setminus \left\{O\right\}$$

Proof

Step	Hyp	Ref	Expression
1		hvmap1o2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hvmap1o2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hvmap1o2.v	$$⊢V={\mathrm{Base}}_U$$
4		hvmap1o2.z	$$⊢\underset{\dot{}}{0}=0_U$$
5		hvmap1o2.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hvmap1o2.f	$$⊢F={\mathrm{Base}}_C$$
7		hvmap1o2.o	$$⊢O=0_C$$
8		hvmap1o2.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
9		hvmap1o2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		eqid	$$⊢\mathrm{ocH}\left(K\right)\left(W\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
11		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
12		eqid	$$⊢\mathrm{LKer}\left(U\right)=\mathrm{LKer}\left(U\right)$$
13		eqid	$$⊢\mathrm{LDual}\left(U\right)=\mathrm{LDual}\left(U\right)$$
14		eqid	$$⊢0_{\mathrm{LDual}\left(U\right)}=0_{\mathrm{LDual}\left(U\right)}$$
15		eqid	$$⊢\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}=\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}$$
16	1 10 2 3 4 11 12 13 14 15 8 9	hvmap1o	$$⊢\phi \to M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}\setminus \left\{0_{\mathrm{LDual}\left(U\right)}\right\}$$
17	1 10 5 6 2 11 12 15 9	lcdvbase	$$⊢\phi \to F=\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}$$
18	1 2 13 14 5 7 9	lcd0v2	$$⊢\phi \to O=0_{\mathrm{LDual}\left(U\right)}$$
19	18	sneqd	$$⊢\phi \to \left\{O\right\}=\left\{0_{\mathrm{LDual}\left(U\right)}\right\}$$
20	17 19	difeq12d	$$⊢\phi \to F\setminus \left\{O\right\}=\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}\setminus \left\{0_{\mathrm{LDual}\left(U\right)}\right\}$$
21		f1oeq3	$$⊢F\setminus \left\{O\right\}=\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}\setminus \left\{0_{\mathrm{LDual}\left(U\right)}\right\}\to \left(M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}F\setminus \left\{O\right\}\leftrightarrow M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}\setminus \left\{0_{\mathrm{LDual}\left(U\right)}\right\}\right)$$
22	20 21	syl	$$⊢\phi \to \left(M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}F\setminus \left\{O\right\}\leftrightarrow M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}\setminus \left\{0_{\mathrm{LDual}\left(U\right)}\right\}\right)$$
23	16 22	mpbird	$$⊢\phi \to M:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}F\setminus \left\{O\right\}$$