Description: Closed subspace H of a Hilbert space. (Contributed by NM, 17-Aug-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | isch | ⊢ ( 𝐻 ∈ Cℋ ↔ ( 𝐻 ∈ Sℋ ∧ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ⊆ 𝐻 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oveq1 | ⊢ ( ℎ = 𝐻 → ( ℎ ↑m ℕ ) = ( 𝐻 ↑m ℕ ) ) | |
| 2 | 1 | imaeq2d | ⊢ ( ℎ = 𝐻 → ( ⇝𝑣 “ ( ℎ ↑m ℕ ) ) = ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ) |
| 3 | id | ⊢ ( ℎ = 𝐻 → ℎ = 𝐻 ) | |
| 4 | 2 3 | sseq12d | ⊢ ( ℎ = 𝐻 → ( ( ⇝𝑣 “ ( ℎ ↑m ℕ ) ) ⊆ ℎ ↔ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ⊆ 𝐻 ) ) |
| 5 | df-ch | ⊢ Cℋ = { ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ ( ℎ ↑m ℕ ) ) ⊆ ℎ } | |
| 6 | 4 5 | elrab2 | ⊢ ( 𝐻 ∈ Cℋ ↔ ( 𝐻 ∈ Sℋ ∧ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ⊆ 𝐻 ) ) |