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	$⊢ X = BaseSet (U)$
	bnsscmcl.d	$⊢ D = IndMet (U)$
	bnsscmcl.j	$⊢ J = MetOpen (D)$
	bnsscmcl.h	$⊢ H = SubSp (U)$
	bnsscmcl.y	$⊢ Y = BaseSet (W)$
Assertion	bnsscmcl	$⊢ (U \in CBan \land W \in H) \to (W \in CBan \leftrightarrow Y \in Clsd (J))$

Proof

Step	Hyp	Ref	Expression
1		bnsscmcl.x	$⊢ X = BaseSet (U)$
2		bnsscmcl.d	$⊢ D = IndMet (U)$
3		bnsscmcl.j	$⊢ J = MetOpen (D)$
4		bnsscmcl.h	$⊢ H = SubSp (U)$
5		bnsscmcl.y	$⊢ Y = BaseSet (W)$
6		bnnv	$⊢ U \in CBan \to U \in NrmCVec$
7	4	sspnv	$⊢ (U \in NrmCVec \land W \in H) \to W \in NrmCVec$
8	6 7	sylan	$⊢ (U \in CBan \land W \in H) \to W \in NrmCVec$
9		eqid	$⊢ IndMet (W) = IndMet (W)$
10	5 9	iscbn	$⊢ W \in CBan \leftrightarrow (W \in NrmCVec \land IndMet (W) \in CMet (Y))$
11	10	baib	$⊢ W \in NrmCVec \to (W \in CBan \leftrightarrow IndMet (W) \in CMet (Y))$
12	8 11	syl	$⊢ (U \in CBan \land W \in H) \to (W \in CBan \leftrightarrow IndMet (W) \in CMet (Y))$
13	5 2 9 4	sspims	$⊢ (U \in NrmCVec \land W \in H) \to IndMet (W) = {D ↾}_{(Y \times Y)}$
14	6 13	sylan	$⊢ (U \in CBan \land W \in H) \to IndMet (W) = {D ↾}_{(Y \times Y)}$
15	14	eleq1d	$⊢ (U \in CBan \land W \in H) \to (IndMet (W) \in CMet (Y) \leftrightarrow {D ↾}_{(Y \times Y)} \in CMet (Y))$
16	1 2	cbncms	$⊢ U \in CBan \to D \in CMet (X)$
17	16	adantr	$⊢ (U \in CBan \land W \in H) \to D \in CMet (X)$
18	3	cmetss	$⊢ D \in CMet (X) \to ({D ↾}_{(Y \times Y)} \in CMet (Y) \leftrightarrow Y \in Clsd (J))$
19	17 18	syl	$⊢ (U \in CBan \land W \in H) \to ({D ↾}_{(Y \times Y)} \in CMet (Y) \leftrightarrow Y \in Clsd (J))$
20	12 15 19	3bitrd	$⊢ (U \in CBan \land W \in H) \to (W \in CBan \leftrightarrow Y \in Clsd (J))$

Metamath Proof Explorer

Theorem bnsscmcl

Proof