Description: Obsolete version of cssbn : Banach space property of a closed subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hhssbnOLD.1 | ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ | |
| hhssbnOLD.2 | ⊢ 𝐻 ∈ Cℋ | ||
| Assertion | hhssbnOLD | ⊢ 𝑊 ∈ CBan |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hhssbnOLD.1 | ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ | |
| 2 | hhssbnOLD.2 | ⊢ 𝐻 ∈ Cℋ | |
| 3 | 2 | chshii | ⊢ 𝐻 ∈ Sℋ |
| 4 | 1 3 | hhssnv | ⊢ 𝑊 ∈ NrmCVec |
| 5 | eqid | ⊢ ( IndMet ‘ 𝑊 ) = ( IndMet ‘ 𝑊 ) | |
| 6 | 1 5 2 | hhsscms | ⊢ ( IndMet ‘ 𝑊 ) ∈ ( CMet ‘ 𝐻 ) |
| 7 | 1 3 | hhssba | ⊢ 𝐻 = ( BaseSet ‘ 𝑊 ) |
| 8 | 7 5 | iscbn | ⊢ ( 𝑊 ∈ CBan ↔ ( 𝑊 ∈ NrmCVec ∧ ( IndMet ‘ 𝑊 ) ∈ ( CMet ‘ 𝐻 ) ) ) |
| 9 | 4 6 8 | mpbir2an | ⊢ 𝑊 ∈ CBan |