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 ⇝𝑣 )