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 36744
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 36743 . 2 class HLHil
2 vk . . 3 setvar 𝑘
3 cvv 3190 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1479 . . . . 5 class 𝑘
6 clh 34789 . . . . 5 class LHyp
75, 6cfv 5857 . . . 4 class (LHyp‘𝑘)
8 vu . . . . 5 setvar 𝑢
94cv 1479 . . . . . 6 class 𝑤
10 cdvh 35886 . . . . . . 7 class DVecH
115, 10cfv 5857 . . . . . 6 class (DVecH‘𝑘)
129, 11cfv 5857 . . . . 5 class ((DVecH‘𝑘)‘𝑤)
13 vv . . . . . 6 setvar 𝑣
148cv 1479 . . . . . . 7 class 𝑢
15 cbs 15800 . . . . . . 7 class Base
1614, 15cfv 5857 . . . . . 6 class (Base‘𝑢)
17 cnx 15797 . . . . . . . . . 10 class ndx
1817, 15cfv 5857 . . . . . . . . 9 class (Base‘ndx)
1913cv 1479 . . . . . . . . 9 class 𝑣
2018, 19cop 4161 . . . . . . . 8 class ⟨(Base‘ndx), 𝑣
21 cplusg 15881 . . . . . . . . . 10 class +g
2217, 21cfv 5857 . . . . . . . . 9 class (+g‘ndx)
2314, 21cfv 5857 . . . . . . . . 9 class (+g𝑢)
2422, 23cop 4161 . . . . . . . 8 class ⟨(+g‘ndx), (+g𝑢)⟩
25 csca 15884 . . . . . . . . . 10 class Scalar
2617, 25cfv 5857 . . . . . . . . 9 class (Scalar‘ndx)
27 cedring 35560 . . . . . . . . . . . 12 class EDRing
285, 27cfv 5857 . . . . . . . . . . 11 class (EDRing‘𝑘)
299, 28cfv 5857 . . . . . . . . . 10 class ((EDRing‘𝑘)‘𝑤)
30 cstv 15883 . . . . . . . . . . . 12 class *𝑟
3117, 30cfv 5857 . . . . . . . . . . 11 class (*𝑟‘ndx)
32 chg 36694 . . . . . . . . . . . . 13 class HGMap
335, 32cfv 5857 . . . . . . . . . . . 12 class (HGMap‘𝑘)
349, 33cfv 5857 . . . . . . . . . . 11 class ((HGMap‘𝑘)‘𝑤)
3531, 34cop 4161 . . . . . . . . . 10 class ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩
36 csts 15798 . . . . . . . . . 10 class sSet
3729, 35, 36co 6615 . . . . . . . . 9 class (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)
3826, 37cop 4161 . . . . . . . 8 class ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩
3920, 24, 38ctp 4159 . . . . . . 7 class {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩}
40 cvsca 15885 . . . . . . . . . 10 class ·𝑠
4117, 40cfv 5857 . . . . . . . . 9 class ( ·𝑠 ‘ndx)
4214, 40cfv 5857 . . . . . . . . 9 class ( ·𝑠𝑢)
4341, 42cop 4161 . . . . . . . 8 class ⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩
44 cip 15886 . . . . . . . . . 10 class ·𝑖
4517, 44cfv 5857 . . . . . . . . 9 class (·𝑖‘ndx)
46 vx . . . . . . . . . 10 setvar 𝑥
47 vy . . . . . . . . . 10 setvar 𝑦
4846cv 1479 . . . . . . . . . . 11 class 𝑥
4947cv 1479 . . . . . . . . . . . 12 class 𝑦
50 chdma 36601 . . . . . . . . . . . . . 14 class HDMap
515, 50cfv 5857 . . . . . . . . . . . . 13 class (HDMap‘𝑘)
529, 51cfv 5857 . . . . . . . . . . . 12 class ((HDMap‘𝑘)‘𝑤)
5349, 52cfv 5857 . . . . . . . . . . 11 class (((HDMap‘𝑘)‘𝑤)‘𝑦)
5448, 53cfv 5857 . . . . . . . . . 10 class ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥)
5546, 47, 19, 19, 54cmpt2 6617 . . . . . . . . 9 class (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))
5645, 55cop 4161 . . . . . . . 8 class ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩
5743, 56cpr 4157 . . . . . . 7 class {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩}
5839, 57cun 3558 . . . . . 6 class ({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})
5913, 16, 58csb 3519 . . . . 5 class (Base‘𝑢) / 𝑣({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})
608, 12, 59csb 3519 . . . 4 class ((DVecH‘𝑘)‘𝑤) / 𝑢(Base‘𝑢) / 𝑣({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})
614, 7, 60cmpt 4683 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ((DVecH‘𝑘)‘𝑤) / 𝑢(Base‘𝑢) / 𝑣({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩}))
622, 3, 61cmpt 4683 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ((DVecH‘𝑘)‘𝑤) / 𝑢(Base‘𝑢) / 𝑣({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥𝑣, 𝑦𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})))
631, 62wceq 1480 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  36745
  Copyright terms: Public domain W3C validator