Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-hdmap Structured version   Visualization version   GIF version

Definition df-hdmap 36102
Description: Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 36137 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
StepHypRef Expression
1 chdma 36100 . 2 class HDMap
2 vk . . 3 setvar 𝑘
3 cvv 3173 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1474 . . . . 5 class 𝑘
6 clh 34288 . . . . 5 class LHyp
75, 6cfv 5804 . . . 4 class (LHyp‘𝑘)
8 va . . . . . . . . . . 11 setvar 𝑎
98cv 1474 . . . . . . . . . 10 class 𝑎
10 vt . . . . . . . . . . 11 setvar 𝑡
11 vv . . . . . . . . . . . 12 setvar 𝑣
1211cv 1474 . . . . . . . . . . 11 class 𝑣
13 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
1413cv 1474 . . . . . . . . . . . . . . . 16 class 𝑧
15 ve . . . . . . . . . . . . . . . . . . . 20 setvar 𝑒
1615cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑒
1716csn 4125 . . . . . . . . . . . . . . . . . 18 class {𝑒}
18 vu . . . . . . . . . . . . . . . . . . . 20 setvar 𝑢
1918cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑢
20 clspn 18792 . . . . . . . . . . . . . . . . . . 19 class LSpan
2119, 20cfv 5804 . . . . . . . . . . . . . . . . . 18 class (LSpan‘𝑢)
2217, 21cfv 5804 . . . . . . . . . . . . . . . . 17 class ((LSpan‘𝑢)‘{𝑒})
2310cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑡
2423csn 4125 . . . . . . . . . . . . . . . . . 18 class {𝑡}
2524, 21cfv 5804 . . . . . . . . . . . . . . . . 17 class ((LSpan‘𝑢)‘{𝑡})
2622, 25cun 3538 . . . . . . . . . . . . . . . 16 class (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡}))
2714, 26wcel 1977 . . . . . . . . . . . . . . 15 wff 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡}))
2827wn 3 . . . . . . . . . . . . . 14 wff ¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡}))
29 vy . . . . . . . . . . . . . . . 16 setvar 𝑦
3029cv 1474 . . . . . . . . . . . . . . 15 class 𝑦
314cv 1474 . . . . . . . . . . . . . . . . . . . . 21 class 𝑤
32 chvm 36063 . . . . . . . . . . . . . . . . . . . . . 22 class HVMap
335, 32cfv 5804 . . . . . . . . . . . . . . . . . . . . 21 class (HVMap‘𝑘)
3431, 33cfv 5804 . . . . . . . . . . . . . . . . . . . 20 class ((HVMap‘𝑘)‘𝑤)
3516, 34cfv 5804 . . . . . . . . . . . . . . . . . . 19 class (((HVMap‘𝑘)‘𝑤)‘𝑒)
3616, 35, 14cotp 4133 . . . . . . . . . . . . . . . . . 18 class 𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧
37 vi . . . . . . . . . . . . . . . . . . 19 setvar 𝑖
3837cv 1474 . . . . . . . . . . . . . . . . . 18 class 𝑖
3936, 38cfv 5804 . . . . . . . . . . . . . . . . 17 class (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩)
4014, 39, 23cotp 4133 . . . . . . . . . . . . . . . 16 class 𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡
4140, 38cfv 5804 . . . . . . . . . . . . . . 15 class (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)
4230, 41wceq 1475 . . . . . . . . . . . . . 14 wff 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)
4328, 42wi 4 . . . . . . . . . . . . 13 wff 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))
4443, 13, 12wral 2896 . . . . . . . . . . . 12 wff 𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))
45 clcd 35893 . . . . . . . . . . . . . . 15 class LCDual
465, 45cfv 5804 . . . . . . . . . . . . . 14 class (LCDual‘𝑘)
4731, 46cfv 5804 . . . . . . . . . . . . 13 class ((LCDual‘𝑘)‘𝑤)
48 cbs 15695 . . . . . . . . . . . . 13 class Base
4947, 48cfv 5804 . . . . . . . . . . . 12 class (Base‘((LCDual‘𝑘)‘𝑤))
5044, 29, 49crio 6510 . . . . . . . . . . 11 class (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))
5110, 12, 50cmpt 4643 . . . . . . . . . 10 class (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
529, 51wcel 1977 . . . . . . . . 9 wff 𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
53 chdma1 36099 . . . . . . . . . . 11 class HDMap1
545, 53cfv 5804 . . . . . . . . . 10 class (HDMap1‘𝑘)
5531, 54cfv 5804 . . . . . . . . 9 class ((HDMap1‘𝑘)‘𝑤)
5652, 37, 55wsbc 3402 . . . . . . . 8 wff [((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
5719, 48cfv 5804 . . . . . . . 8 class (Base‘𝑢)
5856, 11, 57wsbc 3402 . . . . . . 7 wff [(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
59 cdvh 35385 . . . . . . . . 9 class DVecH
605, 59cfv 5804 . . . . . . . 8 class (DVecH‘𝑘)
6131, 60cfv 5804 . . . . . . 7 class ((DVecH‘𝑘)‘𝑤)
6258, 18, 61wsbc 3402 . . . . . 6 wff [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
63 cid 4948 . . . . . . . 8 class I
645, 48cfv 5804 . . . . . . . 8 class (Base‘𝑘)
6563, 64cres 5040 . . . . . . 7 class ( I ↾ (Base‘𝑘))
66 cltrn 34405 . . . . . . . . . 10 class LTrn
675, 66cfv 5804 . . . . . . . . 9 class (LTrn‘𝑘)
6831, 67cfv 5804 . . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
6963, 68cres 5040 . . . . . . 7 class ( I ↾ ((LTrn‘𝑘)‘𝑤))
7065, 69cop 4131 . . . . . 6 class ⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩
7162, 15, 70wsbc 3402 . . . . 5 wff [⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))
7271, 8cab 2596 . . . 4 class {𝑎[⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}
734, 7, 72cmpt 4643 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎[⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})
742, 3, 73cmpt 4643 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎[⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
751, 74wceq 1475 1 wff HDMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎[⟨( I ↾ (Base‘𝑘)), ( I ↾ ((LTrn‘𝑘)‘𝑤))⟩ / 𝑒][((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝑘)‘𝑤) / 𝑖]𝑎 ∈ (𝑡𝑣 ↦ (𝑦 ∈ (Base‘((LCDual‘𝑘)‘𝑤))∀𝑧𝑣𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝑘)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
Colors of variables: wff setvar class
This definition is referenced by:  hdmapffval  36136
  Copyright terms: Public domain W3C validator