Definition df-thl 21218

Description: Define the Hilbert lattice of closed subspaces of a given pre-Hilbert space. (Contributed by Mario Carneiro, 25-Oct-2015.)

Assertion

Ref	Expression
df-thl	⊢ toHL = (ℎ ∈ V ↦ ((toInc‘(ClSubSp‘ℎ)) sSet ⟨(oc‘ndx), (ocv‘ℎ)⟩))

Detailed syntax breakdown of Definition df-thl

Step	Hyp	Ref	Expression
1		cthl 21215	. 2 class toHL
2		vh	. . 3 setvar ℎ
3		cvv 3475	. . 3 class V
4	2	cv 1541	. . . . . 6 class ℎ
5		ccss 21214	. . . . . 6 class ClSubSp
6	4, 5	cfv 6544	. . . . 5 class (ClSubSp‘ℎ)
7		cipo 18480	. . . . 5 class toInc
8	6, 7	cfv 6544	. . . 4 class (toInc‘(ClSubSp‘ℎ))
9		cnx 17126	. . . . . 6 class ndx
10		coc 17205	. . . . . 6 class oc
11	9, 10	cfv 6544	. . . . 5 class (oc‘ndx)
12		cocv 21213	. . . . . 6 class ocv
13	4, 12	cfv 6544	. . . . 5 class (ocv‘ℎ)
14	11, 13	cop 4635	. . . 4 class ⟨(oc‘ndx), (ocv‘ℎ)⟩
15		csts 17096	. . . 4 class sSet
16	8, 14, 15	co 7409	. . 3 class ((toInc‘(ClSubSp‘ℎ)) sSet ⟨(oc‘ndx), (ocv‘ℎ)⟩)
17	2, 3, 16	cmpt 5232	. 2 class (ℎ ∈ V ↦ ((toInc‘(ClSubSp‘ℎ)) sSet ⟨(oc‘ndx), (ocv‘ℎ)⟩))
18	1, 17	wceq 1542	1 wff toHL = (ℎ ∈ V ↦ ((toInc‘(ClSubSp‘ℎ)) sSet ⟨(oc‘ndx), (ocv‘ℎ)⟩))

This definition is referenced by:  thlval  21248