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 ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ ⦋ DVecH ⁡ k ⁡ w / u⦌ ⦋ Base u / v⦌ Base ndx v + ndx + u Scalar ⁡ ndx EDRing ⁡ k ⁡ w sSet * ndx HGMap ⁡ k ⁡ w ∪ ⋅ ndx ⋅ u ⋅ 𝑖 ⁡ ndx x ∈ v , y ∈ v ⟼ HDMap ⁡ k ⁡ w ⁡ y ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlh class HLHil
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp ⁡ k
7 cdvh class DVecH
8 5 7 cfv class DVecH ⁡ k
9 3 cv setvar w
10 9 8 cfv class DVecH ⁡ k ⁡ w
11 vu setvar u
12 cbs class Base
13 11 cv setvar u
14 13 12 cfv class Base u
15 vv setvar v
16 cnx class ndx
17 16 12 cfv class Base ndx
18 15 cv setvar v
19 17 18 cop class Base ndx v
20 cplusg class + 𝑔
21 16 20 cfv class + ndx
22 13 20 cfv class + u
23 21 22 cop class + ndx + u
24 csca class Scalar
25 16 24 cfv class Scalar ⁡ ndx
26 cedring class EDRing
27 5 26 cfv class EDRing ⁡ k
28 9 27 cfv class EDRing ⁡ k ⁡ w
29 csts class sSet
30 cstv class ∗ 𝑟
31 16 30 cfv class * ndx
32 chg class HGMap
33 5 32 cfv class HGMap ⁡ k
34 9 33 cfv class HGMap ⁡ k ⁡ w
35 31 34 cop class * ndx HGMap ⁡ k ⁡ w
36 28 35 29 co class EDRing ⁡ k ⁡ w sSet * ndx HGMap ⁡ k ⁡ w
37 25 36 cop class Scalar ⁡ ndx EDRing ⁡ k ⁡ w sSet * ndx HGMap ⁡ k ⁡ w
38 19 23 37 ctp class Base ndx v + ndx + u Scalar ⁡ ndx EDRing ⁡ k ⁡ w sSet * ndx HGMap ⁡ k ⁡ w
39 cvsca class ⋅ 𝑠
40 16 39 cfv class ⋅ ndx
41 13 39 cfv class ⋅ u
42 40 41 cop class ⋅ ndx ⋅ u
43 cip class ⋅ 𝑖
44 16 43 cfv class ⋅ 𝑖 ⁡ ndx
45 vx setvar x
46 vy setvar y
47 chdma class HDMap
48 5 47 cfv class HDMap ⁡ k
49 9 48 cfv class HDMap ⁡ k ⁡ w
50 46 cv setvar y
51 50 49 cfv class HDMap ⁡ k ⁡ w ⁡ y
52 45 cv setvar x
53 52 51 cfv class HDMap ⁡ k ⁡ w ⁡ y ⁡ x
54 45 46 18 18 53 cmpo class x ∈ v , y ∈ v ⟼ HDMap ⁡ k ⁡ w ⁡ y ⁡ x
55 44 54 cop class ⋅ 𝑖 ⁡ ndx x ∈ v , y ∈ v ⟼ HDMap ⁡ k ⁡ w ⁡ y ⁡ x
56 42 55 cpr class ⋅ ndx ⋅ u ⋅ 𝑖 ⁡ ndx x ∈ v , y ∈ v ⟼ HDMap ⁡ k ⁡ w ⁡ y ⁡ x
57 38 56 cun class Base ndx v + ndx + u Scalar ⁡ ndx EDRing ⁡ k ⁡ w sSet * ndx HGMap ⁡ k ⁡ w ∪ ⋅ ndx ⋅ u ⋅ 𝑖 ⁡ ndx x ∈ v , y ∈ v ⟼ HDMap ⁡ k ⁡ w ⁡ y ⁡ x
58 15 14 57 csb class ⦋ Base u / v⦌ Base ndx v + ndx + u Scalar ⁡ ndx EDRing ⁡ k ⁡ w sSet * ndx HGMap ⁡ k ⁡ w ∪ ⋅ ndx ⋅ u ⋅ 𝑖 ⁡ ndx x ∈ v , y ∈ v ⟼ HDMap ⁡ k ⁡ w ⁡ y ⁡ x
59 11 10 58 csb class ⦋ DVecH ⁡ k ⁡ w / u⦌ ⦋ Base u / v⦌ Base ndx v + ndx + u Scalar ⁡ ndx EDRing ⁡ k ⁡ w sSet * ndx HGMap ⁡ k ⁡ w ∪ ⋅ ndx ⋅ u ⋅ 𝑖 ⁡ ndx x ∈ v , y ∈ v ⟼ HDMap ⁡ k ⁡ w ⁡ y ⁡ x
60 3 6 59 cmpt class w ∈ LHyp ⁡ k ⟼ ⦋ DVecH ⁡ k ⁡ w / u⦌ ⦋ Base u / v⦌ Base ndx v + ndx + u Scalar ⁡ ndx EDRing ⁡ k ⁡ w sSet * ndx HGMap ⁡ k ⁡ w ∪ ⋅ ndx ⋅ u ⋅ 𝑖 ⁡ ndx x ∈ v , y ∈ v ⟼ HDMap ⁡ k ⁡ w ⁡ y ⁡ x
61 1 2 60 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ ⦋ DVecH ⁡ k ⁡ w / u⦌ ⦋ Base u / v⦌ Base ndx v + ndx + u Scalar ⁡ ndx EDRing ⁡ k ⁡ w sSet * ndx HGMap ⁡ k ⁡ w ∪ ⋅ ndx ⋅ u ⋅ 𝑖 ⁡ ndx x ∈ v , y ∈ v ⟼ HDMap ⁡ k ⁡ w ⁡ y ⁡ x
62 0 61 wceq wff HLHil = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ ⦋ DVecH ⁡ k ⁡ w / u⦌ ⦋ Base u / v⦌ Base ndx v + ndx + u Scalar ⁡ ndx EDRing ⁡ k ⁡ w sSet * ndx HGMap ⁡ k ⁡ w ∪ ⋅ ndx ⋅ u ⋅ 𝑖 ⁡ ndx x ∈ v , y ∈ v ⟼ HDMap ⁡ k ⁡ w ⁡ y ⁡ x