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

Definition df-hlhil 32126
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  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  [_ (
( DVecH `  k ) `  w )  /  u ]_ [_ ( Base `  u
)  /  v ]_ ( { <. ( Base `  ndx ) ,  v >. , 
<. ( +g  `  ndx ) ,  ( +g  `  u ) >. ,  <. (Scalar `  ndx ) ,  ( ( ( EDRing `  k
) `  w ) sSet  <.
( * r `  ndx ) ,  ( (HGMap `  k ) `  w
) >. ) >. }  u.  {
<. ( .s `  ndx ) ,  ( .s `  u ) >. ,  <. ( .i `  ndx ) ,  ( x  e.  v ,  y  e.  v  |->  ( ( ( (HDMap `  k ) `  w ) `  y
) `  x )
) >. } ) ) )
Distinct variable group:    w, k, u, v, x, y

Detailed syntax breakdown of Definition df-hlhil
StepHypRef Expression
1 chlh 32125 . 2  class HLHil
2 vk . . 3  set  k
3 cvv 2788 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1622 . . . . 5  class  k
6 clh 30173 . . . . 5  class  LHyp
75, 6cfv 5255 . . . 4  class  ( LHyp `  k )
8 vu . . . . 5  set  u
94cv 1622 . . . . . 6  class  w
10 cdvh 31268 . . . . . . 7  class  DVecH
115, 10cfv 5255 . . . . . 6  class  ( DVecH `  k )
129, 11cfv 5255 . . . . 5  class  ( (
DVecH `  k ) `  w )
13 vv . . . . . 6  set  v
148cv 1622 . . . . . . 7  class  u
15 cbs 13148 . . . . . . 7  class  Base
1614, 15cfv 5255 . . . . . 6  class  ( Base `  u )
17 cnx 13145 . . . . . . . . . 10  class  ndx
1817, 15cfv 5255 . . . . . . . . 9  class  ( Base `  ndx )
1913cv 1622 . . . . . . . . 9  class  v
2018, 19cop 3643 . . . . . . . 8  class  <. ( Base `  ndx ) ,  v >.
21 cplusg 13208 . . . . . . . . . 10  class  +g
2217, 21cfv 5255 . . . . . . . . 9  class  ( +g  ` 
ndx )
2314, 21cfv 5255 . . . . . . . . 9  class  ( +g  `  u )
2422, 23cop 3643 . . . . . . . 8  class  <. ( +g  `  ndx ) ,  ( +g  `  u
) >.
25 csca 13211 . . . . . . . . . 10  class Scalar
2617, 25cfv 5255 . . . . . . . . 9  class  (Scalar `  ndx )
27 cedring 30942 . . . . . . . . . . . 12  class  EDRing
285, 27cfv 5255 . . . . . . . . . . 11  class  ( EDRing `  k )
299, 28cfv 5255 . . . . . . . . . 10  class  ( (
EDRing `  k ) `  w )
30 cstv 13210 . . . . . . . . . . . 12  class  * r
3117, 30cfv 5255 . . . . . . . . . . 11  class  ( * r `  ndx )
32 chg 32076 . . . . . . . . . . . . 13  class HGMap
335, 32cfv 5255 . . . . . . . . . . . 12  class  (HGMap `  k )
349, 33cfv 5255 . . . . . . . . . . 11  class  ( (HGMap `  k ) `  w
)
3531, 34cop 3643 . . . . . . . . . 10  class  <. (
* r `  ndx ) ,  ( (HGMap `  k ) `  w
) >.
36 csts 13146 . . . . . . . . . 10  class sSet
3729, 35, 36co 5858 . . . . . . . . 9  class  ( ( ( EDRing `  k ) `  w ) sSet  <. (
* r `  ndx ) ,  ( (HGMap `  k ) `  w
) >. )
3826, 37cop 3643 . . . . . . . 8  class  <. (Scalar ` 
ndx ) ,  ( ( ( EDRing `  k
) `  w ) sSet  <.
( * r `  ndx ) ,  ( (HGMap `  k ) `  w
) >. ) >.
3920, 24, 38ctp 3642 . . . . . . 7  class  { <. (
Base `  ndx ) ,  v >. ,  <. ( +g  `  ndx ) ,  ( +g  `  u
) >. ,  <. (Scalar ` 
ndx ) ,  ( ( ( EDRing `  k
) `  w ) sSet  <.
( * r `  ndx ) ,  ( (HGMap `  k ) `  w
) >. ) >. }
40 cvsca 13212 . . . . . . . . . 10  class  .s
4117, 40cfv 5255 . . . . . . . . 9  class  ( .s
`  ndx )
4214, 40cfv 5255 . . . . . . . . 9  class  ( .s
`  u )
4341, 42cop 3643 . . . . . . . 8  class  <. ( .s `  ndx ) ,  ( .s `  u
) >.
44 cip 13213 . . . . . . . . . 10  class  .i
4517, 44cfv 5255 . . . . . . . . 9  class  ( .i
`  ndx )
46 vx . . . . . . . . . 10  set  x
47 vy . . . . . . . . . 10  set  y
4846cv 1622 . . . . . . . . . . 11  class  x
4947cv 1622 . . . . . . . . . . . 12  class  y
50 chdma 31983 . . . . . . . . . . . . . 14  class HDMap
515, 50cfv 5255 . . . . . . . . . . . . 13  class  (HDMap `  k )
529, 51cfv 5255 . . . . . . . . . . . 12  class  ( (HDMap `  k ) `  w
)
5349, 52cfv 5255 . . . . . . . . . . 11  class  ( ( (HDMap `  k ) `  w ) `  y
)
5448, 53cfv 5255 . . . . . . . . . 10  class  ( ( ( (HDMap `  k
) `  w ) `  y ) `  x
)
5546, 47, 19, 19, 54cmpt2 5860 . . . . . . . . 9  class  ( x  e.  v ,  y  e.  v  |->  ( ( ( (HDMap `  k
) `  w ) `  y ) `  x
) )
5645, 55cop 3643 . . . . . . . 8  class  <. ( .i `  ndx ) ,  ( x  e.  v ,  y  e.  v 
|->  ( ( ( (HDMap `  k ) `  w
) `  y ) `  x ) ) >.
5743, 56cpr 3641 . . . . . . 7  class  { <. ( .s `  ndx ) ,  ( .s `  u ) >. ,  <. ( .i `  ndx ) ,  ( x  e.  v ,  y  e.  v  |->  ( ( ( (HDMap `  k ) `  w ) `  y
) `  x )
) >. }
5839, 57cun 3150 . . . . . 6  class  ( {
<. ( Base `  ndx ) ,  v >. , 
<. ( +g  `  ndx ) ,  ( +g  `  u ) >. ,  <. (Scalar `  ndx ) ,  ( ( ( EDRing `  k
) `  w ) sSet  <.
( * r `  ndx ) ,  ( (HGMap `  k ) `  w
) >. ) >. }  u.  {
<. ( .s `  ndx ) ,  ( .s `  u ) >. ,  <. ( .i `  ndx ) ,  ( x  e.  v ,  y  e.  v  |->  ( ( ( (HDMap `  k ) `  w ) `  y
) `  x )
) >. } )
5913, 16, 58csb 3081 . . . . 5  class  [_ ( Base `  u )  / 
v ]_ ( { <. (
Base `  ndx ) ,  v >. ,  <. ( +g  `  ndx ) ,  ( +g  `  u
) >. ,  <. (Scalar ` 
ndx ) ,  ( ( ( EDRing `  k
) `  w ) sSet  <.
( * r `  ndx ) ,  ( (HGMap `  k ) `  w
) >. ) >. }  u.  {
<. ( .s `  ndx ) ,  ( .s `  u ) >. ,  <. ( .i `  ndx ) ,  ( x  e.  v ,  y  e.  v  |->  ( ( ( (HDMap `  k ) `  w ) `  y
) `  x )
) >. } )
608, 12, 59csb 3081 . . . 4  class  [_ (
( DVecH `  k ) `  w )  /  u ]_ [_ ( Base `  u
)  /  v ]_ ( { <. ( Base `  ndx ) ,  v >. , 
<. ( +g  `  ndx ) ,  ( +g  `  u ) >. ,  <. (Scalar `  ndx ) ,  ( ( ( EDRing `  k
) `  w ) sSet  <.
( * r `  ndx ) ,  ( (HGMap `  k ) `  w
) >. ) >. }  u.  {
<. ( .s `  ndx ) ,  ( .s `  u ) >. ,  <. ( .i `  ndx ) ,  ( x  e.  v ,  y  e.  v  |->  ( ( ( (HDMap `  k ) `  w ) `  y
) `  x )
) >. } )
614, 7, 60cmpt 4077 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  [_ ( ( DVecH `  k ) `  w
)  /  u ]_ [_ ( Base `  u
)  /  v ]_ ( { <. ( Base `  ndx ) ,  v >. , 
<. ( +g  `  ndx ) ,  ( +g  `  u ) >. ,  <. (Scalar `  ndx ) ,  ( ( ( EDRing `  k
) `  w ) sSet  <.
( * r `  ndx ) ,  ( (HGMap `  k ) `  w
) >. ) >. }  u.  {
<. ( .s `  ndx ) ,  ( .s `  u ) >. ,  <. ( .i `  ndx ) ,  ( x  e.  v ,  y  e.  v  |->  ( ( ( (HDMap `  k ) `  w ) `  y
) `  x )
) >. } ) )
622, 3, 61cmpt 4077 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  [_ ( ( DVecH `  k ) `  w
)  /  u ]_ [_ ( Base `  u
)  /  v ]_ ( { <. ( Base `  ndx ) ,  v >. , 
<. ( +g  `  ndx ) ,  ( +g  `  u ) >. ,  <. (Scalar `  ndx ) ,  ( ( ( EDRing `  k
) `  w ) sSet  <.
( * r `  ndx ) ,  ( (HGMap `  k ) `  w
) >. ) >. }  u.  {
<. ( .s `  ndx ) ,  ( .s `  u ) >. ,  <. ( .i `  ndx ) ,  ( x  e.  v ,  y  e.  v  |->  ( ( ( (HDMap `  k ) `  w ) `  y
) `  x )
) >. } ) ) )
631, 62wceq 1623 1  wff HLHil  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  [_ (
( DVecH `  k ) `  w )  /  u ]_ [_ ( Base `  u
)  /  v ]_ ( { <. ( Base `  ndx ) ,  v >. , 
<. ( +g  `  ndx ) ,  ( +g  `  u ) >. ,  <. (Scalar `  ndx ) ,  ( ( ( EDRing `  k
) `  w ) sSet  <.
( * r `  ndx ) ,  ( (HGMap `  k ) `  w
) >. ) >. }  u.  {
<. ( .s `  ndx ) ,  ( .s `  u ) >. ,  <. ( .i `  ndx ) ,  ( x  e.  v ,  y  e.  v  |->  ( ( ( (HDMap `  k ) `  w ) `  y
) `  x )
) >. } ) ) )
Colors of variables: wff set class
This definition is referenced by:  hlhilset  32127
  Copyright terms: Public domain W3C validator