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	⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
	hhssbnOLD.2	⊢ 𝐻 ∈ Cℋ
Assertion	hhssbnOLD	⊢ 𝑊 ∈ CBan

Proof

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