Metamath Proof Explorer

Definition df-hlhil

Description: Define our final Hilbert space constructed from a Hilbert lattice. (Contributed by NM, 21-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

Ref Expression
Assertion 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 ) ) >. } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlh 
 |-  HLHil
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 cdvh 
 |-  DVecH
8 5 7 cfv 
 |-  ( DVecH ` k )
9 3 cv 
 |-  w
10 9 8 cfv 
 |-  ( ( DVecH ` k ) ` w )
11 vu 
 |-  u
12 cbs 
 |-  Base
13 11 cv 
 |-  u
14 13 12 cfv 
 |-  ( Base ` u )
15 vv 
 |-  v
16 cnx 
 |-  ndx
17 16 12 cfv 
 |-  ( Base ` ndx )
18 15 cv 
 |-  v
19 17 18 cop 
 |-  <. ( Base ` ndx ) , v >.
20 cplusg 
 |-  +g
21 16 20 cfv 
 |-  ( +g ` ndx )
22 13 20 cfv 
 |-  ( +g ` u )
23 21 22 cop 
 |-  <. ( +g ` ndx ) , ( +g ` u ) >.
24 csca 
 |-  Scalar
25 16 24 cfv 
 |-  ( Scalar ` ndx )
26 cedring 
 |-  EDRing
27 5 26 cfv 
 |-  ( EDRing ` k )
28 9 27 cfv 
 |-  ( ( EDRing ` k ) ` w )
29 csts 
 |-  sSet
30 cstv 
 |-  *r
31 16 30 cfv 
 |-  ( *r ` ndx )
32 chg 
 |-  HGMap
33 5 32 cfv 
 |-  ( HGMap ` k )
34 9 33 cfv 
 |-  ( ( HGMap ` k ) ` w )
35 31 34 cop 
 |-  <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >.
36 28 35 29 co 
 |-  ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. )
37 25 36 cop 
 |-  <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >.
38 19 23 37 ctp 
 |-  { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( ( HGMap ` k ) ` w ) >. ) >. }
39 cvsca 
 |-  .s
40 16 39 cfv 
 |-  ( .s ` ndx )
41 13 39 cfv 
 |-  ( .s ` u )
42 40 41 cop 
 |-  <. ( .s ` ndx ) , ( .s ` u ) >.
43 cip 
 |-  .i
44 16 43 cfv 
 |-  ( .i ` ndx )
45 vx 
 |-  x
46 vy 
 |-  y
47 chdma 
 |-  HDMap
48 5 47 cfv 
 |-  ( HDMap ` k )
49 9 48 cfv 
 |-  ( ( HDMap ` k ) ` w )
50 46 cv 
 |-  y
51 50 49 cfv 
 |-  ( ( ( HDMap ` k ) ` w ) ` y )
52 45 cv 
 |-  x
53 52 51 cfv 
 |-  ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x )
54 45 46 18 18 53 cmpo 
 |-  ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) )
55 44 54 cop 
 |-  <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >.
56 42 55 cpr 
 |-  { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( ( HDMap ` k ) ` w ) ` y ) ` x ) ) >. }
57 38 56 cun 
 |-  ( { <. ( 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 ) ) >. } )
58 15 14 57 csb 
 |-  [_ ( 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 ) ) >. } )
59 11 10 58 csb 
 |-  [_ ( ( 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 ) ) >. } )
60 3 6 59 cmpt 
 |-  ( 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 ) ) >. } ) )
61 1 2 60 cmpt 
 |-  ( 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 ) ) >. } ) ) )
62 0 61 wceq 
 |-  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 ) ) >. } ) ) )