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	$⊢ X = W ↾_{𝑠} U$
	cmslssbn.s	$⊢ S = LSubSp (W)$
Assertion	cmslssbn	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp) \land (X \in CMetSp \land U \in S)) \to X \in Ban$

Proof

Step	Hyp	Ref	Expression
1		cmslssbn.x	$⊢ X = W ↾_{𝑠} U$
2		cmslssbn.s	$⊢ S = LSubSp (W)$
3	1 2	lssnvc	$⊢ (W \in NrmVec \land U \in S) \to X \in NrmVec$
4	3	ad2ant2rl	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp) \land (X \in CMetSp \land U \in S)) \to X \in NrmVec$
5		simprl	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp) \land (X \in CMetSp \land U \in S)) \to X \in CMetSp$
6		eqid	$⊢ Scalar (W) = Scalar (W)$
7	1 6	resssca	$⊢ U \in S \to Scalar (W) = Scalar (X)$
8	7	ad2antll	$⊢ (W \in NrmVec \land (X \in CMetSp \land U \in S)) \to Scalar (W) = Scalar (X)$
9	8	eleq1d	$⊢ (W \in NrmVec \land (X \in CMetSp \land U \in S)) \to (Scalar (W) \in CMetSp \leftrightarrow Scalar (X) \in CMetSp)$
10	9	biimpd	$⊢ (W \in NrmVec \land (X \in CMetSp \land U \in S)) \to (Scalar (W) \in CMetSp \to Scalar (X) \in CMetSp)$
11	10	impancom	$⊢ (W \in NrmVec \land Scalar (W) \in CMetSp) \to ((X \in CMetSp \land U \in S) \to Scalar (X) \in CMetSp)$
12	11	imp	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp) \land (X \in CMetSp \land U \in S)) \to Scalar (X) \in CMetSp$
13		eqid	$⊢ Scalar (X) = Scalar (X)$
14	13	isbn	$⊢ X \in Ban \leftrightarrow (X \in NrmVec \land X \in CMetSp \land Scalar (X) \in CMetSp)$
15	4 5 12 14	syl3anbrc	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp) \land (X \in CMetSp \land U \in S)) \to X \in Ban$

Metamath Proof Explorer

Theorem cmslssbn

Proof