Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
Subspaces and projections
Subspaces
df-sh
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ℎ ∈ ℎ ∧ ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ ∧ ( · ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ ) }