Metamath Proof Explorer

Theorem h2hcau

Description: The Cauchy sequences of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses h2hc.1 ⊒ π‘ˆ = ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩
h2hc.2 ⊒ π‘ˆ ∈ NrmCVec
h2hc.3 ⊒ β„‹ = ( BaseSet β€˜ π‘ˆ )
h2hc.4 ⊒ 𝐷 = ( IndMet β€˜ π‘ˆ )
Assertion h2hcau Cauchy = ( ( Cau β€˜ 𝐷 ) ∩ ( β„‹ ↑m β„• ) )

Proof

Step Hyp Ref Expression
1 h2hc.1 ⊒ π‘ˆ = ⟨ ⟨ +β„Ž , Β·β„Ž ⟩ , normβ„Ž ⟩
2 h2hc.2 ⊒ π‘ˆ ∈ NrmCVec
3 h2hc.3 ⊒ β„‹ = ( BaseSet β€˜ π‘ˆ )
4 h2hc.4 ⊒ 𝐷 = ( IndMet β€˜ π‘ˆ )
5 df-rab ⊒ { 𝑓 ∈ ( β„‹ ↑m β„• ) ∣ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ } = { 𝑓 ∣ ( 𝑓 ∈ ( β„‹ ↑m β„• ) ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ ) }
6 df-hcau ⊒ Cauchy = { 𝑓 ∈ ( β„‹ ↑m β„• ) ∣ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ }
7 elin ⊒ ( 𝑓 ∈ ( ( Cau β€˜ 𝐷 ) ∩ ( β„‹ ↑m β„• ) ) ↔ ( 𝑓 ∈ ( Cau β€˜ 𝐷 ) ∧ 𝑓 ∈ ( β„‹ ↑m β„• ) ) )
8 ancom ⊒ ( ( 𝑓 ∈ ( Cau β€˜ 𝐷 ) ∧ 𝑓 ∈ ( β„‹ ↑m β„• ) ) ↔ ( 𝑓 ∈ ( β„‹ ↑m β„• ) ∧ 𝑓 ∈ ( Cau β€˜ 𝐷 ) ) )
9 3 hlex ⊒ β„‹ ∈ V
10 nnex ⊒ β„• ∈ V
11 9 10 elmap ⊒ ( 𝑓 ∈ ( β„‹ ↑m β„• ) ↔ 𝑓 : β„• ⟢ β„‹ )
12 nnuz ⊒ β„• = ( β„€β‰₯ β€˜ 1 )
13 3 4 imsxmet ⊒ ( π‘ˆ ∈ NrmCVec β†’ 𝐷 ∈ ( ∞Met β€˜ β„‹ ) )
14 2 13 mp1i ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ 𝐷 ∈ ( ∞Met β€˜ β„‹ ) )
15 1zzd ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ 1 ∈ β„€ )
16 eqidd ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘˜ ∈ β„• ) β†’ ( 𝑓 β€˜ π‘˜ ) = ( 𝑓 β€˜ π‘˜ ) )
17 eqidd ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ 𝑗 ∈ β„• ) β†’ ( 𝑓 β€˜ 𝑗 ) = ( 𝑓 β€˜ 𝑗 ) )
18 id ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ 𝑓 : β„• ⟢ β„‹ )
19 12 14 15 16 17 18 iscauf ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ ( 𝑓 ∈ ( Cau β€˜ 𝐷 ) ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( ( 𝑓 β€˜ 𝑗 ) 𝐷 ( 𝑓 β€˜ π‘˜ ) ) < π‘₯ ) )
20 ffvelcdm ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ 𝑗 ∈ β„• ) β†’ ( 𝑓 β€˜ 𝑗 ) ∈ β„‹ )
21 20 adantr ⊒ ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ 𝑗 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ) β†’ ( 𝑓 β€˜ 𝑗 ) ∈ β„‹ )
22 eluznn ⊒ ( ( 𝑗 ∈ β„• ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ) β†’ π‘˜ ∈ β„• )
23 ffvelcdm ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ π‘˜ ∈ β„• ) β†’ ( 𝑓 β€˜ π‘˜ ) ∈ β„‹ )
24 22 23 sylan2 ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ ( 𝑗 ∈ β„• ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ) ) β†’ ( 𝑓 β€˜ π‘˜ ) ∈ β„‹ )
25 24 anassrs ⊒ ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ 𝑗 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ) β†’ ( 𝑓 β€˜ π‘˜ ) ∈ β„‹ )
26 1 2 3 4 h2hmetdval ⊒ ( ( ( 𝑓 β€˜ 𝑗 ) ∈ β„‹ ∧ ( 𝑓 β€˜ π‘˜ ) ∈ β„‹ ) β†’ ( ( 𝑓 β€˜ 𝑗 ) 𝐷 ( 𝑓 β€˜ π‘˜ ) ) = ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) )
27 21 25 26 syl2anc ⊒ ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ 𝑗 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ) β†’ ( ( 𝑓 β€˜ 𝑗 ) 𝐷 ( 𝑓 β€˜ π‘˜ ) ) = ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) )
28 27 breq1d ⊒ ( ( ( 𝑓 : β„• ⟢ β„‹ ∧ 𝑗 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ) β†’ ( ( ( 𝑓 β€˜ 𝑗 ) 𝐷 ( 𝑓 β€˜ π‘˜ ) ) < π‘₯ ↔ ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ ) )
29 28 ralbidva ⊒ ( ( 𝑓 : β„• ⟢ β„‹ ∧ 𝑗 ∈ β„• ) β†’ ( βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( ( 𝑓 β€˜ 𝑗 ) 𝐷 ( 𝑓 β€˜ π‘˜ ) ) < π‘₯ ↔ βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ ) )
30 29 rexbidva ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ ( βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( ( 𝑓 β€˜ 𝑗 ) 𝐷 ( 𝑓 β€˜ π‘˜ ) ) < π‘₯ ↔ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ ) )
31 30 ralbidv ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ ( βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( ( 𝑓 β€˜ 𝑗 ) 𝐷 ( 𝑓 β€˜ π‘˜ ) ) < π‘₯ ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ ) )
32 19 31 bitrd ⊒ ( 𝑓 : β„• ⟢ β„‹ β†’ ( 𝑓 ∈ ( Cau β€˜ 𝐷 ) ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ ) )
33 11 32 sylbi ⊒ ( 𝑓 ∈ ( β„‹ ↑m β„• ) β†’ ( 𝑓 ∈ ( Cau β€˜ 𝐷 ) ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ ) )
34 33 pm5.32i ⊒ ( ( 𝑓 ∈ ( β„‹ ↑m β„• ) ∧ 𝑓 ∈ ( Cau β€˜ 𝐷 ) ) ↔ ( 𝑓 ∈ ( β„‹ ↑m β„• ) ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ ) )
35 7 8 34 3bitri ⊒ ( 𝑓 ∈ ( ( Cau β€˜ 𝐷 ) ∩ ( β„‹ ↑m β„• ) ) ↔ ( 𝑓 ∈ ( β„‹ ↑m β„• ) ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ ) )
36 35 eqabi ⊒ ( ( Cau β€˜ 𝐷 ) ∩ ( β„‹ ↑m β„• ) ) = { 𝑓 ∣ ( 𝑓 ∈ ( β„‹ ↑m β„• ) ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑗 ∈ β„• βˆ€ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝑗 ) ( normβ„Ž β€˜ ( ( 𝑓 β€˜ 𝑗 ) βˆ’β„Ž ( 𝑓 β€˜ π‘˜ ) ) ) < π‘₯ ) }
37 5 6 36 3eqtr4i ⊒ Cauchy = ( ( Cau β€˜ 𝐷 ) ∩ ( β„‹ ↑m β„• ) )