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 ⊢ W = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
hhssims2.3 ⊢ D = IndMet ⁡ W
hhsscms.3 ⊢ H ∈ C ℋ
Assertion hhsscms ⊢ D ∈ CMet ⁡ H

Proof

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