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

Metamath Proof Explorer

Theorem 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 ‘ 𝐽 ) ) )