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

Definition df-hgmap 35997
Description: Define map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
Assertion
Ref Expression
df-hgmap HGMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎[((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))))}))
Distinct variable group:   𝑎,𝑏,𝑘,𝑚,𝑢,𝑣,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-hgmap
StepHypRef Expression
1 chg 35996 . 2 class HGMap
2 vk . . 3 setvar 𝑘
3 cvv 3172 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1473 . . . . 5 class 𝑘
6 clh 34091 . . . . 5 class LHyp
75, 6cfv 5790 . . . 4 class (LHyp‘𝑘)
8 va . . . . . . . . . 10 setvar 𝑎
98cv 1473 . . . . . . . . 9 class 𝑎
10 vx . . . . . . . . . 10 setvar 𝑥
11 vb . . . . . . . . . . 11 setvar 𝑏
1211cv 1473 . . . . . . . . . 10 class 𝑏
1310cv 1473 . . . . . . . . . . . . . . 15 class 𝑥
14 vv . . . . . . . . . . . . . . . 16 setvar 𝑣
1514cv 1473 . . . . . . . . . . . . . . 15 class 𝑣
16 vu . . . . . . . . . . . . . . . . 17 setvar 𝑢
1716cv 1473 . . . . . . . . . . . . . . . 16 class 𝑢
18 cvsca 15718 . . . . . . . . . . . . . . . 16 class ·𝑠
1917, 18cfv 5790 . . . . . . . . . . . . . . 15 class ( ·𝑠𝑢)
2013, 15, 19co 6527 . . . . . . . . . . . . . 14 class (𝑥( ·𝑠𝑢)𝑣)
21 vm . . . . . . . . . . . . . . 15 setvar 𝑚
2221cv 1473 . . . . . . . . . . . . . 14 class 𝑚
2320, 22cfv 5790 . . . . . . . . . . . . 13 class (𝑚‘(𝑥( ·𝑠𝑢)𝑣))
24 vy . . . . . . . . . . . . . . 15 setvar 𝑦
2524cv 1473 . . . . . . . . . . . . . 14 class 𝑦
2615, 22cfv 5790 . . . . . . . . . . . . . 14 class (𝑚𝑣)
274cv 1473 . . . . . . . . . . . . . . . 16 class 𝑤
28 clcd 35696 . . . . . . . . . . . . . . . . 17 class LCDual
295, 28cfv 5790 . . . . . . . . . . . . . . . 16 class (LCDual‘𝑘)
3027, 29cfv 5790 . . . . . . . . . . . . . . 15 class ((LCDual‘𝑘)‘𝑤)
3130, 18cfv 5790 . . . . . . . . . . . . . 14 class ( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))
3225, 26, 31co 6527 . . . . . . . . . . . . 13 class (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))
3323, 32wceq 1474 . . . . . . . . . . . 12 wff (𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))
34 cbs 15641 . . . . . . . . . . . . 13 class Base
3517, 34cfv 5790 . . . . . . . . . . . 12 class (Base‘𝑢)
3633, 14, 35wral 2895 . . . . . . . . . . 11 wff 𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))
3736, 24, 12crio 6488 . . . . . . . . . 10 class (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣)))
3810, 12, 37cmpt 4637 . . . . . . . . 9 class (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))))
399, 38wcel 1976 . . . . . . . 8 wff 𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))))
40 chdma 35903 . . . . . . . . . 10 class HDMap
415, 40cfv 5790 . . . . . . . . 9 class (HDMap‘𝑘)
4227, 41cfv 5790 . . . . . . . 8 class ((HDMap‘𝑘)‘𝑤)
4339, 21, 42wsbc 3401 . . . . . . 7 wff [((HDMap‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))))
44 csca 15717 . . . . . . . . 9 class Scalar
4517, 44cfv 5790 . . . . . . . 8 class (Scalar‘𝑢)
4645, 34cfv 5790 . . . . . . 7 class (Base‘(Scalar‘𝑢))
4743, 11, 46wsbc 3401 . . . . . 6 wff [(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))))
48 cdvh 35188 . . . . . . . 8 class DVecH
495, 48cfv 5790 . . . . . . 7 class (DVecH‘𝑘)
5027, 49cfv 5790 . . . . . 6 class ((DVecH‘𝑘)‘𝑤)
5147, 16, 50wsbc 3401 . . . . 5 wff [((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))))
5251, 8cab 2595 . . . 4 class {𝑎[((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))))}
534, 7, 52cmpt 4637 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎[((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))))})
542, 3, 53cmpt 4637 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎[((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))))}))
551, 54wceq 1474 1 wff HGMap = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑎[((DVecH‘𝑘)‘𝑤) / 𝑢][(Base‘(Scalar‘𝑢)) / 𝑏][((HDMap‘𝑘)‘𝑤) / 𝑚]𝑎 ∈ (𝑥𝑏 ↦ (𝑦𝑏𝑣 ∈ (Base‘𝑢)(𝑚‘(𝑥( ·𝑠𝑢)𝑣)) = (𝑦( ·𝑠 ‘((LCDual‘𝑘)‘𝑤))(𝑚𝑣))))}))
Colors of variables: wff setvar class
This definition is referenced by:  hgmapffval  35998
  Copyright terms: Public domain W3C validator