Definition df-hvmap 40616

Description: Extend class notation with a map from each nonzero vector 𝑥 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 40410, dochfl1 40335- should we update those to use this definition? (Contributed by NM, 23-Mar-2015.)

Assertion

Ref	Expression
df-hvmap	⊢ HVMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))))

Distinct variable group:   𝑤,𝑘,𝑥,𝑣,𝑗,𝑡

Detailed syntax breakdown of Definition df-hvmap

Step	Hyp	Ref	Expression
1		chvm 40615	. 2 class HVMap
2		vk	. . 3 setvar 𝑘
3		cvv 3474	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1540	. . . . 5 class 𝑘
6		clh 38843	. . . . 5 class LHyp
7	5, 6	cfv 6540	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1540	. . . . . . . 8 class 𝑤
10		cdvh 39937	. . . . . . . . 9 class DVecH
11	5, 10	cfv 6540	. . . . . . . 8 class (DVecH‘𝑘)
12	9, 11	cfv 6540	. . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
13		cbs 17140	. . . . . . 7 class Base
14	12, 13	cfv 6540	. . . . . 6 class (Base‘((DVecH‘𝑘)‘𝑤))
15		c0g 17381	. . . . . . . 8 class 0g
16	12, 15	cfv 6540	. . . . . . 7 class (0g‘((DVecH‘𝑘)‘𝑤))
17	16	csn 4627	. . . . . 6 class {(0g‘((DVecH‘𝑘)‘𝑤))}
18	14, 17	cdif 3944	. . . . 5 class ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))})
19		vv	. . . . . 6 setvar 𝑣
20	19	cv 1540	. . . . . . . . 9 class 𝑣
21		vt	. . . . . . . . . . 11 setvar 𝑡
22	21	cv 1540	. . . . . . . . . 10 class 𝑡
23		vj	. . . . . . . . . . . 12 setvar 𝑗
24	23	cv 1540	. . . . . . . . . . 11 class 𝑗
25	8	cv 1540	. . . . . . . . . . 11 class 𝑥
26		cvsca 17197	. . . . . . . . . . . 12 class ·𝑠
27	12, 26	cfv 6540	. . . . . . . . . . 11 class ( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))
28	24, 25, 27	co 7405	. . . . . . . . . 10 class (𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)
29		cplusg 17193	. . . . . . . . . . 11 class +g
30	12, 29	cfv 6540	. . . . . . . . . 10 class (+g‘((DVecH‘𝑘)‘𝑤))
31	22, 28, 30	co 7405	. . . . . . . . 9 class (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
32	20, 31	wceq 1541	. . . . . . . 8 wff 𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
33	25	csn 4627	. . . . . . . . 9 class {𝑥}
34		coch 40206	. . . . . . . . . . 11 class ocH
35	5, 34	cfv 6540	. . . . . . . . . 10 class (ocH‘𝑘)
36	9, 35	cfv 6540	. . . . . . . . 9 class ((ocH‘𝑘)‘𝑤)
37	33, 36	cfv 6540	. . . . . . . 8 class (((ocH‘𝑘)‘𝑤)‘{𝑥})
38	32, 21, 37	wrex 3070	. . . . . . 7 wff ∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))
39		csca 17196	. . . . . . . . 9 class Scalar
40	12, 39	cfv 6540	. . . . . . . 8 class (Scalar‘((DVecH‘𝑘)‘𝑤))
41	40, 13	cfv 6540	. . . . . . 7 class (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))
42	38, 23, 41	crio 7360	. . . . . 6 class (℩𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))
43	19, 14, 42	cmpt 5230	. . . . 5 class (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))))
44	8, 18, 43	cmpt 5230	. . . 4 class (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))
45	4, 7, 44	cmpt 5230	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥))))))
46	2, 3, 45	cmpt 5230	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))))
47	1, 46	wceq 1541	1 wff HVMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ ((Base‘((DVecH‘𝑘)‘𝑤)) ∖ {(0g‘((DVecH‘𝑘)‘𝑤))}) ↦ (𝑣 ∈ (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (℩𝑗 ∈ (Base‘(Scalar‘((DVecH‘𝑘)‘𝑤)))∃𝑡 ∈ (((ocH‘𝑘)‘𝑤)‘{𝑥})𝑣 = (𝑡(+g‘((DVecH‘𝑘)‘𝑤))(𝑗( ·𝑠 ‘((DVecH‘𝑘)‘𝑤))𝑥)))))))

This definition is referenced by:  hvmapffval  40617