Definition df-hdmap 39735

Description: Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 39768 description for more details. (Contributed by NM, 15-May-2015.)

Assertion

Ref	Expression
df-hdmap	⊢ HDMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))

Distinct variable group:   𝑒,𝑎,𝑖,𝑘,𝑡,𝑢,𝑣,𝑤,𝑦,𝑧

Detailed syntax breakdown of Definition df-hdmap

Step	Hyp	Ref	Expression
1		chdma 39733	. 2 class HDMap
2		vk	. . 3 setvar 𝑘
3		cvv 3422	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1538	. . . . 5 class 𝑘
6		clh 37925	. . . . 5 class LHyp
7	5, 6	cfv 6418	. . . 4 class (LHyp‘𝑘)
8		va	. . . . . . . . . . 11 setvar 𝑎
9	8	cv 1538	. . . . . . . . . 10 class 𝑎
10		vt	. . . . . . . . . . 11 setvar 𝑡
11		vv	. . . . . . . . . . . 12 setvar 𝑣
12	11	cv 1538	. . . . . . . . . . 11 class 𝑣
13		vz	. . . . . . . . . . . . . . . . 17 setvar 𝑧
14	13	cv 1538	. . . . . . . . . . . . . . . 16 class 𝑧
15		ve	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑒
16	15	cv 1538	. . . . . . . . . . . . . . . . . . 19 class 𝑒
17	16	csn 4558	. . . . . . . . . . . . . . . . . 18 class {𝑒}
18		vu	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑢
19	18	cv 1538	. . . . . . . . . . . . . . . . . . 19 class 𝑢
20		clspn 20148	. . . . . . . . . . . . . . . . . . 19 class LSpan
21	19, 20	cfv 6418	. . . . . . . . . . . . . . . . . 18 class (LSpan‘𝑢)
22	17, 21	cfv 6418	. . . . . . . . . . . . . . . . 17 class ((LSpan‘𝑢)‘{𝑒})
23	10	cv 1538	. . . . . . . . . . . . . . . . . . 19 class 𝑡
24	23	csn 4558	. . . . . . . . . . . . . . . . . 18 class {𝑡}
25	24, 21	cfv 6418	. . . . . . . . . . . . . . . . 17 class ((LSpan‘𝑢)‘{𝑡})
26	22, 25	cun 3881	. . . . . . . . . . . . . . . 16 class (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡}))
27	14, 26	wcel 2108	. . . . . . . . . . . . . . 15 wff 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡}))
28	27	wn 3	. . . . . . . . . . . . . 14 wff ¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡}))
29		vy	. . . . . . . . . . . . . . . 16 setvar 𝑦
30	29	cv 1538	. . . . . . . . . . . . . . 15 class 𝑦
31	4	cv 1538	. . . . . . . . . . . . . . . . . . . . 21 class 𝑤
32		chvm 39697	. . . . . . . . . . . . . . . . . . . . . 22 class HVMap
33	5, 32	cfv 6418	. . . . . . . . . . . . . . . . . . . . 21 class (HVMap‘𝑘)
34	31, 33	cfv 6418	. . . . . . . . . . . . . . . . . . . 20 class ((HVMap‘𝑘)‘𝑤)
35	16, 34	cfv 6418	. . . . . . . . . . . . . . . . . . 19 class (((HVMap‘𝑘)‘𝑤)‘𝑒)
36	16, 35, 14	cotp 4566	. . . . . . . . . . . . . . . . . 18 class ⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩
37		vi	. . . . . . . . . . . . . . . . . . 19 setvar 𝑖
38	37	cv 1538	. . . . . . . . . . . . . . . . . 18 class 𝑖
39	36, 38	cfv 6418	. . . . . . . . . . . . . . . . 17 class (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩)
40	14, 39, 23	cotp 4566	. . . . . . . . . . . . . . . 16 class ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩
41	40, 38	cfv 6418	. . . . . . . . . . . . . . 15 class (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)
42	30, 41	wceq 1539	. . . . . . . . . . . . . 14 wff 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)
43	28, 42	wi 4	. . . . . . . . . . . . 13 wff (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))
44	43, 13, 12	wral 3063	. . . . . . . . . . . 12 wff ∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))
45		clcd 39527	. . . . . . . . . . . . . . 15 class LCDual
46	5, 45	cfv 6418	. . . . . . . . . . . . . 14 class (LCDual‘𝑘)
47	31, 46	cfv 6418	. . . . . . . . . . . . 13 class ((LCDual‘𝑘)‘𝑤)
48		cbs 16840	. . . . . . . . . . . . 13 class Base
49	47, 48	cfv 6418	. . . . . . . . . . . 12 class (Base‘((LCDual‘𝑘)‘𝑤))
50	44, 29, 49	crio 7211	. . . . . . . . . . 11 class (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))
51	10, 12, 50	cmpt 5153	. . . . . . . . . 10 class (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
52	9, 51	wcel 2108	. . . . . . . . 9 wff 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
53		chdma1 39732	. . . . . . . . . . 11 class HDMap1
54	5, 53	cfv 6418	. . . . . . . . . 10 class (HDMap1‘𝑘)
55	31, 54	cfv 6418	. . . . . . . . 9 class ((HDMap1‘𝑘)‘𝑤)
56	52, 37, 55	wsbc 3711	. . . . . . . 8 wff [((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
57	19, 48	cfv 6418	. . . . . . . 8 class (Base‘𝑢)
58	56, 11, 57	wsbc 3711	. . . . . . 7 wff [(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
59		cdvh 39019	. . . . . . . . 9 class DVecH
60	5, 59	cfv 6418	. . . . . . . 8 class (DVecH‘𝑘)
61	31, 60	cfv 6418	. . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
62	58, 18, 61	wsbc 3711	. . . . . 6 wff [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
63		cid 5479	. . . . . . . 8 class I
64	5, 48	cfv 6418	. . . . . . . 8 class (Base‘𝑘)
65	63, 64	cres 5582	. . . . . . 7 class ( I ↾ (Base‘𝑘))
66		cltrn 38042	. . . . . . . . . 10 class LTrn
67	5, 66	cfv 6418	. . . . . . . . 9 class (LTrn‘𝑘)
68	31, 67	cfv 6418	. . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
69	63, 68	cres 5582	. . . . . . 7 class ( I ↾ ((LTrn‘𝑘)‘𝑤))
70	65, 69	cop 4564	. . . . . 6 class ⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩
71	62, 15, 70	wsbc 3711	. . . . 5 wff [⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
72	71, 8	cab 2715	. . . 4 class {𝑎 ∣ [⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}
73	4, 7, 72	cmpt 5153	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})
74	2, 3, 73	cmpt 5153	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
75	1, 74	wceq 1539	1 wff HDMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))

This definition is referenced by:  hdmapffval  39767