This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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ℎ ∈ ℎ ∧ ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ ∧ ( ·ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ ) }