chscllem2

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

	Ref	Expression
Hypotheses	chscl.1	$⊢ φ \to A \in C_{ℋ}$
	chscl.2	$⊢ φ \to B \in C_{ℋ}$
	chscl.3	$⊢ φ \to B \subseteq ⊥ (A)$
	chscl.4	$⊢ φ \to H : ℕ ⟶ A +_{ℋ} B$
	chscl.5	$⊢ φ \to H \underset{v}{⇝} u$
	chscl.6	$⊢ F = (n \in ℕ ⟼ {proj}_{ℎ} (A) (H (n)))$
Assertion	chscllem2	$⊢ φ \to F \in dom \underset{v}{⇝}$

Proof

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

Metamath Proof Explorer

Theorem chscllem2

Proof