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

Definition df-hlhil 37954
Description: Define our final Hilbert space constructed from a Hilbert lattice. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
Assertion
Ref Expression
df-hlhil HLHil = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((DVecH‘𝑘)‘𝑤) / 𝑢(Base‘𝑢) / 𝑣({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})))
Distinct variable group:   𝑤,𝑘,𝑢,𝑣,𝑥,𝑦

Detailed syntax breakdown of Definition df-hlhil
StepHypRef Expression
1 chlh 37953 . 2 class HLHil
2 vk . . 3 setvar 𝑘
3 cvv 3385 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1652 . . . . 5 class 𝑘
6 clh 36005 . . . . 5 class LHyp
75, 6cfv 6101 . . . 4 class (LHyp‘𝑘)
8 vu . . . . 5 setvar 𝑢
94cv 1652 . . . . . 6 class 𝑤
10 cdvh 37099 . . . . . . 7 class DVecH
115, 10cfv 6101 . . . . . 6 class (DVecH‘𝑘)
129, 11cfv 6101 . . . . 5 class ((DVecH‘𝑘)‘𝑤)
13 vv . . . . . 6 setvar 𝑣
148cv 1652 . . . . . . 7 class 𝑢
15 cbs 16184 . . . . . . 7 class Base
1614, 15cfv 6101 . . . . . 6 class (Base‘𝑢)
17 cnx 16181 . . . . . . . . . 10 class ndx
1817, 15cfv 6101 . . . . . . . . 9 class (Base‘ndx)
1913cv 1652 . . . . . . . . 9 class 𝑣
2018, 19cop 4374 . . . . . . . 8 class ⟨(Base‘ndx), 𝑣
21 cplusg 16267 . . . . . . . . . 10 class +g
2217, 21cfv 6101 . . . . . . . . 9 class (+g‘ndx)
2314, 21cfv 6101 . . . . . . . . 9 class (+g𝑢)
2422, 23cop 4374 . . . . . . . 8 class ⟨(+g‘ndx), (+g𝑢)⟩
25 csca 16270 . . . . . . . . . 10 class Scalar
2617, 25cfv 6101 . . . . . . . . 9 class (Scalar‘ndx)
27 cedring 36774 . . . . . . . . . . . 12 class EDRing
285, 27cfv 6101 . . . . . . . . . . 11 class (EDRing‘𝑘)
299, 28cfv 6101 . . . . . . . . . 10 class ((EDRing‘𝑘)‘𝑤)
30 cstv 16269 . . . . . . . . . . . 12 class *𝑟
3117, 30cfv 6101 . . . . . . . . . . 11 class (*𝑟‘ndx)
32 chg 37904 . . . . . . . . . . . . 13 class HGMap
335, 32cfv 6101 . . . . . . . . . . . 12 class (HGMap‘𝑘)
349, 33cfv 6101 . . . . . . . . . . 11 class ((HGMap‘𝑘)‘𝑤)
3531, 34cop 4374 . . . . . . . . . 10 class ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩
36 csts 16182 . . . . . . . . . 10 class sSet
3729, 35, 36co 6878 . . . . . . . . 9 class (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)
3826, 37cop 4374 . . . . . . . 8 class ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩
3920, 24, 38ctp 4372 . . . . . . 7 class {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩}
40 cvsca 16271 . . . . . . . . . 10 class ·𝑠
4117, 40cfv 6101 . . . . . . . . 9 class ( ·𝑠 ‘ndx)
4214, 40cfv 6101 . . . . . . . . 9 class ( ·𝑠𝑢)
4341, 42cop 4374 . . . . . . . 8 class ⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩
44 cip 16272 . . . . . . . . . 10 class ·𝑖
4517, 44cfv 6101 . . . . . . . . 9 class (·𝑖‘ndx)
46 vx . . . . . . . . . 10 setvar 𝑥
47 vy . . . . . . . . . 10 setvar 𝑦
4846cv 1652 . . . . . . . . . . 11 class 𝑥
4947cv 1652 . . . . . . . . . . . 12 class 𝑦
50 chdma 37813 . . . . . . . . . . . . . 14 class HDMap
515, 50cfv 6101 . . . . . . . . . . . . 13 class (HDMap‘𝑘)
529, 51cfv 6101 . . . . . . . . . . . 12 class ((HDMap‘𝑘)‘𝑤)
5349, 52cfv 6101 . . . . . . . . . . 11 class (((HDMap‘𝑘)‘𝑤)‘𝑦)
5448, 53cfv 6101 . . . . . . . . . 10 class ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥)
5546, 47, 19, 19, 54cmpt2 6880 . . . . . . . . 9 class (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))
5645, 55cop 4374 . . . . . . . 8 class ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩
5743, 56cpr 4370 . . . . . . 7 class {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩}
5839, 57cun 3767 . . . . . 6 class ({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})
5913, 16, 58csb 3728 . . . . 5 class (Base‘𝑢) / 𝑣({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})
608, 12, 59csb 3728 . . . 4 class ((DVecH‘𝑘)‘𝑤) / 𝑢(Base‘𝑢) / 𝑣({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})
614, 7, 60cmpt 4922 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ((DVecH‘𝑘)‘𝑤) / 𝑢(Base‘𝑢) / 𝑣({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩}))
622, 3, 61cmpt 4922 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((DVecH‘𝑘)‘𝑤) / 𝑢(Base‘𝑢) / 𝑣({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})))
631, 62wceq 1653 1 wff HLHil = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((DVecH‘𝑘)‘𝑤) / 𝑢(Base‘𝑢) / 𝑣({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})))
Colors of variables: wff setvar class
This definition is referenced by:  hlhilset  37955
  Copyright terms: Public domain W3C validator