Theorem hvmapfval

Description: Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015)

	Ref	Expression
Hypotheses	hvmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hvmapval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hvmapval.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	hvmapval.v	$$⊢V={\mathrm{Base}}_U$$
	hvmapval.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	hvmapval.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hvmapval.z	$$⊢\underset{\dot{}}{0}=0_U$$
	hvmapval.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	hvmapval.r	$$⊢R={\mathrm{Base}}_S$$
	hvmapval.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	hvmapval.k	$$⊢\phi \to \left(K\in A\wedge W\in H\right)$$
Assertion	hvmapfval	$$⊢\phi \to M=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hvmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hvmapval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hvmapval.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
4		hvmapval.v	$$⊢V={\mathrm{Base}}_U$$
5		hvmapval.p	$$⊢\underset{\dot{}}{+}={+}_U$$
6		hvmapval.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		hvmapval.z	$$⊢\underset{\dot{}}{0}=0_U$$
8		hvmapval.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
9		hvmapval.r	$$⊢R={\mathrm{Base}}_S$$
10		hvmapval.m	$$⊢M=\mathrm{HVMap}\left(K\right)\left(W\right)$$
11		hvmapval.k	$$⊢\phi \to \left(K\in A\wedge W\in H\right)$$
12	1	hvmapffval	$$⊢K\in A\to \mathrm{HVMap}\left(K\right)=\left(w\in H⟼\left(x\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\setminus \left\{0_{\mathrm{DVecH}\left(K\right)\left(w\right)}\right\}\right)⟼\left(v\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)}|\exists t\in \mathrm{ocH}\left(K\right)\left(w\right)\left(\left\{x\right\}\right)v=t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)\right)\right)\right)\right)$$
13	12	fveq1d	$$⊢K\in A\to \mathrm{HVMap}\left(K\right)\left(W\right)=\left(w\in H⟼\left(x\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\setminus \left\{0_{\mathrm{DVecH}\left(K\right)\left(w\right)}\right\}\right)⟼\left(v\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)}|\exists t\in \mathrm{ocH}\left(K\right)\left(w\right)\left(\left\{x\right\}\right)v=t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)\right)\right)\right)\right)\left(W\right)$$
14	10 13	syl5eq	$$⊢K\in A\to M=\left(w\in H⟼\left(x\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\setminus \left\{0_{\mathrm{DVecH}\left(K\right)\left(w\right)}\right\}\right)⟼\left(v\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)}|\exists t\in \mathrm{ocH}\left(K\right)\left(w\right)\left(\left\{x\right\}\right)v=t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)\right)\right)\right)\right)\left(W\right)$$
15		fveq2	$$⊢w=W\to \mathrm{DVecH}\left(K\right)\left(w\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
16	15 2	eqtr4di	$$⊢w=W\to \mathrm{DVecH}\left(K\right)\left(w\right)=U$$
17	16	fveq2d	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}={\mathrm{Base}}_U$$
18	17 4	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}=V$$
19	16	fveq2d	$$⊢w=W\to 0_{\mathrm{DVecH}\left(K\right)\left(w\right)}=0_U$$
20	19 7	eqtr4di	$$⊢w=W\to 0_{\mathrm{DVecH}\left(K\right)\left(w\right)}=\underset{\dot{}}{0}$$
21	20	sneqd	$$⊢w=W\to \left\{0_{\mathrm{DVecH}\left(K\right)\left(w\right)}\right\}=\left\{\underset{\dot{}}{0}\right\}$$
22	18 21	difeq12d	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\setminus \left\{0_{\mathrm{DVecH}\left(K\right)\left(w\right)}\right\}=V\setminus \left\{\underset{\dot{}}{0}\right\}$$
23	16	fveq2d	$$⊢w=W\to \mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)=\mathrm{Scalar}\left(U\right)$$
24	23 8	eqtr4di	$$⊢w=W\to \mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)=S$$
25	24	fveq2d	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)}={\mathrm{Base}}_S$$
26	25 9	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)}=R$$
27		fveq2	$$⊢w=W\to \mathrm{ocH}\left(K\right)\left(w\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
28	27 3	eqtr4di	$$⊢w=W\to \mathrm{ocH}\left(K\right)\left(w\right)=O$$
29	28	fveq1d	$$⊢w=W\to \mathrm{ocH}\left(K\right)\left(w\right)\left(\left\{x\right\}\right)=O\left(\left\{x\right\}\right)$$
30	16	fveq2d	$$⊢w=W\to {+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}={+}_U$$
31	30 5	eqtr4di	$$⊢w=W\to {+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}=\underset{\dot{}}{+}$$
32		eqidd	$$⊢w=W\to t=t$$
33	16	fveq2d	$$⊢w=W\to {\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}={\cdot }_U$$
34	33 6	eqtr4di	$$⊢w=W\to {\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}=\underset{\dot{}}{·}$$
35	34	oveqd	$$⊢w=W\to j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x=j\underset{\dot{}}{·}x$$
36	31 32 35	oveq123d	$$⊢w=W\to t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)$$
37	36	eqeq2d	$$⊢w=W\to \left(v=t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)\leftrightarrow v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)$$
38	29 37	rexeqbidv	$$⊢w=W\to \left(\exists t\in \mathrm{ocH}\left(K\right)\left(w\right)\left(\left\{x\right\}\right)v=t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)\leftrightarrow \exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)$$
39	26 38	riotaeqbidv	$$⊢w=W\to \left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)}|\exists t\in \mathrm{ocH}\left(K\right)\left(w\right)\left(\left\{x\right\}\right)v=t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)\right)=\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)$$
40	18 39	mpteq12dv	$$⊢w=W\to \left(v\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)}|\exists t\in \mathrm{ocH}\left(K\right)\left(w\right)\left(\left\{x\right\}\right)v=t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)\right)\right)=\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)$$
41	22 40	mpteq12dv	$$⊢w=W\to \left(x\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\setminus \left\{0_{\mathrm{DVecH}\left(K\right)\left(w\right)}\right\}\right)⟼\left(v\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)}|\exists t\in \mathrm{ocH}\left(K\right)\left(w\right)\left(\left\{x\right\}\right)v=t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)\right)\right)\right)=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)$$
42		eqid	$$⊢\left(w\in H⟼\left(x\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\setminus \left\{0_{\mathrm{DVecH}\left(K\right)\left(w\right)}\right\}\right)⟼\left(v\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)}|\exists t\in \mathrm{ocH}\left(K\right)\left(w\right)\left(\left\{x\right\}\right)v=t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)\right)\right)\right)\right)=\left(w\in H⟼\left(x\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\setminus \left\{0_{\mathrm{DVecH}\left(K\right)\left(w\right)}\right\}\right)⟼\left(v\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)}|\exists t\in \mathrm{ocH}\left(K\right)\left(w\right)\left(\left\{x\right\}\right)v=t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)\right)\right)\right)\right)$$
43	4	fvexi	$$⊢V\in \mathrm{V}$$
44	43	difexi	$$⊢V\setminus \left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
45	44	mptex	$$⊢\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)\in \mathrm{V}$$
46	41 42 45	fvmpt	$$⊢W\in H\to \left(w\in H⟼\left(x\in \left({\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\setminus \left\{0_{\mathrm{DVecH}\left(K\right)\left(w\right)}\right\}\right)⟼\left(v\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\left(\iota j\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)}|\exists t\in \mathrm{ocH}\left(K\right)\left(w\right)\left(\left\{x\right\}\right)v=t{+}_{\mathrm{DVecH}\left(K\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(K\right)\left(w\right)}x\right)\right)\right)\right)\right)\left(W\right)=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)$$
47	14 46	sylan9eq	$$⊢\left(K\in A\wedge W\in H\right)\to M=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)$$
48	11 47	syl	$$⊢\phi \to M=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota j\in R|\exists t\in O\left(\left\{x\right\}\right)v=t\underset{\dot{}}{+}\left(j\underset{\dot{}}{·}x\right)\right)\right)\right)$$