Definition df-hlhil 39874

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

Step	Hyp	Ref	Expression
1		chlh 39873	. 2 class HLHil
2		vk	. . 3 setvar 𝑘
3		cvv 3422	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1538	. . . . 5 class 𝑘
6		clh 37925	. . . . 5 class LHyp
7	5, 6	cfv 6418	. . . 4 class (LHyp‘𝑘)
8		vu	. . . . 5 setvar 𝑢
9	4	cv 1538	. . . . . 6 class 𝑤
10		cdvh 39019	. . . . . . 7 class DVecH
11	5, 10	cfv 6418	. . . . . 6 class (DVecH‘𝑘)
12	9, 11	cfv 6418	. . . . 5 class ((DVecH‘𝑘)‘𝑤)
13		vv	. . . . . 6 setvar 𝑣
14	8	cv 1538	. . . . . . 7 class 𝑢
15		cbs 16840	. . . . . . 7 class Base
16	14, 15	cfv 6418	. . . . . 6 class (Base‘𝑢)
17		cnx 16822	. . . . . . . . . 10 class ndx
18	17, 15	cfv 6418	. . . . . . . . 9 class (Base‘ndx)
19	13	cv 1538	. . . . . . . . 9 class 𝑣
20	18, 19	cop 4564	. . . . . . . 8 class ⟨(Base‘ndx), 𝑣⟩
21		cplusg 16888	. . . . . . . . . 10 class +g
22	17, 21	cfv 6418	. . . . . . . . 9 class (+g‘ndx)
23	14, 21	cfv 6418	. . . . . . . . 9 class (+g‘𝑢)
24	22, 23	cop 4564	. . . . . . . 8 class ⟨(+g‘ndx), (+g‘𝑢)⟩
25		csca 16891	. . . . . . . . . 10 class Scalar
26	17, 25	cfv 6418	. . . . . . . . 9 class (Scalar‘ndx)
27		cedring 38694	. . . . . . . . . . . 12 class EDRing
28	5, 27	cfv 6418	. . . . . . . . . . 11 class (EDRing‘𝑘)
29	9, 28	cfv 6418	. . . . . . . . . 10 class ((EDRing‘𝑘)‘𝑤)
30		cstv 16890	. . . . . . . . . . . 12 class *𝑟
31	17, 30	cfv 6418	. . . . . . . . . . 11 class (*𝑟‘ndx)
32		chg 39824	. . . . . . . . . . . . 13 class HGMap
33	5, 32	cfv 6418	. . . . . . . . . . . 12 class (HGMap‘𝑘)
34	9, 33	cfv 6418	. . . . . . . . . . 11 class ((HGMap‘𝑘)‘𝑤)
35	31, 34	cop 4564	. . . . . . . . . 10 class ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩
36		csts 16792	. . . . . . . . . 10 class sSet
37	29, 35, 36	co 7255	. . . . . . . . 9 class (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)
38	26, 37	cop 4564	. . . . . . . 8 class ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩
39	20, 24, 38	ctp 4562	. . . . . . 7 class {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g‘𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩}
40		cvsca 16892	. . . . . . . . . 10 class ·𝑠
41	17, 40	cfv 6418	. . . . . . . . 9 class ( ·𝑠 ‘ndx)
42	14, 40	cfv 6418	. . . . . . . . 9 class ( ·𝑠 ‘𝑢)
43	41, 42	cop 4564	. . . . . . . 8 class ⟨( ·𝑠 ‘ndx), ( ·𝑠 ‘𝑢)⟩
44		cip 16893	. . . . . . . . . 10 class ·𝑖
45	17, 44	cfv 6418	. . . . . . . . 9 class (·𝑖‘ndx)
46		vx	. . . . . . . . . 10 setvar 𝑥
47		vy	. . . . . . . . . 10 setvar 𝑦
48	46	cv 1538	. . . . . . . . . . 11 class 𝑥
49	47	cv 1538	. . . . . . . . . . . 12 class 𝑦
50		chdma 39733	. . . . . . . . . . . . . 14 class HDMap
51	5, 50	cfv 6418	. . . . . . . . . . . . 13 class (HDMap‘𝑘)
52	9, 51	cfv 6418	. . . . . . . . . . . 12 class ((HDMap‘𝑘)‘𝑤)
53	49, 52	cfv 6418	. . . . . . . . . . 11 class (((HDMap‘𝑘)‘𝑤)‘𝑦)
54	48, 53	cfv 6418	. . . . . . . . . 10 class ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥)
55	46, 47, 19, 19, 54	cmpo 7257	. . . . . . . . 9 class (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))
56	45, 55	cop 4564	. . . . . . . 8 class ⟨(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩
57	43, 56	cpr 4560	. . . . . . 7 class {⟨( ·𝑠 ‘ndx), ( ·𝑠 ‘𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩}
58	39, 57	cun 3881	. . . . . 6 class ({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g‘𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠 ‘𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})
59	13, 16, 58	csb 3828	. . . . 5 class ⦋(Base‘𝑢) / 𝑣⦌({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g‘𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠 ‘𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})
60	8, 12, 59	csb 3828	. . . 4 class ⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g‘𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠 ‘𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})
61	4, 7, 60	cmpt 5153	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ ⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g‘𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠 ‘𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩}))
62	2, 3, 61	cmpt 5153	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g‘𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠 ‘𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})))
63	1, 62	wceq 1539	1 wff HLHil = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ ⦋((DVecH‘𝑘)‘𝑤) / 𝑢⦌⦋(Base‘𝑢) / 𝑣⦌({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (+g‘𝑢)⟩, ⟨(Scalar‘ndx), (((EDRing‘𝑘)‘𝑤) sSet ⟨(*𝑟‘ndx), ((HGMap‘𝑘)‘𝑤)⟩)⟩} ∪ {⟨( ·𝑠 ‘ndx), ( ·𝑠 ‘𝑢)⟩, ⟨(·𝑖‘ndx), (𝑥 ∈ 𝑣, 𝑦 ∈ 𝑣 ↦ ((((HDMap‘𝑘)‘𝑤)‘𝑦)‘𝑥))⟩})))

This definition is referenced by:  hlhilset  39875