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 = ( ℎ ∈ V ↦ ( ( toInc ‘ ( ClSubSp ‘ ℎ ) ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ ℎ ) ⟩ ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cthl ⊢ toHL
1 vh ⊢ ℎ
2 cvv ⊢ V
3 cipo ⊢ toInc
4 ccss ⊢ ClSubSp
5 1 cv ⊢ ℎ
6 5 4 cfv ⊢ ( ClSubSp ‘ ℎ )
7 6 3 cfv ⊢ ( toInc ‘ ( ClSubSp ‘ ℎ ) )
8 csts ⊢ sSet
9 coc ⊢ oc
10 cnx ⊢ ndx
11 10 9 cfv ⊢ ( oc ‘ ndx )
12 cocv ⊢ ocv
13 5 12 cfv ⊢ ( ocv ‘ ℎ )
14 11 13 cop ⊢ ⟨ ( oc ‘ ndx ) , ( ocv ‘ ℎ ) ⟩
15 7 14 8 co ⊢ ( ( toInc ‘ ( ClSubSp ‘ ℎ ) ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ ℎ ) ⟩ )
16 1 2 15 cmpt ⊢ ( ℎ ∈ V ↦ ( ( toInc ‘ ( ClSubSp ‘ ℎ ) ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ ℎ ) ⟩ ) )
17 0 16 wceq ⊢ toHL = ( ℎ ∈ V ↦ ( ( toInc ‘ ( ClSubSp ‘ ℎ ) ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ ℎ ) ⟩ ) )