Metamath Proof Explorer

Definition df-thl

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

Ref Expression
Assertion df-thl ⊢ toHL = h ∈ V ⟼ toInc ⁡ ClSubSp ⁡ h sSet oc ⁡ ndx ocv ⁡ h

Detailed syntax breakdown

Step Hyp Ref Expression
0 cthl class toHL
1 vh setvar h
2 cvv class V
3 cipo class toInc
4 ccss class ClSubSp
5 1 cv setvar h
6 5 4 cfv class ClSubSp ⁡ h
7 6 3 cfv class toInc ⁡ ClSubSp ⁡ h
8 csts class sSet
9 coc class oc
10 cnx class ndx
11 10 9 cfv class oc ⁡ ndx
12 cocv class ocv
13 5 12 cfv class ocv ⁡ h
14 11 13 cop class oc ⁡ ndx ocv ⁡ h
15 7 14 8 co class toInc ⁡ ClSubSp ⁡ h sSet oc ⁡ ndx ocv ⁡ h
16 1 2 15 cmpt class h ∈ V ⟼ toInc ⁡ ClSubSp ⁡ h sSet oc ⁡ ndx ocv ⁡ h
17 0 16 wceq wff toHL = h ∈ V ⟼ toInc ⁡ ClSubSp ⁡ h sSet oc ⁡ ndx ocv ⁡ h