Metamath Proof Explorer

Definition df-css

Description: Define the set of closed (linear) subspaces of a given pre-Hilbert space. (Contributed by NM, 7-Oct-2011)

Ref Expression
Assertion df-css ⊢ ClSubSp = h ∈ V ⟼ s | s = ocv ⁡ h ⁡ ocv ⁡ h ⁡ s

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccss class ClSubSp
1 vh setvar h
2 cvv class V
3 vs setvar s
4 3 cv setvar s
5 cocv class ocv
6 1 cv setvar h
7 6 5 cfv class ocv ⁡ h
8 4 7 cfv class ocv ⁡ h ⁡ s
9 8 7 cfv class ocv ⁡ h ⁡ ocv ⁡ h ⁡ s
10 4 9 wceq wff s = ocv ⁡ h ⁡ ocv ⁡ h ⁡ s
11 10 3 cab class s | s = ocv ⁡ h ⁡ ocv ⁡ h ⁡ s
12 1 2 11 cmpt class h ∈ V ⟼ s | s = ocv ⁡ h ⁡ ocv ⁡ h ⁡ s
13 0 12 wceq wff ClSubSp = h ∈ V ⟼ s | s = ocv ⁡ h ⁡ ocv ⁡ h ⁡ s