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

Theorem chscllem2 27881
Description: Lemma for chscl 27884. (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 27880 . . . 4 (𝜑𝐹:ℕ⟶𝐴)
8 chss 27470 . . . . 5 (𝐴C𝐴 ⊆ ℋ)
91, 8syl 17 . . . 4 (𝜑𝐴 ⊆ ℋ)
107, 9fssd 5970 . . 3 (𝜑𝐹:ℕ⟶ ℋ)
11 hlimcaui 27477 . . . . . . 7 (𝐻𝑣 𝑢𝐻 ∈ Cauchy)
125, 11syl 17 . . . . . 6 (𝜑𝐻 ∈ Cauchy)
13 hcaucvg 27427 . . . . . 6 ((𝐻 ∈ Cauchy ∧ 𝑥 ∈ ℝ+) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥)
1412, 13sylan 487 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥)
15 eluznn 11634 . . . . . . . . 9 ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
1615adantll 746 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
17 chsh 27465 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴C𝐴S )
181, 17syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴S )
19 chsh 27465 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵C𝐵S )
202, 19syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵S )
21 shscl 27561 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴S𝐵S ) → (𝐴 + 𝐵) ∈ S )
2218, 20, 21syl2anc 691 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 + 𝐵) ∈ S )
23 shss 27451 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 + 𝐵) ∈ S → (𝐴 + 𝐵) ⊆ ℋ)
2422, 23syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 + 𝐵) ⊆ ℋ)
2524adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → (𝐴 + 𝐵) ⊆ ℋ)
264ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → (𝐻𝑗) ∈ (𝐴 + 𝐵))
2725, 26sseldd 3569 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → (𝐻𝑗) ∈ ℋ)
2827adantrr 749 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐻𝑗) ∈ ℋ)
294, 24fssd 5970 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐻:ℕ⟶ ℋ)
3029adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐻:ℕ⟶ ℋ)
31 simprr 792 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈ ℕ)
3230, 31ffvelrnd 6268 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐻𝑘) ∈ ℋ)
33 hvsubcl 27258 . . . . . . . . . . . . . . . . . 18 (((𝐻𝑗) ∈ ℋ ∧ (𝐻𝑘) ∈ ℋ) → ((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ)
3428, 32, 33syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ)
359adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → 𝐴 ⊆ ℋ)
367ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → (𝐹𝑗) ∈ 𝐴)
3735, 36sseldd 3569 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → (𝐹𝑗) ∈ ℋ)
3837adantrr 749 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹𝑗) ∈ ℋ)
399adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐴 ⊆ ℋ)
407adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐹:ℕ⟶𝐴)
4140, 31ffvelrnd 6268 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹𝑘) ∈ 𝐴)
4239, 41sseldd 3569 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹𝑘) ∈ ℋ)
43 hvsubcl 27258 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑗) ∈ ℋ ∧ (𝐹𝑘) ∈ ℋ) → ((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ)
4438, 42, 43syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ)
45 hvsubcl 27258 . . . . . . . . . . . . . . . . 17 ((((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ ∧ ((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ) → (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ ℋ)
4634, 44, 45syl2anc 691 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ ℋ)
47 normcl 27366 . . . . . . . . . . . . . . . 16 ((((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ ℋ → (norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) ∈ ℝ)
4846, 47syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) ∈ ℝ)
4948sqge0d 12898 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤ ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2))
50 normcl 27366 . . . . . . . . . . . . . . . . 17 (((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ → (norm‘((𝐹𝑗) − (𝐹𝑘))) ∈ ℝ)
5144, 50syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐹𝑗) − (𝐹𝑘))) ∈ ℝ)
5251resqcld 12897 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) ∈ ℝ)
5348resqcld 12897 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2) ∈ ℝ)
5452, 53addge01d 10494 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (0 ≤ ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2) ↔ ((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) ≤ (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2))))
5549, 54mpbid 221 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) ≤ (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2)))
5618adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐴S )
5736adantrr 749 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹𝑗) ∈ 𝐴)
58 shsubcl 27461 . . . . . . . . . . . . . . . . 17 ((𝐴S ∧ (𝐹𝑗) ∈ 𝐴 ∧ (𝐹𝑘) ∈ 𝐴) → ((𝐹𝑗) − (𝐹𝑘)) ∈ 𝐴)
5956, 57, 41, 58syl3anc 1318 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐹𝑗) − (𝐹𝑘)) ∈ 𝐴)
60 hvsubsub4 27301 . . . . . . . . . . . . . . . . . 18 ((((𝐻𝑗) ∈ ℋ ∧ (𝐻𝑘) ∈ ℋ) ∧ ((𝐹𝑗) ∈ ℋ ∧ (𝐹𝑘) ∈ ℋ)) → (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) = (((𝐻𝑗) − (𝐹𝑗)) − ((𝐻𝑘) − (𝐹𝑘))))
6128, 32, 38, 42, 60syl22anc 1319 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) = (((𝐻𝑗) − (𝐹𝑗)) − ((𝐻𝑘) − (𝐹𝑘))))
62 ocsh 27526 . . . . . . . . . . . . . . . . . . 19 (𝐴 ⊆ ℋ → (⊥‘𝐴) ∈ S )
6339, 62syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (⊥‘𝐴) ∈ S )
64 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑗 → (𝐻𝑛) = (𝐻𝑗))
6564fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑗 → ((proj𝐴)‘(𝐻𝑛)) = ((proj𝐴)‘(𝐻𝑗)))
66 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((proj𝐴)‘(𝐻𝑗)) ∈ V
6765, 6, 66fvmpt 6191 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ ℕ → (𝐹𝑗) = ((proj𝐴)‘(𝐻𝑗)))
6867eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → ((proj𝐴)‘(𝐻𝑗)) = (𝐹𝑗))
6968adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ) → ((proj𝐴)‘(𝐻𝑗)) = (𝐹𝑗))
701adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → 𝐴C )
719, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (⊥‘𝐴) ∈ S )
72 shless 27602 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐵S ∧ (⊥‘𝐴) ∈ S𝐴S ) ∧ 𝐵 ⊆ (⊥‘𝐴)) → (𝐵 + 𝐴) ⊆ ((⊥‘𝐴) + 𝐴))
7320, 71, 18, 3, 72syl31anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐵 + 𝐴) ⊆ ((⊥‘𝐴) + 𝐴))
74 shscom 27562 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴S𝐵S ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
7518, 20, 74syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))
76 shscom 27562 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴S ∧ (⊥‘𝐴) ∈ S ) → (𝐴 + (⊥‘𝐴)) = ((⊥‘𝐴) + 𝐴))
7718, 71, 76syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 + (⊥‘𝐴)) = ((⊥‘𝐴) + 𝐴))
7873, 75, 773sstr4d 3611 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 + 𝐵) ⊆ (𝐴 + (⊥‘𝐴)))
7978adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → (𝐴 + 𝐵) ⊆ (𝐴 + (⊥‘𝐴)))
8079, 26sseldd 3569 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ ℕ) → (𝐻𝑗) ∈ (𝐴 + (⊥‘𝐴)))
81 pjpreeq 27641 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴C ∧ (𝐻𝑗) ∈ (𝐴 + (⊥‘𝐴))) → (((proj𝐴)‘(𝐻𝑗)) = (𝐹𝑗) ↔ ((𝐹𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻𝑗) = ((𝐹𝑗) + 𝑥))))
8270, 80, 81syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ℕ) → (((proj𝐴)‘(𝐻𝑗)) = (𝐹𝑗) ↔ ((𝐹𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻𝑗) = ((𝐹𝑗) + 𝑥))))
8369, 82mpbid 221 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ) → ((𝐹𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻𝑗) = ((𝐹𝑗) + 𝑥)))
8483simprd 478 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ) → ∃𝑥 ∈ (⊥‘𝐴)(𝐻𝑗) = ((𝐹𝑗) + 𝑥))
8527adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝐻𝑗) ∈ ℋ)
8637adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝐹𝑗) ∈ ℋ)
87 shss 27451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊥‘𝐴) ∈ S → (⊥‘𝐴) ⊆ ℋ)
8871, 87syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (⊥‘𝐴) ⊆ ℋ)
8988adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ℕ) → (⊥‘𝐴) ⊆ ℋ)
9089sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → 𝑥 ∈ ℋ)
91 hvsubadd 27318 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐻𝑗) ∈ ℋ ∧ (𝐹𝑗) ∈ ℋ ∧ 𝑥 ∈ ℋ) → (((𝐻𝑗) − (𝐹𝑗)) = 𝑥 ↔ ((𝐹𝑗) + 𝑥) = (𝐻𝑗)))
9285, 86, 90, 91syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (((𝐻𝑗) − (𝐹𝑗)) = 𝑥 ↔ ((𝐹𝑗) + 𝑥) = (𝐻𝑗)))
93 eqcom 2617 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝐻𝑗) − (𝐹𝑗)) ↔ ((𝐻𝑗) − (𝐹𝑗)) = 𝑥)
94 eqcom 2617 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐻𝑗) = ((𝐹𝑗) + 𝑥) ↔ ((𝐹𝑗) + 𝑥) = (𝐻𝑗))
9592, 93, 943bitr4g 302 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝑥 = ((𝐻𝑗) − (𝐹𝑗)) ↔ (𝐻𝑗) = ((𝐹𝑗) + 𝑥)))
9695rexbidva 3031 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ) → (∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻𝑗) − (𝐹𝑗)) ↔ ∃𝑥 ∈ (⊥‘𝐴)(𝐻𝑗) = ((𝐹𝑗) + 𝑥)))
9784, 96mpbird 246 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ) → ∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻𝑗) − (𝐹𝑗)))
98 risset 3044 . . . . . . . . . . . . . . . . . . . 20 (((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴) ↔ ∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻𝑗) − (𝐹𝑗)))
9997, 98sylibr 223 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → ((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴))
10099adantrr 749 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴))
101 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑘 → (𝑗 ∈ ℕ ↔ 𝑘 ∈ ℕ))
102101anbi2d 736 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑘 → ((𝜑𝑗 ∈ ℕ) ↔ (𝜑𝑘 ∈ ℕ)))
103 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑘 → (𝐻𝑗) = (𝐻𝑘))
104 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑘 → (𝐹𝑗) = (𝐹𝑘))
105103, 104oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑘 → ((𝐻𝑗) − (𝐹𝑗)) = ((𝐻𝑘) − (𝐹𝑘)))
106105eleq1d 2672 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑘 → (((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴) ↔ ((𝐻𝑘) − (𝐹𝑘)) ∈ (⊥‘𝐴)))
107102, 106imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑘 → (((𝜑𝑗 ∈ ℕ) → ((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴)) ↔ ((𝜑𝑘 ∈ ℕ) → ((𝐻𝑘) − (𝐹𝑘)) ∈ (⊥‘𝐴))))
108107, 99chvarv 2251 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → ((𝐻𝑘) − (𝐹𝑘)) ∈ (⊥‘𝐴))
109108adantrl 748 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻𝑘) − (𝐹𝑘)) ∈ (⊥‘𝐴))
110 shsubcl 27461 . . . . . . . . . . . . . . . . . 18 (((⊥‘𝐴) ∈ S ∧ ((𝐻𝑗) − (𝐹𝑗)) ∈ (⊥‘𝐴) ∧ ((𝐻𝑘) − (𝐹𝑘)) ∈ (⊥‘𝐴)) → (((𝐻𝑗) − (𝐹𝑗)) − ((𝐻𝑘) − (𝐹𝑘))) ∈ (⊥‘𝐴))
11163, 100, 109, 110syl3anc 1318 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻𝑗) − (𝐹𝑗)) − ((𝐻𝑘) − (𝐹𝑘))) ∈ (⊥‘𝐴))
11261, 111eqeltrd 2688 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ (⊥‘𝐴))
113 shocorth 27535 . . . . . . . . . . . . . . . . 17 (𝐴S → ((((𝐹𝑗) − (𝐹𝑘)) ∈ 𝐴 ∧ (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ (⊥‘𝐴)) → (((𝐹𝑗) − (𝐹𝑘)) ·ih (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = 0))
11456, 113syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((((𝐹𝑗) − (𝐹𝑘)) ∈ 𝐴 ∧ (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ (⊥‘𝐴)) → (((𝐹𝑗) − (𝐹𝑘)) ·ih (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = 0))
11559, 112, 114mp2and 711 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐹𝑗) − (𝐹𝑘)) ·ih (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = 0)
116 normpyth 27386 . . . . . . . . . . . . . . . 16 ((((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ ∧ (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))) ∈ ℋ) → ((((𝐹𝑗) − (𝐹𝑘)) ·ih (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = 0 → ((norm‘(((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))))↑2) = (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2))))
11744, 46, 116syl2anc 691 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((((𝐹𝑗) − (𝐹𝑘)) ·ih (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = 0 → ((norm‘(((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))))↑2) = (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2))))
118115, 117mpd 15 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘(((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))))↑2) = (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2)))
119 hvpncan3 27283 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ ∧ ((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ) → (((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = ((𝐻𝑗) − (𝐻𝑘)))
12044, 34, 119syl2anc 691 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))) = ((𝐻𝑗) − (𝐻𝑘)))
121120fveq2d 6107 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘(((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))) = (norm‘((𝐻𝑗) − (𝐻𝑘))))
122121oveq1d 6564 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘(((𝐹𝑗) − (𝐹𝑘)) + (((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘)))))↑2) = ((norm‘((𝐻𝑗) − (𝐻𝑘)))↑2))
123118, 122eqtr3d 2646 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) + ((norm‘(((𝐻𝑗) − (𝐻𝑘)) − ((𝐹𝑗) − (𝐹𝑘))))↑2)) = ((norm‘((𝐻𝑗) − (𝐻𝑘)))↑2))
12455, 123breqtrd 4609 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) ≤ ((norm‘((𝐻𝑗) − (𝐻𝑘)))↑2))
125 normcl 27366 . . . . . . . . . . . . . 14 (((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ → (norm‘((𝐻𝑗) − (𝐻𝑘))) ∈ ℝ)
12634, 125syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐻𝑗) − (𝐻𝑘))) ∈ ℝ)
127 normge0 27367 . . . . . . . . . . . . . 14 (((𝐹𝑗) − (𝐹𝑘)) ∈ ℋ → 0 ≤ (norm‘((𝐹𝑗) − (𝐹𝑘))))
12844, 127syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤ (norm‘((𝐹𝑗) − (𝐹𝑘))))
129 normge0 27367 . . . . . . . . . . . . . 14 (((𝐻𝑗) − (𝐻𝑘)) ∈ ℋ → 0 ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))))
13034, 129syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))))
13151, 126, 128, 130le2sqd 12906 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘((𝐹𝑗) − (𝐹𝑘))) ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))) ↔ ((norm‘((𝐹𝑗) − (𝐹𝑘)))↑2) ≤ ((norm‘((𝐻𝑗) − (𝐻𝑘)))↑2)))
132124, 131mpbird 246 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐹𝑗) − (𝐹𝑘))) ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))))
133132adantlr 747 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐹𝑗) − (𝐹𝑘))) ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))))
13451adantlr 747 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐹𝑗) − (𝐹𝑘))) ∈ ℝ)
135126adantlr 747 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (norm‘((𝐻𝑗) − (𝐻𝑘))) ∈ ℝ)
136 rpre 11715 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
137136ad2antlr 759 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝑥 ∈ ℝ)
138 lelttr 10007 . . . . . . . . . . 11 (((norm‘((𝐹𝑗) − (𝐹𝑘))) ∈ ℝ ∧ (norm‘((𝐻𝑗) − (𝐻𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((norm‘((𝐹𝑗) − (𝐹𝑘))) ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))) ∧ (norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥) → (norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
139134, 135, 137, 138syl3anc 1318 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((norm‘((𝐹𝑗) − (𝐹𝑘))) ≤ (norm‘((𝐻𝑗) − (𝐻𝑘))) ∧ (norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥) → (norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
140133, 139mpand 707 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥 → (norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
141140anassrs 678 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥 → (norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
14216, 141syldan 486 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑗)) → ((norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥 → (norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
143142ralimdva 2945 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥 → ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
144143reximdva 3000 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐻𝑗) − (𝐻𝑘))) < 𝑥 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
14514, 144mpd 15 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥)
146145ralrimiva 2949 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥)
147 hcau 27425 . . 3 (𝐹 ∈ Cauchy ↔ (𝐹:ℕ⟶ ℋ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(norm‘((𝐹𝑗) − (𝐹𝑘))) < 𝑥))
14810, 146, 147sylanbrc 695 . 2 (𝜑𝐹 ∈ Cauchy)
149 ax-hcompl 27443 . 2 (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹𝑣 𝑥)
150 hlimf 27478 . . . . 5 𝑣 :dom ⇝𝑣 ⟶ ℋ
151 ffn 5958 . . . . 5 ( ⇝𝑣 :dom ⇝𝑣 ⟶ ℋ → ⇝𝑣 Fn dom ⇝𝑣 )
152150, 151ax-mp 5 . . . 4 𝑣 Fn dom ⇝𝑣
153 fnbr 5907 . . . 4 (( ⇝𝑣 Fn dom ⇝𝑣𝐹𝑣 𝑥) → 𝐹 ∈ dom ⇝𝑣 )
154152, 153mpan 702 . . 3 (𝐹𝑣 𝑥𝐹 ∈ dom ⇝𝑣 )
155154rexlimivw 3011 . 2 (∃𝑥 ∈ ℋ 𝐹𝑣 𝑥𝐹 ∈ dom ⇝𝑣 )
156148, 149, 1553syl 18 1 (𝜑𝐹 ∈ dom ⇝𝑣 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wral 2896  wrex 2897  wss 3540   class class class wbr 4583  cmpt 4643  dom cdm 5038   Fn wfn 5799  wf 5800  cfv 5804  (class class class)co 6549  cr 9814  0cc0 9815   + caddc 9818   < clt 9953  cle 9954  cn 10897  2c2 10947  cuz 11563  +crp 11708  cexp 12722  chil 27160   + cva 27161   ·ih csp 27163  normcno 27164   cmv 27166  Cauchyccau 27167  𝑣 chli 27168   S csh 27169   C cch 27170  cort 27171   + cph 27172  projcpjh 27178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895  ax-hilex 27240  ax-hfvadd 27241  ax-hvcom 27242  ax-hvass 27243  ax-hv0cl 27244  ax-hvaddid 27245  ax-hfvmul 27246  ax-hvmulid 27247  ax-hvmulass 27248  ax-hvdistr1 27249  ax-hvdistr2 27250  ax-hvmul0 27251  ax-hfi 27320  ax-his1 27323  ax-his2 27324  ax-his3 27325  ax-his4 27326  ax-hcompl 27443
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-icc 12053  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-lm 20843  df-haus 20929  df-cau 22862  df-grpo 26731  df-gid 26732  df-ginv 26733  df-gdiv 26734  df-ablo 26783  df-vc 26798  df-nv 26831  df-va 26834  df-ba 26835  df-sm 26836  df-0v 26837  df-vs 26838  df-nmcv 26839  df-ims 26840  df-hnorm 27209  df-hvsub 27212  df-hlim 27213  df-hcau 27214  df-sh 27448  df-ch 27462  df-oc 27493  df-ch0 27494  df-shs 27551  df-pjh 27638
This theorem is referenced by:  chscllem4  27883
  Copyright terms: Public domain W3C validator