Definition df-hvmap

Description: Extend class notation with a map from each nonzero vector x to a unique nonzero functional in the closed kernel dual space. (We could extend it to include the zero vector, but that is unnecessary for our purposes.) TODO: This pattern is used several times earlier, e.g., lcf1o , dochfl1 - should we update those to use this definition? (Contributed by NM, 23-Mar-2015)

	Ref	Expression
Assertion	df-hvmap	$$⊢\mathrm{HVMap}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\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)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chvm	$$class\mathrm{HVMap}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vw	$$setvarw$$
4		clh	$$class\mathrm{LHyp}$$
5	1	cv	$$setvark$$
6	5 4	cfv	$$class\mathrm{LHyp}\left(k\right)$$
7		vx	$$setvarx$$
8		cbs	$$class\mathrm{Base}$$
9		cdvh	$$class\mathrm{DVecH}$$
10	5 9	cfv	$$class\mathrm{DVecH}\left(k\right)$$
11	3	cv	$$setvarw$$
12	11 10	cfv	$$class\mathrm{DVecH}\left(k\right)\left(w\right)$$
13	12 8	cfv	$$class{\mathrm{Base}}_{\mathrm{DVecH}\left(k\right)\left(w\right)}$$
14		c0g	$$class{0}_{𝑔}$$
15	12 14	cfv	$$class{0}_{\mathrm{DVecH}\left(k\right)\left(w\right)}$$
16	15	csn	$$class\left\{0_{\mathrm{DVecH}\left(k\right)\left(w\right)}\right\}$$
17	13 16	cdif	$$class\left({\mathrm{Base}}_{\mathrm{DVecH}\left(k\right)\left(w\right)}\setminus \left\{0_{\mathrm{DVecH}\left(k\right)\left(w\right)}\right\}\right)$$
18		vv	$$setvarv$$
19		vj	$$setvarj$$
20		csca	$$class\mathrm{Scalar}$$
21	12 20	cfv	$$class\mathrm{Scalar}\left(\mathrm{DVecH}\left(k\right)\left(w\right)\right)$$
22	21 8	cfv	$$class{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(k\right)\left(w\right)\right)}$$
23		vt	$$setvart$$
24		coch	$$class\mathrm{ocH}$$
25	5 24	cfv	$$class\mathrm{ocH}\left(k\right)$$
26	11 25	cfv	$$class\mathrm{ocH}\left(k\right)\left(w\right)$$
27	7	cv	$$setvarx$$
28	27	csn	$$class\left\{x\right\}$$
29	28 26	cfv	$$class\mathrm{ocH}\left(k\right)\left(w\right)\left(\left\{x\right\}\right)$$
30	18	cv	$$setvarv$$
31	23	cv	$$setvart$$
32		cplusg	$$class{+}_{𝑔}$$
33	12 32	cfv	$$class{+}_{\mathrm{DVecH}\left(k\right)\left(w\right)}$$
34	19	cv	$$setvarj$$
35		cvsca	$$class{\cdot }_{𝑠}$$
36	12 35	cfv	$$class{\cdot }_{\mathrm{DVecH}\left(k\right)\left(w\right)}$$
37	34 27 36	co	$$class\left(j{\cdot }_{\mathrm{DVecH}\left(k\right)\left(w\right)}x\right)$$
38	31 37 33	co	$$class\left(t{+}_{\mathrm{DVecH}\left(k\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(k\right)\left(w\right)}x\right)\right)$$
39	30 38	wceq	$$wffv=t{+}_{\mathrm{DVecH}\left(k\right)\left(w\right)}\left(j{\cdot }_{\mathrm{DVecH}\left(k\right)\left(w\right)}x\right)$$
40	39 23 29	wrex	$$wff\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)$$
41	40 19 22	crio	$$class\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)$$
42	18 13 41	cmpt	$$class\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)$$
43	7 17 42	cmpt	$$class\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)$$
44	3 6 43	cmpt	$$class\left(w\in \mathrm{LHyp}\left(k\right)⟼\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)$$
45	1 2 44	cmpt	$$class\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\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)\right)$$
46	0 45	wceq	$$wff\mathrm{HVMap}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\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)\right)$$