Metamath Proof Explorer

Theorem 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 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
hhssims2.3 ⊢ 𝐷 = ( IndMet ‘ 𝑊 )
hhsscms.3 ⊢ 𝐻 ∈ Cℋ
Assertion hhsscms 𝐷 ∈ ( CMet ‘ 𝐻 )

Proof

Step Hyp Ref Expression
1 hhssims2.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
2 hhssims2.3 ⊢ 𝐷 = ( IndMet ‘ 𝑊 )
3 hhsscms.3 ⊢ 𝐻 ∈ Cℋ
4 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
5 3 chshii ⊢ 𝐻 ∈ Sℋ
6 1 2 5 hhssmet ⊢ 𝐷 ∈ ( Met ‘ 𝐻 )
7 simpl ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 ∈ ( Cau ‘ 𝐷 ) )
8 1 2 5 hhssims2 ⊢ 𝐷 = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) )
9 8 fveq2i ⊢ ( Cau ‘ 𝐷 ) = ( Cau ‘ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) )
10 7 9 eleqtrdi ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 ∈ ( Cau ‘ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) ) )
11 eqid ⊢ ( normℎ ∘ −ℎ ) = ( normℎ ∘ −ℎ )
12 11 hilxmet ⊢ ( normℎ ∘ −ℎ ) ∈ ( ∞Met ‘ ℋ )
13 simpr ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 : ℕ ⟶ 𝐻 )
14 causs ⊢ ( ( ( normℎ ∘ −ℎ ) ∈ ( ∞Met ‘ ℋ ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → ( 𝑓 ∈ ( Cau ‘ ( normℎ ∘ −ℎ ) ) ↔ 𝑓 ∈ ( Cau ‘ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) ) ) )
15 12 13 14 sylancr ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → ( 𝑓 ∈ ( Cau ‘ ( normℎ ∘ −ℎ ) ) ↔ 𝑓 ∈ ( Cau ‘ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) ) ) )
16 10 15 mpbird ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 ∈ ( Cau ‘ ( normℎ ∘ −ℎ ) ) )
17 3 chssii ⊢ 𝐻 ⊆ ℋ
18 fss ⊢ ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝐻 ⊆ ℋ ) → 𝑓 : ℕ ⟶ ℋ )
19 13 17 18 sylancl ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 : ℕ ⟶ ℋ )
20 ax-hilex ⊢ ℋ ∈ V
21 nnex ⊢ ℕ ∈ V
22 20 21 elmap ⊢ ( 𝑓 ∈ ( ℋ ↑m ℕ ) ↔ 𝑓 : ℕ ⟶ ℋ )
23 19 22 sylibr ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 ∈ ( ℋ ↑m ℕ ) )
24 eqid ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
25 24 11 hhims ⊢ ( normℎ ∘ −ℎ ) = ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
26 24 25 hhcau ⊢ Cauchy = ( ( Cau ‘ ( normℎ ∘ −ℎ ) ) ∩ ( ℋ ↑m ℕ ) )
27 26 elin2 ⊢ ( 𝑓 ∈ Cauchy ↔ ( 𝑓 ∈ ( Cau ‘ ( normℎ ∘ −ℎ ) ) ∧ 𝑓 ∈ ( ℋ ↑m ℕ ) ) )
28 16 23 27 sylanbrc ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 ∈ Cauchy )
29 ax-hcompl ⊢ ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝑓 ⇝𝑣 𝑥 )
30 vex ⊢ 𝑓 ∈ V
31 vex ⊢ 𝑥 ∈ V
32 30 31 breldm ⊢ ( 𝑓 ⇝𝑣 𝑥 → 𝑓 ∈ dom ⇝𝑣 )
33 32 rexlimivw ⊢ ( ∃ 𝑥 ∈ ℋ 𝑓 ⇝𝑣 𝑥 → 𝑓 ∈ dom ⇝𝑣 )
34 28 29 33 3syl ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 ∈ dom ⇝𝑣 )
35 hlimf ⊢ ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ
36 ffun ⊢ ( ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ → Fun ⇝𝑣 )
37 funfvbrb ⊢ ( Fun ⇝𝑣 → ( 𝑓 ∈ dom ⇝𝑣 ↔ 𝑓 ⇝𝑣 ( ⇝𝑣 ‘ 𝑓 ) ) )
38 35 36 37 mp2b ⊢ ( 𝑓 ∈ dom ⇝𝑣 ↔ 𝑓 ⇝𝑣 ( ⇝𝑣 ‘ 𝑓 ) )
39 34 38 sylib ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 ⇝𝑣 ( ⇝𝑣 ‘ 𝑓 ) )
40 eqid ⊢ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) = ( MetOpen ‘ ( normℎ ∘ −ℎ ) )
41 24 25 40 hhlm ⊢ ⇝𝑣 = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ) ↾ ( ℋ ↑m ℕ ) )
42 resss ⊢ ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ) ↾ ( ℋ ↑m ℕ ) ) ⊆ ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) )
43 41 42 eqsstri ⊢ ⇝𝑣 ⊆ ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) )
44 43 ssbri ⊢ ( 𝑓 ⇝𝑣 ( ⇝𝑣 ‘ 𝑓 ) → 𝑓 ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ) ( ⇝𝑣 ‘ 𝑓 ) )
45 39 44 syl ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ) ( ⇝𝑣 ‘ 𝑓 ) )
46 8 40 4 metrest ⊢ ( ( ( normℎ ∘ −ℎ ) ∈ ( ∞Met ‘ ℋ ) ∧ 𝐻 ⊆ ℋ ) → ( ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ↾t 𝐻 ) = ( MetOpen ‘ 𝐷 ) )
47 12 17 46 mp2an ⊢ ( ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ↾t 𝐻 ) = ( MetOpen ‘ 𝐷 )
48 47 eqcomi ⊢ ( MetOpen ‘ 𝐷 ) = ( ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ↾t 𝐻 )
49 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
50 3 a1i ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝐻 ∈ Cℋ )
51 40 mopntop ⊢ ( ( normℎ ∘ −ℎ ) ∈ ( ∞Met ‘ ℋ ) → ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ∈ Top )
52 12 51 mp1i ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ∈ Top )
53 fvex ⊢ ( ⇝𝑣 ‘ 𝑓 ) ∈ V
54 53 chlimi ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 ( ⇝𝑣 ‘ 𝑓 ) ) → ( ⇝𝑣 ‘ 𝑓 ) ∈ 𝐻 )
55 50 13 39 54 syl3anc ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → ( ⇝𝑣 ‘ 𝑓 ) ∈ 𝐻 )
56 1zzd ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 1 ∈ ℤ )
57 48 49 50 52 55 56 13 lmss ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → ( 𝑓 ( ⇝𝑡 ‘ ( MetOpen ‘ ( normℎ ∘ −ℎ ) ) ) ( ⇝𝑣 ‘ 𝑓 ) ↔ 𝑓 ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ( ⇝𝑣 ‘ 𝑓 ) ) )
58 45 57 mpbid ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ( ⇝𝑣 ‘ 𝑓 ) )
59 30 53 breldm ⊢ ( 𝑓 ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ( ⇝𝑣 ‘ 𝑓 ) → 𝑓 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) )
60 58 59 syl ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝐻 ) → 𝑓 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) )
61 4 6 60 iscmet3i ⊢ 𝐷 ∈ ( CMet ‘ 𝐻 )