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 )