hhsscms

Description: The induced metric of a closed subspace is complete. (Contributed by NM, 10-Apr-2008) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhssims2.1	$⊢ W = ⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩$
	hhssims2.3	$⊢ D = IndMet (W)$
	hhsscms.3	$⊢ H \in C_{ℋ}$
Assertion	hhsscms	$⊢ D \in CMet (H)$

Proof

Step	Hyp	Ref	Expression
1		hhssims2.1	$⊢ W = ⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩$
2		hhssims2.3	$⊢ D = IndMet (W)$
3		hhsscms.3	$⊢ H \in C_{ℋ}$
4		eqid	$⊢ MetOpen (D) = MetOpen (D)$
5	3	chshii	$⊢ H \in S_{ℋ}$
6	1 2 5	hhssmet	$⊢ D \in Met (H)$
7		simpl	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f \in Cau (D)$
8	1 2 5	hhssims2	$⊢ D = {({norm}_{ℎ} \circ -_{ℎ}) ↾}_{(H \times H)}$
9	8	fveq2i	$⊢ Cau (D) = Cau ({({norm}_{ℎ} \circ -_{ℎ}) ↾}_{(H \times H)})$
10	7 9	eleqtrdi	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f \in Cau ({({norm}_{ℎ} \circ -_{ℎ}) ↾}_{(H \times H)})$
11		eqid	$⊢ {norm}_{ℎ} \circ -_{ℎ} = {norm}_{ℎ} \circ -_{ℎ}$
12	11	hilxmet	$⊢ {norm}_{ℎ} \circ -_{ℎ} \in ∞Met (ℋ)$
13		simpr	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f : ℕ ⟶ H$
14		causs	$⊢ ({norm}_{ℎ} \circ -_{ℎ} \in ∞Met (ℋ) \land f : ℕ ⟶ H) \to (f \in Cau ({norm}_{ℎ} \circ -_{ℎ}) \leftrightarrow f \in Cau ({({norm}_{ℎ} \circ -_{ℎ}) ↾}_{(H \times H)}))$
15	12 13 14	sylancr	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to (f \in Cau ({norm}_{ℎ} \circ -_{ℎ}) \leftrightarrow f \in Cau ({({norm}_{ℎ} \circ -_{ℎ}) ↾}_{(H \times H)}))$
16	10 15	mpbird	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f \in Cau ({norm}_{ℎ} \circ -_{ℎ})$
17	3	chssii	$⊢ H \subseteq ℋ$
18		fss	$⊢ (f : ℕ ⟶ H \land H \subseteq ℋ) \to f : ℕ ⟶ ℋ$
19	13 17 18	sylancl	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f : ℕ ⟶ ℋ$
20		ax-hilex	$⊢ ℋ \in V$
21		nnex	$⊢ ℕ \in V$
22	20 21	elmap	$⊢ f \in (ℋ^{ℕ}) \leftrightarrow f : ℕ ⟶ ℋ$
23	19 22	sylibr	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f \in (ℋ^{ℕ})$
24		eqid	$⊢ ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩ = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
25	24 11	hhims	$⊢ {norm}_{ℎ} \circ -_{ℎ} = IndMet (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$
26	24 25	hhcau	$⊢ Cauchy = Cau ({norm}_{ℎ} \circ -_{ℎ}) \cap (ℋ^{ℕ})$
27	26	elin2	$⊢ f \in Cauchy \leftrightarrow (f \in Cau ({norm}_{ℎ} \circ -_{ℎ}) \land f \in (ℋ^{ℕ}))$
28	16 23 27	sylanbrc	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f \in Cauchy$
29		ax-hcompl	$⊢ f \in Cauchy \to \exists x \in ℋ f \underset{v}{⇝} x$
30		vex	$⊢ f \in V$
31		vex	$⊢ x \in V$
32	30 31	breldm	$⊢ f \underset{v}{⇝} x \to f \in dom \underset{v}{⇝}$
33	32	rexlimivw	$⊢ \exists x \in ℋ f \underset{v}{⇝} x \to f \in dom \underset{v}{⇝}$
34	28 29 33	3syl	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f \in dom \underset{v}{⇝}$
35		hlimf	$⊢ \underset{v}{⇝} : dom \underset{v}{⇝} ⟶ ℋ$
36		ffun	$⊢ \underset{v}{⇝} : dom \underset{v}{⇝} ⟶ ℋ \to Fun \underset{v}{⇝}$
37		funfvbrb	$⊢ Fun \underset{v}{⇝} \to (f \in dom \underset{v}{⇝} \leftrightarrow f \underset{v}{⇝} \underset{v}{⇝} (f))$
38	35 36 37	mp2b	$⊢ f \in dom \underset{v}{⇝} \leftrightarrow f \underset{v}{⇝} \underset{v}{⇝} (f)$
39	34 38	sylib	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f \underset{v}{⇝} \underset{v}{⇝} (f)$
40		eqid	$⊢ MetOpen ({norm}_{ℎ} \circ -_{ℎ}) = MetOpen ({norm}_{ℎ} \circ -_{ℎ})$
41	24 25 40	hhlm	$⊢ \underset{v}{⇝} = {\underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) ↾}_{(ℋ^{ℕ})}$
42		resss	$⊢ {\underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) ↾}_{(ℋ^{ℕ})} \subseteq \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
43	41 42	eqsstri	$⊢ \underset{v}{⇝} \subseteq \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
44	43	ssbri	$⊢ f \underset{v}{⇝} \underset{v}{⇝} (f) \to f \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) \underset{v}{⇝} (f)$
45	39 44	syl	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) \underset{v}{⇝} (f)$
46	8 40 4	metrest	$⊢ ({norm}_{ℎ} \circ -_{ℎ} \in ∞Met (ℋ) \land H \subseteq ℋ) \to MetOpen ({norm}_{ℎ} \circ -_{ℎ}) ↾_{𝑡} H = MetOpen (D)$
47	12 17 46	mp2an	$⊢ MetOpen ({norm}_{ℎ} \circ -_{ℎ}) ↾_{𝑡} H = MetOpen (D)$
48	47	eqcomi	$⊢ MetOpen (D) = MetOpen ({norm}_{ℎ} \circ -_{ℎ}) ↾_{𝑡} H$
49		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
50	3	a1i	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to H \in C_{ℋ}$
51	40	mopntop	$⊢ {norm}_{ℎ} \circ -_{ℎ} \in ∞Met (ℋ) \to MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \in Top$
52	12 51	mp1i	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \in Top$
53		fvex	$⊢ \underset{v}{⇝} (f) \in V$
54	53	chlimi	$⊢ (H \in C_{ℋ} \land f : ℕ ⟶ H \land f \underset{v}{⇝} \underset{v}{⇝} (f)) \to \underset{v}{⇝} (f) \in H$
55	50 13 39 54	syl3anc	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to \underset{v}{⇝} (f) \in H$
56		1zzd	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to 1 \in ℤ$
57	48 49 50 52 55 56 13	lmss	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to (f \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) \underset{v}{⇝} (f) \leftrightarrow f \underset{t}{⇝} (MetOpen (D)) \underset{v}{⇝} (f))$
58	45 57	mpbid	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f \underset{t}{⇝} (MetOpen (D)) \underset{v}{⇝} (f)$
59	30 53	breldm	$⊢ f \underset{t}{⇝} (MetOpen (D)) \underset{v}{⇝} (f) \to f \in dom \underset{t}{⇝} (MetOpen (D))$
60	58 59	syl	$⊢ (f \in Cau (D) \land f : ℕ ⟶ H) \to f \in dom \underset{t}{⇝} (MetOpen (D))$
61	4 6 60	iscmet3i	$⊢ D \in CMet (H)$

Metamath Proof Explorer

Theorem hhsscms

Proof