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

Metamath Proof Explorer

Theorem hhssbnOLD

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 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
hhssbnOLD.2 ⊢ H ∈ C ℋ
Assertion hhssbnOLD ⊢ W ∈ CBan

Proof

Step Hyp Ref Expression
1 hhssbnOLD.1 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
2 hhssbnOLD.2 ⊢ H ∈ C ℋ
3 2 chshii ⊢ H ∈ S ℋ
4 1 3 hhssnv ⊢ W ∈ NrmCVec
5 eqid ⊢ IndMet ⁡ W = IndMet ⁡ W
6 1 5 2 hhsscms ⊢ IndMet ⁡ W ∈ CMet ⁡ H
7 1 3 hhssba ⊢ H = BaseSet ⁡ W
8 7 5 iscbn ⊢ W ∈ CBan ↔ W ∈ NrmCVec ∧ IndMet ⁡ W ∈ CMet ⁡ H
9 4 6 8 mpbir2an ⊢ W ∈ CBan