Theorem lcf1o

Description: Define a function J that provides a bijection from nonzero vectors V to nonzero functionals with closed kernels C . (Contributed by NM, 22-Feb-2015)

	Ref	Expression
Hypotheses	lcf1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcf1o.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lcf1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcf1o.v	$$⊢V={\mathrm{Base}}_U$$
	lcf1o.a	$$⊢\underset{\dot{}}{+}={+}_U$$
	lcf1o.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	lcf1o.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcf1o.r	$$⊢R={\mathrm{Base}}_S$$
	lcf1o.z	$$⊢\underset{\dot{}}{0}=0_U$$
	lcf1o.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lcf1o.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcf1o.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lcf1o.q	$$⊢Q=0_D$$
	lcf1o.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
	lcf1o.j	$$⊢J=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)$$
	lcflo.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	lcf1o	$$⊢\phi \to J:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lcf1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcf1o.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcf1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lcf1o.v	$$⊢V={\mathrm{Base}}_U$$
5		lcf1o.a	$$⊢\underset{\dot{}}{+}={+}_U$$
6		lcf1o.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		lcf1o.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
8		lcf1o.r	$$⊢R={\mathrm{Base}}_S$$
9		lcf1o.z	$$⊢\underset{\dot{}}{0}=0_U$$
10		lcf1o.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
11		lcf1o.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
12		lcf1o.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
13		lcf1o.q	$$⊢Q=0_D$$
14		lcf1o.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
15		lcf1o.j	$$⊢J=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)$$
16		lcflo.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		oveq1	$$⊢w=z\to w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)=z\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)$$
18	17	eqeq2d	$$⊢w=z\to \left(v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow v=z\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)$$
19	18	cbvrexvw	$$⊢\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow \exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=z\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)$$
20		oveq1	$$⊢k=l\to k\underset{\dot{}}{·}x=l\underset{\dot{}}{·}x$$
21	20	oveq2d	$$⊢k=l\to z\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)$$
22	21	eqeq2d	$$⊢k=l\to \left(v=z\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow v=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
23	22	rexbidv	$$⊢k=l\to \left(\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=z\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow \exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
24	19 23	syl5bb	$$⊢k=l\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\leftrightarrow \exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
25	24	cbvriotavw	$$⊢\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)=\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
26		eqeq1	$$⊢v=u\to \left(v=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\leftrightarrow u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
27	26	rexbidv	$$⊢v=u\to \left(\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\leftrightarrow \exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
28	27	riotabidv	$$⊢v=u\to \left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)=\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
29	25 28	syl5eq	$$⊢v=u\to \left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)=\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)$$
30	29	cbvmptv	$$⊢\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)=\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)\right)$$
31		sneq	$$⊢x=y\to \left\{x\right\}=\left\{y\right\}$$
32	31	fveq2d	$$⊢x=y\to \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)=\underset{\dot{}}{\perp }\left(\left\{y\right\}\right)$$
33		oveq2	$$⊢x=y\to l\underset{\dot{}}{·}x=l\underset{\dot{}}{·}y$$
34	33	oveq2d	$$⊢x=y\to z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)$$
35	34	eqeq2d	$$⊢x=y\to \left(u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\leftrightarrow u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)$$
36	32 35	rexeqbidv	$$⊢x=y\to \left(\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\leftrightarrow \exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)$$
37	36	riotabidv	$$⊢x=y\to \left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)=\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)$$
38	37	mpteq2dv	$$⊢x=y\to \left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}x\right)\right)\right)=\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)\right)$$
39	30 38	syl5eq	$$⊢x=y\to \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)=\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)\right)$$
40	39	cbvmptv	$$⊢\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)=\left(y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)\right)\right)$$
41	15 40	eqtri	$$⊢J=\left(y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(u\in V⟼\left(\iota l\in R|\exists z\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)u=z\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}y\right)\right)\right)\right)$$
42	1 2 3 4 5 6 7 8 9 10 11 12 13 14 41 16	lcfrlem9	$$⊢\phi \to J:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}$$