Metamath Proof Explorer


Definition df-sh

Description: Define the set of subspaces of a Hilbert space. See issh for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of Beran p. 95. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion df-sh S = { ∈ 𝒫 ℋ ∣ ( 0 ∧ ( + “ ( × ) ) ⊆ ∧ ( · “ ( ℂ × ) ) ⊆ ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 csh S
1 vh
2 chba
3 2 cpw 𝒫 ℋ
4 c0v 0
5 1 cv
6 4 5 wcel 0
7 cva +
8 5 5 cxp ( × )
9 7 8 cima ( + “ ( × ) )
10 9 5 wss ( + “ ( × ) ) ⊆
11 csm ·
12 cc
13 12 5 cxp ( ℂ × )
14 11 13 cima ( · “ ( ℂ × ) )
15 14 5 wss ( · “ ( ℂ × ) ) ⊆
16 6 10 15 w3a ( 0 ∧ ( + “ ( × ) ) ⊆ ∧ ( · “ ( ℂ × ) ) ⊆ )
17 16 1 3 crab { ∈ 𝒫 ℋ ∣ ( 0 ∧ ( + “ ( × ) ) ⊆ ∧ ( · “ ( ℂ × ) ) ⊆ ) }
18 0 17 wceq S = { ∈ 𝒫 ℋ ∣ ( 0 ∧ ( + “ ( × ) ) ⊆ ∧ ( · “ ( ℂ × ) ) ⊆ ) }