Metamath Proof Explorer

Theorem chscllem2

Description: Lemma for chscl . (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses chscl.1 ⊢ ( 𝜑 → 𝐴 ∈ Cℋ )
chscl.2 ⊢ ( 𝜑 → 𝐵 ∈ Cℋ )
chscl.3 ⊢ ( 𝜑 → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) )
chscl.4 ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) )
chscl.5 ⊢ ( 𝜑 → 𝐻 ⇝𝑣 𝑢 )
chscl.6 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) )
Assertion chscllem2 ( 𝜑 → 𝐹 ∈ dom ⇝𝑣 )

Proof

Step Hyp Ref Expression
1 chscl.1 ⊢ ( 𝜑 → 𝐴 ∈ Cℋ )
2 chscl.2 ⊢ ( 𝜑 → 𝐵 ∈ Cℋ )
3 chscl.3 ⊢ ( 𝜑 → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) )
4 chscl.4 ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) )
5 chscl.5 ⊢ ( 𝜑 → 𝐻 ⇝𝑣 𝑢 )
6 chscl.6 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) )
7 1 2 3 4 5 6 chscllem1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝐴 )
8 chss ⊢ ( 𝐴 ∈ Cℋ → 𝐴 ⊆ ℋ )
9 1 8 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℋ )
10 7 9 fssd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℋ )
11 hlimcaui ⊢ ( 𝐻 ⇝𝑣 𝑢 → 𝐻 ∈ Cauchy )
12 5 11 syl ⊢ ( 𝜑 → 𝐻 ∈ Cauchy )
13 hcaucvg ⊢ ( ( 𝐻 ∈ Cauchy ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) < 𝑥 )
14 12 13 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) < 𝑥 )
15 eluznn ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ ℕ )
16 15 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ ℕ )
17 chsh ⊢ ( 𝐴 ∈ Cℋ → 𝐴 ∈ Sℋ )
18 1 17 syl ⊢ ( 𝜑 → 𝐴 ∈ Sℋ )
19 chsh ⊢ ( 𝐵 ∈ Cℋ → 𝐵 ∈ Sℋ )
20 2 19 syl ⊢ ( 𝜑 → 𝐵 ∈ Sℋ )
21 shscl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ )
22 18 20 21 syl2anc ⊢ ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ )
23 shss ⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ → ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ )
24 22 23 syl ⊢ ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ )
26 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐻 ‘ 𝑗 ) ∈ ( 𝐴 +ℋ 𝐵 ) )
27 25 26 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐻 ‘ 𝑗 ) ∈ ℋ )
28 27 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( 𝐻 ‘ 𝑗 ) ∈ ℋ )
29 4 24 fssd ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ℋ )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → 𝐻 : ℕ ⟶ ℋ )
31 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → 𝑘 ∈ ℕ )
32 30 31 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( 𝐻 ‘ 𝑘 ) ∈ ℋ )
33 hvsubcl ⊢ ( ( ( 𝐻 ‘ 𝑗 ) ∈ ℋ ∧ ( 𝐻 ‘ 𝑘 ) ∈ ℋ ) → ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ∈ ℋ )
34 28 32 33 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ∈ ℋ )
35 9 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐴 ⊆ ℋ )
36 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝐴 )
37 35 36 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℋ )
38 37 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℋ )
39 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → 𝐴 ⊆ ℋ )
40 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → 𝐹 : ℕ ⟶ 𝐴 )
41 40 31 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐴 )
42 39 41 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℋ )
43 hvsubcl ⊢ ( ( ( 𝐹 ‘ 𝑗 ) ∈ ℋ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℋ ) → ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ℋ )
44 38 42 43 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ℋ )
45 hvsubcl ⊢ ( ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ∈ ℋ ∧ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ℋ ) → ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℋ )
46 34 44 45 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℋ )
47 normcl ⊢ ( ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℋ → ( normℎ ‘ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ )
48 46 47 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( normℎ ‘ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ∈ ℝ )
49 48 sqge0d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → 0 ≤ ( ( normℎ ‘ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ↑ 2 ) )
50 normcl ⊢ ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ℋ → ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
51 44 50 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
52 51 resqcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ↑ 2 ) ∈ ℝ )
53 48 resqcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( normℎ ‘ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ↑ 2 ) ∈ ℝ )
54 52 53 addge01d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( 0 ≤ ( ( normℎ ‘ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ↑ 2 ) ↔ ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ↑ 2 ) ≤ ( ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ↑ 2 ) ) ) )
55 49 54 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ↑ 2 ) ≤ ( ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ↑ 2 ) ) )
56 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → 𝐴 ∈ Sℋ )
57 36 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝐴 )
58 shsubcl ⊢ ( ( 𝐴 ∈ Sℋ ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝐴 )
59 56 57 41 58 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝐴 )
60 hvsubsub4 ⊢ ( ( ( ( 𝐻 ‘ 𝑗 ) ∈ ℋ ∧ ( 𝐻 ‘ 𝑘 ) ∈ ℋ ) ∧ ( ( 𝐹 ‘ 𝑗 ) ∈ ℋ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℋ ) ) → ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) −ℎ ( ( 𝐻 ‘ 𝑘 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) )
61 28 32 38 42 60 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) −ℎ ( ( 𝐻 ‘ 𝑘 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) )
62 ocsh ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )
63 39 62 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )
64 2fveq3 ⊢ ( 𝑛 = 𝑗 → ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) = ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑗 ) ) )
65 fvex ⊢ ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑗 ) ) ∈ V
66 64 6 65 fvmpt ⊢ ( 𝑗 ∈ ℕ → ( 𝐹 ‘ 𝑗 ) = ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑗 ) ) )
67 66 eqcomd ⊢ ( 𝑗 ∈ ℕ → ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑗 ) ) = ( 𝐹 ‘ 𝑗 ) )
68 67 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑗 ) ) = ( 𝐹 ‘ 𝑗 ) )
69 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐴 ∈ Cℋ )
70 9 62 syl ⊢ ( 𝜑 → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )
71 shless ⊢ ( ( ( 𝐵 ∈ Sℋ ∧ ( ⊥ ‘ 𝐴 ) ∈ Sℋ ∧ 𝐴 ∈ Sℋ ) ∧ 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( 𝐵 +ℋ 𝐴 ) ⊆ ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
72 20 70 18 3 71 syl31anc ⊢ ( 𝜑 → ( 𝐵 +ℋ 𝐴 ) ⊆ ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
73 shscom ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐴 ) )
74 18 20 73 syl2anc ⊢ ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐴 ) )
75 shscom ⊢ ( ( 𝐴 ∈ Sℋ ∧ ( ⊥ ‘ 𝐴 ) ∈ Sℋ ) → ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
76 18 70 75 syl2anc ⊢ ( 𝜑 → ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
77 72 74 76 3sstr4d ⊢ ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) )
79 78 26 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐻 ‘ 𝑗 ) ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) )
80 pjpreeq ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐻 ‘ 𝑗 ) ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) ) → ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑗 ) ) = ( 𝐹 ‘ 𝑗 ) ↔ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝐴 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) +ℎ 𝑥 ) ) ) )
81 69 79 80 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑗 ) ) = ( 𝐹 ‘ 𝑗 ) ↔ ( ( 𝐹 ‘ 𝑗 ) ∈ 𝐴 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) +ℎ 𝑥 ) ) ) )
82 68 81 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑗 ) ∈ 𝐴 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) +ℎ 𝑥 ) ) )
83 82 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) +ℎ 𝑥 ) )
84 27 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ) → ( 𝐻 ‘ 𝑗 ) ∈ ℋ )
85 37 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℋ )
86 shss ⊢ ( ( ⊥ ‘ 𝐴 ) ∈ Sℋ → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
87 70 86 syl ⊢ ( 𝜑 → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
88 87 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
89 88 sselda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ) → 𝑥 ∈ ℋ )
90 hvsubadd ⊢ ( ( ( 𝐻 ‘ 𝑗 ) ∈ ℋ ∧ ( 𝐹 ‘ 𝑗 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) = 𝑥 ↔ ( ( 𝐹 ‘ 𝑗 ) +ℎ 𝑥 ) = ( 𝐻 ‘ 𝑗 ) ) )
91 84 85 89 90 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ) → ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) = 𝑥 ↔ ( ( 𝐹 ‘ 𝑗 ) +ℎ 𝑥 ) = ( 𝐻 ‘ 𝑗 ) ) )
92 eqcom ⊢ ( 𝑥 = ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) ↔ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) = 𝑥 )
93 eqcom ⊢ ( ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) +ℎ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑗 ) +ℎ 𝑥 ) = ( 𝐻 ‘ 𝑗 ) )
94 91 92 93 3bitr4g ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ) → ( 𝑥 = ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) +ℎ 𝑥 ) ) )
95 94 rexbidva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) 𝑥 = ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) +ℎ 𝑥 ) ) )
96 83 95 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) 𝑥 = ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) )
97 risset ⊢ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) ∈ ( ⊥ ‘ 𝐴 ) ↔ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) 𝑥 = ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) )
98 96 97 sylibr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) ∈ ( ⊥ ‘ 𝐴 ) )
99 98 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) ∈ ( ⊥ ‘ 𝐴 ) )
100 eleq1w ⊢ ( 𝑗 = 𝑘 → ( 𝑗 ∈ ℕ ↔ 𝑘 ∈ ℕ ) )
101 100 anbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ↔ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) )
102 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐻 ‘ 𝑗 ) = ( 𝐻 ‘ 𝑘 ) )
103 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑘 ) )
104 102 103 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝐻 ‘ 𝑘 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) )
105 104 eleq1d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) ∈ ( ⊥ ‘ 𝐴 ) ↔ ( ( 𝐻 ‘ 𝑘 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ⊥ ‘ 𝐴 ) ) )
106 101 105 imbi12d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) ∈ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑘 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ⊥ ‘ 𝐴 ) ) ) )
107 106 98 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑘 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ⊥ ‘ 𝐴 ) )
108 107 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝐻 ‘ 𝑘 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ⊥ ‘ 𝐴 ) )
109 shsubcl ⊢ ( ( ( ⊥ ‘ 𝐴 ) ∈ Sℋ ∧ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) ∈ ( ⊥ ‘ 𝐴 ) ∧ ( ( 𝐻 ‘ 𝑘 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ⊥ ‘ 𝐴 ) ) → ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) −ℎ ( ( 𝐻 ‘ 𝑘 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( ⊥ ‘ 𝐴 ) )
110 63 99 108 109 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑗 ) ) −ℎ ( ( 𝐻 ‘ 𝑘 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( ⊥ ‘ 𝐴 ) )
111 61 110 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( ⊥ ‘ 𝐴 ) )
112 shocorth ⊢ ( 𝐴 ∈ Sℋ → ( ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝐴 ∧ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( ⊥ ‘ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ·ih ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) = 0 ) )
113 56 112 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝐴 ∧ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( ⊥ ‘ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ·ih ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) = 0 ) )
114 59 111 113 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ·ih ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) = 0 )
115 normpyth ⊢ ( ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ℋ ∧ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℋ ) → ( ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ·ih ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) = 0 → ( ( normℎ ‘ ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) +ℎ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ↑ 2 ) ) ) )
116 44 46 115 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ·ih ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) = 0 → ( ( normℎ ‘ ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) +ℎ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ↑ 2 ) ) ) )
117 114 116 mpd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( normℎ ‘ ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) +ℎ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ↑ 2 ) ) )
118 hvpncan3 ⊢ ( ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ℋ ∧ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ∈ ℋ ) → ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) +ℎ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) )
119 44 34 118 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) +ℎ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) )
120 119 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( normℎ ‘ ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) +ℎ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ) = ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) )
121 120 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( normℎ ‘ ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) +ℎ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ↑ 2 ) = ( ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) ↑ 2 ) )
122 117 121 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) −ℎ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ) ↑ 2 ) ) = ( ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) ↑ 2 ) )
123 55 122 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ↑ 2 ) ≤ ( ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) ↑ 2 ) )
124 normcl ⊢ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ∈ ℋ → ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) ∈ ℝ )
125 34 124 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) ∈ ℝ )
126 normge0 ⊢ ( ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) )
127 44 126 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → 0 ≤ ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) )
128 normge0 ⊢ ( ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) )
129 34 128 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → 0 ≤ ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) )
130 51 125 127 129 le2sqd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) ↔ ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ↑ 2 ) ≤ ( ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) ↑ 2 ) ) )
131 123 130 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) )
132 131 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) )
133 51 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
134 125 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) ∈ ℝ )
135 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
136 135 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → 𝑥 ∈ ℝ )
137 lelttr ⊢ ( ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ ∧ ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) ∧ ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) < 𝑥 ) → ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ) )
138 133 134 136 137 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) ∧ ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) < 𝑥 ) → ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ) )
139 132 138 mpand ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) < 𝑥 → ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ) )
140 139 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) < 𝑥 → ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ) )
141 16 140 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) < 𝑥 → ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ) )
142 141 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ) )
143 142 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( normℎ ‘ ( ( 𝐻 ‘ 𝑗 ) −ℎ ( 𝐻 ‘ 𝑘 ) ) ) < 𝑥 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ) )
144 14 143 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 )
145 144 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 )
146 hcau ⊢ ( 𝐹 ∈ Cauchy ↔ ( 𝐹 : ℕ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑗 ) −ℎ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑥 ) )
147 10 145 146 sylanbrc ⊢ ( 𝜑 → 𝐹 ∈ Cauchy )
148 ax-hcompl ⊢ ( 𝐹 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 )
149 hlimf ⊢ ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ
150 ffn ⊢ ( ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ → ⇝𝑣 Fn dom ⇝𝑣 )
151 149 150 ax-mp ⊢ ⇝𝑣 Fn dom ⇝𝑣
152 fnbr ⊢ ( ( ⇝𝑣 Fn dom ⇝𝑣 ∧ 𝐹 ⇝𝑣 𝑥 ) → 𝐹 ∈ dom ⇝𝑣 )
153 151 152 mpan ⊢ ( 𝐹 ⇝𝑣 𝑥 → 𝐹 ∈ dom ⇝𝑣 )
154 153 rexlimivw ⊢ ( ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 → 𝐹 ∈ dom ⇝𝑣 )
155 147 148 154 3syl ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝𝑣 )