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

Metamath Proof Explorer

Theorem cmslssbn

Description: A complete linear subspace of a normed vector space is a Banach space. We furthermore have to assume that the field of scalars is complete since this is a requirement in the current definition of Banach spaces df-bn . (Contributed by AV, 8-Oct-2022)

Ref Expression
Hypotheses cmslssbn.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
cmslssbn.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion cmslssbn ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ) ∧ ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ) → 𝑋 ∈ Ban )

Proof

Step Hyp Ref Expression
1 cmslssbn.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2 cmslssbn.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 1 2 lssnvc ⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmVec )
4 3 ad2ant2rl ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ) ∧ ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ) → 𝑋 ∈ NrmVec )
5 simprl ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ) ∧ ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ) → 𝑋 ∈ CMetSp )
6 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
7 1 6 resssca ⊢ ( 𝑈 ∈ 𝑆 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
8 7 ad2antll ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
9 8 eleq1d ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ) → ( ( Scalar ‘ 𝑊 ) ∈ CMetSp ↔ ( Scalar ‘ 𝑋 ) ∈ CMetSp ) )
10 9 biimpd ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ) → ( ( Scalar ‘ 𝑊 ) ∈ CMetSp → ( Scalar ‘ 𝑋 ) ∈ CMetSp ) )
11 10 impancom ⊢ ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ) → ( ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑋 ) ∈ CMetSp ) )
12 11 imp ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ) ∧ ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ) → ( Scalar ‘ 𝑋 ) ∈ CMetSp )
13 eqid ⊢ ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑋 )
14 13 isbn ⊢ ( 𝑋 ∈ Ban ↔ ( 𝑋 ∈ NrmVec ∧ 𝑋 ∈ CMetSp ∧ ( Scalar ‘ 𝑋 ) ∈ CMetSp ) )
15 4 5 12 14 syl3anbrc ⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ) ∧ ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ) → 𝑋 ∈ Ban )