HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  chscllem2 Structured version   Visualization version   GIF version

Theorem chscllem2 28625
Description: Lemma for chscl 28628. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
chscl.1 (𝜑𝐴C )
chscl.2 (𝜑𝐵C )
chscl.3 (𝜑𝐵 ⊆ (⊥‘𝐴))
chscl.4 (𝜑𝐻:ℕ⟶(𝐴 + 𝐵))
chscl.5 (𝜑𝐻𝑣 𝑢)
chscl.6 𝐹 = (𝑛 ∈ ℕ ↦ ((proj𝐴)‘(𝐻𝑛)))
Assertion
Ref Expression
chscllem2 (𝜑𝐹 ∈ dom ⇝𝑣 )
Distinct variable groups:   𝑢,𝑛,𝐴   𝜑,𝑛   𝐵,𝑛,𝑢   𝑛,𝐻,𝑢
Allowed substitution hints:   𝜑(𝑢)   𝐹(𝑢,𝑛)

Proof of Theorem chscllem2
Dummy variables 𝑗 𝑥 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 chscl.1 . . . . 5 (𝜑𝐴C )
2 chscl.2 . . . . 5 (𝜑𝐵C )
3 chscl.3 . . . . 5 (𝜑𝐵 ⊆ (⊥‘𝐴))
4 chscl.4 . . . . 5 (𝜑𝐻:ℕ⟶(𝐴 + 𝐵))
5 chscl.5 . . . . 5 (𝜑𝐻𝑣 𝑢)
6 chscl.6 . . . . 5 𝐹 = (𝑛 ∈ ℕ ↦ ((proj𝐴)‘(𝐻𝑛)))
71, 2, 3, 4, 5, 6chscllem1 28624 . . . 4 (𝜑𝐹:ℕ⟶𝐴)
8 chss 28214 . . . . 5 (𝐴C𝐴 ⊆ ℋ)
91, 8syl 17 . . . 4 (𝜑𝐴 ⊆ ℋ)
107, 9fssd 6095 . . 3 (𝜑𝐹:ℕ⟶ ℋ)
11 hlimcaui 28221 . . . . . . 7 (𝐻𝑣 𝑢𝐻 ∈ Cauchy)
125, 11syl 17 . . . . . 6 (𝜑𝐻 ∈ Cauchy)
13 hcaucvg 28171 . . . . . 6 ((𝐻 ∈ Cauchy ∧ 𝑥 ∈ ℝ+) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥)
1412, 13sylan 487 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥)
15 eluznn 11796 . . . . . . . . 9 ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
1615adantll 750 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
17 chsh 28209 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴C𝐴S )
181, 17syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴S )
19 chsh 28209 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵C𝐵S )
202, 19syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵S )
21 shscl 28305 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴S𝐵S ) → (𝐴 + 𝐵) ∈ S )
2218, 20, 21syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 + 𝐵) ∈ S )
23 shss 28195 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 + 𝐵) ∈ S → (𝐴 + 𝐵) ⊆ ℋ)
2422, 23syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 + 𝐵) ⊆ ℋ)
2524adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → (𝐴 + 𝐵) ⊆ ℋ)
264ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → (𝐻𝑗) ∈ (𝐴 + 𝐵))
2725, 26sseldd 3637 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → (𝐻𝑗) ∈ ℋ)
2827adantrr 753 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐻𝑗) ∈ ℋ)
294, 24fssd 6095 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐻:ℕ⟶ ℋ)
3029adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐻:ℕ⟶ ℋ)
31 simprr 811 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈ ℕ)
3230, 31ffvelrnd 6400 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐻𝑘) ∈ ℋ)
33 hvsubcl 28002 . . . . . . . . . . . . . . . . . 18 (((𝐻𝑗) ∈ ℋ ∧ (𝐻𝑘) ∈ ℋ) → ((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ)
3428, 32, 33syl2anc 694 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ)
359adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → 𝐴 ⊆ ℋ)
367ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → (𝐹𝑗) ∈ 𝐴)
3735, 36sseldd 3637 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → (𝐹𝑗) ∈ ℋ)
3837adantrr 753 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹𝑗) ∈ ℋ)
399adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐴 ⊆ ℋ)
407adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐹:ℕ⟶𝐴)
4140, 31ffvelrnd 6400 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹𝑘) ∈ 𝐴)
4239, 41sseldd 3637 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹𝑘) ∈ ℋ)
43 hvsubcl 28002 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑗) ∈ ℋ ∧ (𝐹𝑘) ∈ ℋ) → ((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ)
4438, 42, 43syl2anc 694 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ)
45 hvsubcl 28002 . . . . . . . . . . . . . . . . 17 ((((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ ∧ ((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ) → (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ ℋ)
4634, 44, 45syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ ℋ)
47 normcl 28110 . . . . . . . . . . . . . . . 16 ((((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ ℋ → (norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) ∈ ℝ)
4846, 47syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) ∈ ℝ)
4948sqge0d 13076 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤ ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2))
50 normcl 28110 . . . . . . . . . . . . . . . . 17 (((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ → (norm‘((𝐹𝑗) − (𝐹𝑘))) ∈ ℝ)
5144, 50syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐹𝑗) − (𝐹𝑘))) ∈ ℝ)
5251resqcld 13075 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) ∈ ℝ)
5348resqcld 13075 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2) ∈ ℝ)
5452, 53addge01d 10653 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (0 ≤ ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2) ↔ ((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) ≤ (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2))))
5549, 54mpbid 222 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) ≤ (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2)))
5618adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐴S )
5736adantrr 753 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹𝑗) ∈ 𝐴)
58 shsubcl 28205 . . . . . . . . . . . . . . . . 17 ((𝐴S ∧ (𝐹𝑗) ∈ 𝐴 ∧ (𝐹𝑘) ∈ 𝐴) → ((𝐹𝑗) − (𝐹𝑘)) ∈ 𝐴)
5956, 57, 41, 58syl3anc 1366 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐹𝑗) − (𝐹𝑘)) ∈ 𝐴)
60 hvsubsub4 28045 . . . . . . . . . . . . . . . . . 18 ((((𝐻𝑗) ∈ ℋ ∧ (𝐻𝑘) ∈ ℋ) ∧ ((𝐹𝑗) ∈ ℋ ∧ (𝐹𝑘) ∈ ℋ)) → (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) = (((𝐻𝑗) − (𝐹𝑗)) − ((𝐻𝑘) − (𝐹𝑘))))
6128, 32, 38, 42, 60syl22anc 1367 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) = (((𝐻𝑗) − (𝐹𝑗)) − ((𝐻𝑘) − (𝐹𝑘))))
62 ocsh 28270 . . . . . . . . . . . . . . . . . . 19 (𝐴 ⊆ ℋ → (⊥‘𝐴) ∈ S )
6339, 62syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (⊥‘𝐴) ∈ S )
64 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑗 → (𝐻𝑛) = (𝐻𝑗))
6564fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑗 → ((proj𝐴)‘(𝐻𝑛)) = ((proj𝐴)‘(𝐻𝑗)))
66 fvex 6239 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((proj𝐴)‘(𝐻𝑗)) ∈ V
6765, 6, 66fvmpt 6321 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ ℕ → (𝐹𝑗) = ((proj𝐴)‘(𝐻𝑗)))
6867eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → ((proj𝐴)‘(𝐻𝑗)) = (𝐹𝑗))
6968adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ) → ((proj𝐴)‘(𝐻𝑗)) = (𝐹𝑗))
701adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → 𝐴C )
719, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (⊥‘𝐴) ∈ S )
72 shless 28346 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐵S ∧ (⊥‘𝐴) ∈ S𝐴S ) ∧ 𝐵 ⊆ (⊥‘𝐴)) → (𝐵 + 𝐴) ⊆ ((⊥‘𝐴) + 𝐴))
7320, 71, 18, 3, 72syl31anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐵 + 𝐴) ⊆ ((⊥‘𝐴) + 𝐴))
74 shscom 28306 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴S𝐵S ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
7518, 20, 74syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))
76 shscom 28306 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴S ∧ (⊥‘𝐴) ∈ S ) → (𝐴 + (⊥‘𝐴)) = ((⊥‘𝐴) + 𝐴))
7718, 71, 76syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 + (⊥‘𝐴)) = ((⊥‘𝐴) + 𝐴))
7873, 75, 773sstr4d 3681 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 + 𝐵) ⊆ (𝐴 + (⊥‘𝐴)))
7978adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → (𝐴 + 𝐵) ⊆ (𝐴 + (⊥‘𝐴)))
8079, 26sseldd 3637 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → (𝐻𝑗) ∈ (𝐴 + (⊥‘𝐴)))
81 pjpreeq 28385 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴C ∧ (𝐻𝑗) ∈ (𝐴 + (⊥‘𝐴))) → (((proj𝐴)‘(𝐻𝑗)) = (𝐹𝑗) ↔ ((𝐹𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻𝑗) = ((𝐹𝑗) + 𝑥))))
8270, 80, 81syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ) → (((proj𝐴)‘(𝐻𝑗)) = (𝐹𝑗) ↔ ((𝐹𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻𝑗) = ((𝐹𝑗) + 𝑥))))
8369, 82mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ) → ((𝐹𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻𝑗) = ((𝐹𝑗) + 𝑥)))
8483simprd 478 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ) → ∃𝑥 ∈ (⊥‘𝐴)(𝐻𝑗) = ((𝐹𝑗) + 𝑥))
8527adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝐻𝑗) ∈ ℋ)
8637adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝐹𝑗) ∈ ℋ)
87 shss 28195 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊥‘𝐴) ∈ S → (⊥‘𝐴) ⊆ ℋ)
8871, 87syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (⊥‘𝐴) ⊆ ℋ)
8988adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → (⊥‘𝐴) ⊆ ℋ)
9089sselda 3636 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → 𝑥 ∈ ℋ)
91 hvsubadd 28062 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐻𝑗) ∈ ℋ ∧ (𝐹𝑗) ∈ ℋ ∧ 𝑥 ∈ ℋ) → (((𝐻𝑗) − (𝐹𝑗)) = 𝑥 ↔ ((𝐹𝑗) + 𝑥) = (𝐻𝑗)))
9285, 86, 90, 91syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (((𝐻𝑗) − (𝐹𝑗)) = 𝑥 ↔ ((𝐹𝑗) + 𝑥) = (𝐻𝑗)))
93 eqcom 2658 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝐻𝑗) − (𝐹𝑗)) ↔ ((𝐻𝑗) − (𝐹𝑗)) = 𝑥)
94 eqcom 2658 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐻𝑗) = ((𝐹𝑗) + 𝑥) ↔ ((𝐹𝑗) + 𝑥) = (𝐻𝑗))
9592, 93, 943bitr4g 303 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝑥 = ((𝐻𝑗) − (𝐹𝑗)) ↔ (𝐻𝑗) = ((𝐹𝑗) + 𝑥)))
9695rexbidva 3078 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ) → (∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻𝑗) − (𝐹𝑗)) ↔ ∃𝑥 ∈ (⊥‘𝐴)(𝐻𝑗) = ((𝐹𝑗) + 𝑥)))
9784, 96mpbird 247 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → ∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻𝑗) − (𝐹𝑗)))
98 risset 3091 . . . . . . . . . . . . . . . . . . . 20 (((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴) ↔ ∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻𝑗) − (𝐹𝑗)))
9997, 98sylibr 224 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → ((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴))
10099adantrr 753 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴))
101 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑘 → (𝑗 ∈ ℕ ↔ 𝑘 ∈ ℕ))
102101anbi2d 740 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑘 → ((𝜑𝑗 ∈ ℕ) ↔ (𝜑𝑘 ∈ ℕ)))
103 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑘 → (𝐻𝑗) = (𝐻𝑘))
104 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑘 → (𝐹𝑗) = (𝐹𝑘))
105103, 104oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑘 → ((𝐻𝑗) − (𝐹𝑗)) = ((𝐻𝑘) − (𝐹𝑘)))
106105eleq1d 2715 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑘 → (((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴) ↔ ((𝐻𝑘) − (𝐹𝑘)) ∈ (⊥‘𝐴)))
107102, 106imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑘 → (((𝜑𝑗 ∈ ℕ) → ((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴)) ↔ ((𝜑𝑘 ∈ ℕ) → ((𝐻𝑘) − (𝐹𝑘)) ∈ (⊥‘𝐴))))
108107, 99chvarv 2299 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → ((𝐻𝑘) − (𝐹𝑘)) ∈ (⊥‘𝐴))
109108adantrl 752 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻𝑘) − (𝐹𝑘)) ∈ (⊥‘𝐴))
110 shsubcl 28205 . . . . . . . . . . . . . . . . . 18 (((⊥‘𝐴) ∈ S ∧ ((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴) ∧ ((𝐻𝑘) − (𝐹𝑘)) ∈ (⊥‘𝐴)) → (((𝐻𝑗) − (𝐹𝑗)) − ((𝐻𝑘) − (𝐹𝑘))) ∈ (⊥‘𝐴))
11163, 100, 109, 110syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻𝑗) − (𝐹𝑗)) − ((𝐻𝑘) − (𝐹𝑘))) ∈ (⊥‘𝐴))
11261, 111eqeltrd 2730 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ (⊥‘𝐴))
113 shocorth 28279 . . . . . . . . . . . . . . . . 17 (𝐴S → ((((𝐹𝑗) − (𝐹𝑘)) ∈ 𝐴 ∧ (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ (⊥‘𝐴)) → (((𝐹𝑗) − (𝐹𝑘)) ·ih (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = 0))
11456, 113syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((((𝐹𝑗) − (𝐹𝑘)) ∈ 𝐴 ∧ (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ (⊥‘𝐴)) → (((𝐹𝑗) − (𝐹𝑘)) ·ih (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = 0))
11559, 112, 114mp2and 715 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐹𝑗) − (𝐹𝑘)) ·ih (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = 0)
116 normpyth 28130 . . . . . . . . . . . . . . . 16 ((((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ ∧ (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ ℋ) → ((((𝐹𝑗) − (𝐹𝑘)) ·ih (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = 0 → ((norm‘(((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))))↑2) = (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2))))
11744, 46, 116syl2anc 694 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((((𝐹𝑗) − (𝐹𝑘)) ·ih (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = 0 → ((norm‘(((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))))↑2) = (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2))))
118115, 117mpd 15 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘(((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))))↑2) = (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2)))
119 hvpncan3 28027 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ ∧ ((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ) → (((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = ((𝐻𝑗) − (𝐻𝑘)))
12044, 34, 119syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = ((𝐻𝑗) − (𝐻𝑘)))
121120fveq2d 6233 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘(((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))) = (norm‘((𝐻𝑗) − (𝐻𝑘))))
122121oveq1d 6705 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘(((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))))↑2) = ((norm‘((𝐻𝑗) − (𝐻𝑘)))↑2))
123118, 122eqtr3d 2687 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2)) = ((norm‘((𝐻𝑗) − (𝐻𝑘)))↑2))
12455, 123breqtrd 4711 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) ≤ ((norm‘((𝐻𝑗) − (𝐻𝑘)))↑2))
125 normcl 28110 . . . . . . . . . . . . . 14 (((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ → (norm‘((𝐻𝑗) − (𝐻𝑘))) ∈ ℝ)
12634, 125syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐻𝑗) − (𝐻𝑘))) ∈ ℝ)
127 normge0 28111 . . . . . . . . . . . . . 14 (((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ → 0 ≤ (norm‘((𝐹𝑗) − (𝐹𝑘))))
12844, 127syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤ (norm‘((𝐹𝑗) − (𝐹𝑘))))
129 normge0 28111 . . . . . . . . . . . . . 14 (((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ → 0 ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))))
13034, 129syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))))
13151, 126, 128, 130le2sqd 13084 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘((𝐹𝑗) − (𝐹𝑘))) ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))) ↔ ((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) ≤ ((norm‘((𝐻𝑗) − (𝐻𝑘)))↑2)))
132124, 131mpbird 247 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐹𝑗) − (𝐹𝑘))) ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))))
133132adantlr 751 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐹𝑗) − (𝐹𝑘))) ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))))
13451adantlr 751 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐹𝑗) − (𝐹𝑘))) ∈ ℝ)
135126adantlr 751 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐻𝑗) − (𝐻𝑘))) ∈ ℝ)
136 rpre 11877 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
137136ad2antlr 763 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝑥 ∈ ℝ)
138 lelttr 10166 . . . . . . . . . . 11 (((norm‘((𝐹𝑗) − (𝐹𝑘))) ∈ ℝ ∧ (norm‘((𝐻𝑗) − (𝐻𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((norm‘((𝐹𝑗) − (𝐹𝑘))) ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))) ∧ (norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥) → (norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
139134, 135, 137, 138syl3anc 1366 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((norm‘((𝐹𝑗) − (𝐹𝑘))) ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))) ∧ (norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥) → (norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
140133, 139mpand 711 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥 → (norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
141140anassrs 681 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥 → (norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
14216, 141syldan 486 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑗)) → ((norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥 → (norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
143142ralimdva 2991 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥 → ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
144143reximdva 3046 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
14514, 144mpd 15 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥)
146145ralrimiva 2995 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥)
147 hcau 28169 . . 3 (𝐹 ∈ Cauchy ↔ (𝐹:ℕ⟶ ℋ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
14810, 146, 147sylanbrc 699 . 2 (𝜑𝐹 ∈ Cauchy)
149 ax-hcompl 28187 . 2 (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹𝑣 𝑥)
150 hlimf 28222 . . . . 5 𝑣 :dom ⇝𝑣 ⟶ ℋ
151 ffn 6083 . . . . 5 ( ⇝𝑣 :dom ⇝𝑣 ⟶ ℋ → ⇝𝑣 Fn dom ⇝𝑣 )
152150, 151ax-mp 5 . . . 4 𝑣 Fn dom ⇝𝑣
153 fnbr 6031 . . . 4 (( ⇝𝑣 Fn dom ⇝𝑣𝐹𝑣 𝑥) → 𝐹 ∈ dom ⇝𝑣 )
154152, 153mpan 706 . . 3 (𝐹𝑣 𝑥𝐹 ∈ dom ⇝𝑣 )
155154rexlimivw 3058 . 2 (∃𝑥 ∈ ℋ 𝐹𝑣 𝑥𝐹 ∈ dom ⇝𝑣 )
156148, 149, 1553syl 18 1 (𝜑𝐹 ∈ dom ⇝𝑣 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wral 2941  wrex 2942  wss 3607   class class class wbr 4685  cmpt 4762  dom cdm 5143   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  cr 9973  0cc0 9974   + caddc 9977   < clt 10112  cle 10113  cn 11058  2c2 11108  cuz 11725  +crp 11870  cexp 12900  chil 27904   + cva 27905   ·ih csp 27907  normcno 27908   cmv 27910  Cauchyccau 27911  𝑣 chli 27912   S csh 27913   C cch 27914  cort 27915   + cph 27916  projcpjh 27922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054  ax-hilex 27984  ax-hfvadd 27985  ax-hvcom 27986  ax-hvass 27987  ax-hv0cl 27988  ax-hvaddid 27989  ax-hfvmul 27990  ax-hvmulid 27991  ax-hvmulass 27992  ax-hvdistr1 27993  ax-hvdistr2 27994  ax-hvmul0 27995  ax-hfi 28064  ax-his1 28067  ax-his2 28068  ax-his3 28069  ax-his4 28070  ax-hcompl 28187
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-icc 12220  df-seq 12842  df-exp 12901  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-topgen 16151  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-bases 20798  df-lm 21081  df-haus 21167  df-cau 23100  df-grpo 27475  df-gid 27476  df-ginv 27477  df-gdiv 27478  df-ablo 27527  df-vc 27542  df-nv 27575  df-va 27578  df-ba 27579  df-sm 27580  df-0v 27581  df-vs 27582  df-nmcv 27583  df-ims 27584  df-hnorm 27953  df-hvsub 27956  df-hlim 27957  df-hcau 27958  df-sh 28192  df-ch 28206  df-oc 28237  df-ch0 28238  df-shs 28295  df-pjh 28382
This theorem is referenced by:  chscllem4  28627
  Copyright terms: Public domain W3C validator