Metamath Proof Explorer

Theorem issh

Description: Subspace H of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion issh ⊢H∈Sℋ↔H⊆ℋ∧0ℎ∈H∧+ℎH×H⊆H∧⋅ℎℂ×H⊆H

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ℋ∈V
2 1 elpw2 ⊢H∈𝒫ℋ↔H⊆ℋ
3 3anass ⊢0ℎ∈H∧+ℎH×H⊆H∧⋅ℎℂ×H⊆H↔0ℎ∈H∧+ℎH×H⊆H∧⋅ℎℂ×H⊆H
4 2 3 anbi12i ⊢H∈𝒫ℋ∧0ℎ∈H∧+ℎH×H⊆H∧⋅ℎℂ×H⊆H↔H⊆ℋ∧0ℎ∈H∧+ℎH×H⊆H∧⋅ℎℂ×H⊆H
5 eleq2 ⊢h=H→0ℎ∈h↔0ℎ∈H
6 id ⊢h=H→h=H
7 6 sqxpeqd ⊢h=H→h×h=H×H
8 7 imaeq2d ⊢h=H→+ℎh×h=+ℎH×H
9 8 6 sseq12d ⊢h=H→+ℎh×h⊆h↔+ℎH×H⊆H
10 xpeq2 ⊢h=H→ℂ×h=ℂ×H
11 10 imaeq2d ⊢h=H→⋅ℎℂ×h=⋅ℎℂ×H
12 11 6 sseq12d ⊢h=H→⋅ℎℂ×h⊆h↔⋅ℎℂ×H⊆H
13 5 9 12 3anbi123d ⊢h=H→0ℎ∈h∧+ℎh×h⊆h∧⋅ℎℂ×h⊆h↔0ℎ∈H∧+ℎH×H⊆H∧⋅ℎℂ×H⊆H
14 df-sh ⊢Sℋ=h∈𝒫ℋ|0ℎ∈h∧+ℎh×h⊆h∧⋅ℎℂ×h⊆h
15 13 14 elrab2 ⊢H∈Sℋ↔H∈𝒫ℋ∧0ℎ∈H∧+ℎH×H⊆H∧⋅ℎℂ×H⊆H
16 anass ⊢H⊆ℋ∧0ℎ∈H∧+ℎH×H⊆H∧⋅ℎℂ×H⊆H↔H⊆ℋ∧0ℎ∈H∧+ℎH×H⊆H∧⋅ℎℂ×H⊆H
17 4 15 16 3bitr4i ⊢H∈Sℋ↔H⊆ℋ∧0ℎ∈H∧+ℎH×H⊆H∧⋅ℎℂ×H⊆H