Definition df-hlhil 37225

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

Step	Hyp	Ref	Expression
1		chlh 37224	. 2 class HLHil
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vw	. . . 4 setvar w
5	2	cv 1482	. . . . 5 class k
6		clh 35270	. . . . 5 class LHyp
7	5, 6	cfv 5888	. . . 4 class ( LHyp ` k )
8		vu	. . . . 5 setvar u
9	4	cv 1482	. . . . . 6 class w
10		cdvh 36367	. . . . . . 7 class DVecH
11	5, 10	cfv 5888	. . . . . 6 class ( DVecH ` k )
12	9, 11	cfv 5888	. . . . 5 class ( ( DVecH ` k ) ` w )
13		vv	. . . . . 6 setvar v
14	8	cv 1482	. . . . . . 7 class u
15		cbs 15857	. . . . . . 7 class Base
16	14, 15	cfv 5888	. . . . . 6 class ( Base ` u )
17		cnx 15854	. . . . . . . . . 10 class ndx
18	17, 15	cfv 5888	. . . . . . . . 9 class ( Base ` ndx )
19	13	cv 1482	. . . . . . . . 9 class v
20	18, 19	cop 4183	. . . . . . . 8 class <. ( Base ` ndx ) , v >.
21		cplusg 15941	. . . . . . . . . 10 class +g
22	17, 21	cfv 5888	. . . . . . . . 9 class ( +g ` ndx )
23	14, 21	cfv 5888	. . . . . . . . 9 class ( +g ` u )
24	22, 23	cop 4183	. . . . . . . 8 class <. ( +g ` ndx ) , ( +g ` u ) >.
25		csca 15944	. . . . . . . . . 10 class Scalar
26	17, 25	cfv 5888	. . . . . . . . 9 class (Scalar ` ndx )
27		cedring 36041	. . . . . . . . . . . 12 class EDRing
28	5, 27	cfv 5888	. . . . . . . . . . 11 class ( EDRing ` k )
29	9, 28	cfv 5888	. . . . . . . . . 10 class ( ( EDRing ` k ) ` w )
30		cstv 15943	. . . . . . . . . . . 12 class *r
31	17, 30	cfv 5888	. . . . . . . . . . 11 class ( *r ` ndx )
32		chg 37175	. . . . . . . . . . . . 13 class HGMap
33	5, 32	cfv 5888	. . . . . . . . . . . 12 class (HGMap ` k )
34	9, 33	cfv 5888	. . . . . . . . . . 11 class ( (HGMap ` k ) ` w )
35	31, 34	cop 4183	. . . . . . . . . 10 class <. ( *r ` ndx ) , ( (HGMap ` k ) ` w ) >.
36		csts 15855	. . . . . . . . . 10 class sSet
37	29, 35, 36	co 6650	. . . . . . . . 9 class ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( (HGMap ` k ) ` w ) >. )
38	26, 37	cop 4183	. . . . . . . 8 class <. (Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( (HGMap ` k ) ` w ) >. ) >.
39	20, 24, 38	ctp 4181	. . . . . . 7 class { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. (Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( (HGMap ` k ) ` w ) >. ) >. }
40		cvsca 15945	. . . . . . . . . 10 class .s
41	17, 40	cfv 5888	. . . . . . . . 9 class ( .s ` ndx )
42	14, 40	cfv 5888	. . . . . . . . 9 class ( .s ` u )
43	41, 42	cop 4183	. . . . . . . 8 class <. ( .s ` ndx ) , ( .s ` u ) >.
44		cip 15946	. . . . . . . . . 10 class .i
45	17, 44	cfv 5888	. . . . . . . . 9 class ( .i ` ndx )
46		vx	. . . . . . . . . 10 setvar x
47		vy	. . . . . . . . . 10 setvar y
48	46	cv 1482	. . . . . . . . . . 11 class x
49	47	cv 1482	. . . . . . . . . . . 12 class y
50		chdma 37082	. . . . . . . . . . . . . 14 class HDMap
51	5, 50	cfv 5888	. . . . . . . . . . . . 13 class (HDMap ` k )
52	9, 51	cfv 5888	. . . . . . . . . . . 12 class ( (HDMap ` k ) ` w )
53	49, 52	cfv 5888	. . . . . . . . . . 11 class ( ( (HDMap ` k ) ` w ) ` y )
54	48, 53	cfv 5888	. . . . . . . . . 10 class ( ( ( (HDMap ` k ) ` w ) ` y ) ` x )
55	46, 47, 19, 19, 54	cmpt2 6652	. . . . . . . . 9 class ( x e. v , y e. v |-> ( ( ( (HDMap ` k ) ` w ) ` y ) ` x ) )
56	45, 55	cop 4183	. . . . . . . 8 class <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( (HDMap ` k ) ` w ) ` y ) ` x ) ) >.
57	43, 56	cpr 4179	. . . . . . 7 class { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( (HDMap ` k ) ` w ) ` y ) ` x ) ) >. }
58	39, 57	cun 3572	. . . . . 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 ) ) >. } )
59	13, 16, 58	csb 3533	. . . . 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 ) ) >. } )
60	8, 12, 59	csb 3533	. . . 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 ) ) >. } )
61	4, 7, 60	cmpt 4729	. . 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 ) ) >. } ) )
62	2, 3, 61	cmpt 4729	. 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 ) ) >. } ) ) )
63	1, 62	wceq 1483	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 ) ) >. } ) ) )

This definition is referenced by:  hlhilset  37226