bnsscmcl

Description: A subspace of a Banach space is a Banach space iff it is closed in the norm-induced metric of the parent space. (Contributed by NM, 1-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnsscmcl.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	bnsscmcl.d	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	bnsscmcl.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	bnsscmcl.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
	bnsscmcl.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
Assertion	bnsscmcl	⊢ ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ 𝐻 ) → ( 𝑊 ∈ CBan ↔ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bnsscmcl.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		bnsscmcl.d	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3		bnsscmcl.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
4		bnsscmcl.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
5		bnsscmcl.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
6		bnnv	⊢ ( 𝑈 ∈ CBan → 𝑈 ∈ NrmCVec )
7	4	sspnv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ NrmCVec )
8	6 7	sylan	⊢ ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ NrmCVec )
9		eqid	⊢ ( IndMet ‘ 𝑊 ) = ( IndMet ‘ 𝑊 )
10	5 9	iscbn	⊢ ( 𝑊 ∈ CBan ↔ ( 𝑊 ∈ NrmCVec ∧ ( IndMet ‘ 𝑊 ) ∈ ( CMet ‘ 𝑌 ) ) )
11	10	baib	⊢ ( 𝑊 ∈ NrmCVec → ( 𝑊 ∈ CBan ↔ ( IndMet ‘ 𝑊 ) ∈ ( CMet ‘ 𝑌 ) ) )
12	8 11	syl	⊢ ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ 𝐻 ) → ( 𝑊 ∈ CBan ↔ ( IndMet ‘ 𝑊 ) ∈ ( CMet ‘ 𝑌 ) ) )
13	5 2 9 4	sspims	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( IndMet ‘ 𝑊 ) = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
14	6 13	sylan	⊢ ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ 𝐻 ) → ( IndMet ‘ 𝑊 ) = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
15	14	eleq1d	⊢ ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ 𝐻 ) → ( ( IndMet ‘ 𝑊 ) ∈ ( CMet ‘ 𝑌 ) ↔ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) )
16	1 2	cbncms	⊢ ( 𝑈 ∈ CBan → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
17	16	adantr	⊢ ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
18	3	cmetss	⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ↔ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) )
19	17 18	syl	⊢ ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ↔ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) )
20	12 15 19	3bitrd	⊢ ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ 𝐻 ) → ( 𝑊 ∈ CBan ↔ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) )

Metamath Proof Explorer

Theorem bnsscmcl

Proof