lssbn

Description: A subspace of a Banach space is a Banach space iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	lssbn.x	$⊢ X = W ↾_{𝑠} U$
	lssbn.s	$⊢ S = LSubSp (W)$
	lssbn.j	$⊢ J = TopOpen (W)$
Assertion	lssbn	$⊢ (W \in Ban \land U \in S) \to (X \in Ban \leftrightarrow U \in Clsd (J))$

Proof

Step	Hyp	Ref	Expression
1		lssbn.x	$⊢ X = W ↾_{𝑠} U$
2		lssbn.s	$⊢ S = LSubSp (W)$
3		lssbn.j	$⊢ J = TopOpen (W)$
4		bnnvc	$⊢ W \in Ban \to W \in NrmVec$
5	1 2	lssnvc	$⊢ (W \in NrmVec \land U \in S) \to X \in NrmVec$
6	4 5	sylan	$⊢ (W \in Ban \land U \in S) \to X \in NrmVec$
7		eqid	$⊢ Scalar (W) = Scalar (W)$
8	1 7	resssca	$⊢ U \in S \to Scalar (W) = Scalar (X)$
9	8	adantl	$⊢ (W \in Ban \land U \in S) \to Scalar (W) = Scalar (X)$
10	7	bnsca	$⊢ W \in Ban \to Scalar (W) \in CMetSp$
11	10	adantr	$⊢ (W \in Ban \land U \in S) \to Scalar (W) \in CMetSp$
12	9 11	eqeltrrd	$⊢ (W \in Ban \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		3anan32	$⊢ (X \in NrmVec \land X \in CMetSp \land Scalar (X) \in CMetSp) \leftrightarrow ((X \in NrmVec \land Scalar (X) \in CMetSp) \land X \in CMetSp)$
16	14 15	bitri	$⊢ X \in Ban \leftrightarrow ((X \in NrmVec \land Scalar (X) \in CMetSp) \land X \in CMetSp)$
17	16	baib	$⊢ (X \in NrmVec \land Scalar (X) \in CMetSp) \to (X \in Ban \leftrightarrow X \in CMetSp)$
18	6 12 17	syl2anc	$⊢ (W \in Ban \land U \in S) \to (X \in Ban \leftrightarrow X \in CMetSp)$
19		bncms	$⊢ W \in Ban \to W \in CMetSp$
20		eqid	$⊢ {Base}_{W} = {Base}_{W}$
21	20 2	lssss	$⊢ U \in S \to U \subseteq {Base}_{W}$
22	1 20 3	cmsss	$⊢ (W \in CMetSp \land U \subseteq {Base}_{W}) \to (X \in CMetSp \leftrightarrow U \in Clsd (J))$
23	19 21 22	syl2an	$⊢ (W \in Ban \land U \in S) \to (X \in CMetSp \leftrightarrow U \in Clsd (J))$
24	18 23	bitrd	$⊢ (W \in Ban \land U \in S) \to (X \in Ban \leftrightarrow U \in Clsd (J))$

Metamath Proof Explorer

Theorem lssbn

Proof