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 β€˜ 𝐻 )