Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem occllem6 5185

Description: Lemma for closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107.

**Hypotheses**
Ref	Expression
occllem6.1	⊢ G = {⟨x, y⟩∣(x ∈ ℕ ∧ y = ((F ‘x) ·_i S))}
occllem6.2	⊢ A ∈ ℋ
occllem6.3	⊢ S ∈ ℋ
occllem6.4	⊢ F ∈ V

**Assertion**
Ref	Expression
occllem6	⊢ (¬ S = 0_v → (F ⇝_v A → G ⇝ (A ·_i S)))

Distinct variable group(s): x,y,F x,S,y

**Proof of Theorem occllem6**
Step	Hyp	Ref	Expression
1		occllem6.1	. . . . . . . 8 ⊢ G = {⟨x, y⟩∣(x ∈ ℕ ∧ y = ((F ‘x) ·_i S))}
2		occllem6.3	. . . . . . . 8 ⊢ S ∈ ℋ
3	1, 2	occllem4 5183	. . . . . . 7 ⊢ (F:ℕ–→ ℋ → G:ℕ–→ℂ)
4		occllem6.2	. . . . . . . 8 ⊢ A ∈ ℋ
5	4, 2	hicl 5044	. . . . . . 7 ⊢ (A ·_i S) ∈ ℂ
6	3, 5	jctir 241	. . . . . 6 ⊢ (F:ℕ–→ ℋ → (G:ℕ–→ℂ ∧ (A ·_i S) ∈ ℂ))
7	6	adantr 306	. . . . 5 ⊢ ((F:ℕ–→ ℋ ∧ A ∈ ℋ ) → (G:ℕ–→ℂ ∧ (A ·_i S) ∈ ℂ))
8	7	a1i 7	. . . 4 ⊢ (¬ S = 0_v → ((F:ℕ–→ ℋ ∧ A ∈ ℋ ) → (G:ℕ–→ℂ ∧ (A ·_i S) ∈ ℂ)))
9	8	adantrd 308	. . 3 ⊢ (¬ S = 0_v → (((F:ℕ–→ ℋ ∧ A ∈ ℋ ) ∧ ∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z))) → (G:ℕ–→ℂ ∧ (A ·_i S) ∈ ℂ)))
10	2	normcl 5081	. . . . . . . . . . . . . . . . . 18 ⊢ (norm ‘S) ∈ ℝ
11		redivclt 4276	. . . . . . . . . . . . . . . . . . 19 ⊢ (((u ∈ ℝ ∧ (norm ‘S) ∈ ℝ) ∧ (norm ‘S) ≠ 0) → (u / (norm ‘S)) ∈ ℝ)
12	11	exp 291	. . . . . . . . . . . . . . . . . 18 ⊢ ((u ∈ ℝ ∧ (norm ‘S) ∈ ℝ) → ((norm ‘S) ≠ 0 → (u / (norm ‘S)) ∈ ℝ))
13	10, 12	mpan2 519	. . . . . . . . . . . . . . . . 17 ⊢ (u ∈ ℝ → ((norm ‘S) ≠ 0 → (u / (norm ‘S)) ∈ ℝ))
14	10	gt0ne0 4340	. . . . . . . . . . . . . . . . 17 ⊢ (0 < (norm ‘S) → (norm ‘S) ≠ 0)
15	13, 14	syl5 22	. . . . . . . . . . . . . . . 16 ⊢ (u ∈ ℝ → (0 < (norm ‘S) → (u / (norm ‘S)) ∈ ℝ))
16	15	adantr 306	. . . . . . . . . . . . . . 15 ⊢ ((u ∈ ℝ ∧ 0 < u) → (0 < (norm ‘S) → (u / (norm ‘S)) ∈ ℝ))
17		divgt0t 4402	. . . . . . . . . . . . . . . . . 18 ⊢ ((u ∈ ℝ ∧ (norm ‘S) ∈ ℝ) → ((0 < u ∧ 0 < (norm ‘S)) → 0 < (u / (norm ‘S))))
18	10, 17	mpan2 519	. . . . . . . . . . . . . . . . 17 ⊢ (u ∈ ℝ → ((0 < u ∧ 0 < (norm ‘S)) → 0 < (u / (norm ‘S))))
19	18	exp3a 292	. . . . . . . . . . . . . . . 16 ⊢ (u ∈ ℝ → (0 < u → (0 < (norm ‘S) → 0 < (u / (norm ‘S)))))
20	19	imp 277	. . . . . . . . . . . . . . 15 ⊢ ((u ∈ ℝ ∧ 0 < u) → (0 < (norm ‘S) → 0 < (u / (norm ‘S))))
21	16, 20	jcad 455	. . . . . . . . . . . . . 14 ⊢ ((u ∈ ℝ ∧ 0 < u) → (0 < (norm ‘S) → ((u / (norm ‘S)) ∈ ℝ ∧ 0 < (u / (norm ‘S)))))
22	21	com12 13	. . . . . . . . . . . . 13 ⊢ (0 < (norm ‘S) → ((u ∈ ℝ ∧ 0 < u) → ((u / (norm ‘S)) ∈ ℝ ∧ 0 < (u / (norm ‘S)))))
23	22	adantr 306	. . . . . . . . . . . 12 ⊢ ((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) → ((u ∈ ℝ ∧ 0 < u) → ((u / (norm ‘S)) ∈ ℝ ∧ 0 < (u / (norm ‘S)))))
24	23	syl4d 28	. . . . . . . . . . 11 ⊢ ((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) → ((((u / (norm ‘S)) ∈ ℝ ∧ 0 < (u / (norm ‘S))) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))) → ((u ∈ ℝ ∧ 0 < u) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S))))))
25		ltmuldivt 4406	. . . . . . . . . . . . . . . . . . 19 ⊢ (((norm ‘((F ‘v) −_v A)) ∈ ℝ ∧ (norm ‘S) ∈ ℝ ∧ u ∈ ℝ) → (0 < (norm ‘S) → (((norm ‘((F ‘v) −_v A)) · (norm ‘S)) < u ↔ (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))))
26	10, 25	mp3an2 640	. . . . . . . . . . . . . . . . . 18 ⊢ (((norm ‘((F ‘v) −_v A)) ∈ ℝ ∧ u ∈ ℝ) → (0 < (norm ‘S) → (((norm ‘((F ‘v) −_v A)) · (norm ‘S)) < u ↔ (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))))
27		ffvrn 2890	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → (F ‘v) ∈ ℋ )
28	27, 4	jctir 241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → ((F ‘v) ∈ ℋ ∧ A ∈ ℋ ))
29		hvsubclt 4998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((F ‘v) ∈ ℋ ∧ A ∈ ℋ ) → ((F ‘v) −_v A) ∈ ℋ )
30		normclt 5076	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((F ‘v) −_v A) ∈ ℋ → (norm ‘((F ‘v) −_v A)) ∈ ℝ)
31	28, 29, 30	3syl 21	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → (norm ‘((F ‘v) −_v A)) ∈ ℝ)
32	31	adantll 309	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ v ∈ ℕ) → (norm ‘((F ‘v) −_v A)) ∈ ℝ)
33	32	adantlr 310	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ (u ∈ ℝ ∧ 0 < u)) ∧ v ∈ ℕ) → (norm ‘((F ‘v) −_v A)) ∈ ℝ)
34		pm3.26 256	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((u ∈ ℝ ∧ 0 < u) → u ∈ ℝ)
35	34	ad2antlr 321	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ (u ∈ ℝ ∧ 0 < u)) ∧ v ∈ ℕ) → u ∈ ℝ)
36	33, 35	jca 236	. . . . . . . . . . . . . . . . . 18 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ (u ∈ ℝ ∧ 0 < u)) ∧ v ∈ ℕ) → ((norm ‘((F ‘v) −_v A)) ∈ ℝ ∧ u ∈ ℝ))
37		pm3.26 256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) → 0 < (norm ‘S))
38	37	ad2antll 320	. . . . . . . . . . . . . . . . . 18 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ (u ∈ ℝ ∧ 0 < u)) ∧ v ∈ ℕ) → 0 < (norm ‘S))
39	26, 36, 38	sylc 62	. . . . . . . . . . . . . . . . 17 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ (u ∈ ℝ ∧ 0 < u)) ∧ v ∈ ℕ) → (((norm ‘((F ‘v) −_v A)) · (norm ‘S)) < u ↔ (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S))))
40	27, 4	jctil 240	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → (A ∈ ℋ ∧ (F ‘v) ∈ ℋ ))
41	2	occllem2 5181	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((A ∈ ℋ ∧ (F ‘v) ∈ ℋ ) → (abs ‘(((F ‘v) ·_i S) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)))
42	40, 41	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → (abs ‘(((F ‘v) ·_i S) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)))
43	1	occllem3 5182	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (v ∈ ℕ → (G ‘v) = ((F ‘v) ·_i S))
44	43	opreq1d 3012	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (v ∈ ℕ → ((G ‘v) − (A ·_i S)) = (((F ‘v) ·_i S) − (A ·_i S)))
45	44	fveq2d 2836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (v ∈ ℕ → (abs ‘((G ‘v) − (A ·_i S))) = (abs ‘(((F ‘v) ·_i S) − (A ·_i S))))
46	45	breq1d 2071	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (v ∈ ℕ → ((abs ‘((G ‘v) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) ↔ (abs ‘(((F ‘v) ·_i S) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S))))
47	46	adantl 305	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → ((abs ‘((G ‘v) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) ↔ (abs ‘(((F ‘v) ·_i S) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S))))
48	42, 47	mpbird 171	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → (abs ‘((G ‘v) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)))
49	48	adantll 309	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ v ∈ ℕ) → (abs ‘((G ‘v) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)))
50	49	adantr 306	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ v ∈ ℕ) ∧ u ∈ ℝ) → (abs ‘((G ‘v) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)))
51		lelttrt 4289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((abs ‘((G ‘v) − (A ·_i S))) ∈ ℝ ∧ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) ∈ ℝ ∧ u ∈ ℝ) → (((abs ‘((G ‘v) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) ∧ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) < u) → (abs ‘((G ‘v) − (A ·_i S))) < u))
52	51	3expa 612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((abs ‘((G ‘v) − (A ·_i S))) ∈ ℝ ∧ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) ∈ ℝ) ∧ u ∈ ℝ) → (((abs ‘((G ‘v) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) ∧ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) < u) → (abs ‘((G ‘v) − (A ·_i S))) < u))
53		ffvrn 2890	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((G:ℕ–→ℂ ∧ v ∈ ℕ) → (G ‘v) ∈ ℂ)
54	53, 3	sylan 343	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → (G ‘v) ∈ ℂ)
55	54, 5	jctir 241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → ((G ‘v) ∈ ℂ ∧ (A ·_i S) ∈ ℂ))
56		subclt 4140	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((G ‘v) ∈ ℂ ∧ (A ·_i S) ∈ ℂ) → ((G ‘v) − (A ·_i S)) ∈ ℂ)
57		absclt 4848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((G ‘v) − (A ·_i S)) ∈ ℂ → (abs ‘((G ‘v) − (A ·_i S))) ∈ ℝ)
58	55, 56, 57	3syl 21	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → (abs ‘((G ‘v) − (A ·_i S))) ∈ ℝ)
59	31, 10	jctir 241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → ((norm ‘((F ‘v) −_v A)) ∈ ℝ ∧ (norm ‘S) ∈ ℝ))
60		axmulrcl 4069	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((norm ‘((F ‘v) −_v A)) ∈ ℝ ∧ (norm ‘S) ∈ ℝ) → ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) ∈ ℝ)
61	59, 60	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) ∈ ℝ)
62	58, 61	jca 236	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((F:ℕ–→ ℋ ∧ v ∈ ℕ) → ((abs ‘((G ‘v) − (A ·_i S))) ∈ ℝ ∧ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) ∈ ℝ))
63	62	adantll 309	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ v ∈ ℕ) → ((abs ‘((G ‘v) − (A ·_i S))) ∈ ℝ ∧ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) ∈ ℝ))
64	52, 63	sylan 343	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ v ∈ ℕ) ∧ u ∈ ℝ) → (((abs ‘((G ‘v) − (A ·_i S))) ≤ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) ∧ ((norm ‘((F ‘v) −_v A)) · (norm ‘S)) < u) → (abs ‘((G ‘v) − (A ·_i S))) < u))
65	50, 64	mpand 524	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ v ∈ ℕ) ∧ u ∈ ℝ) → (((norm ‘((F ‘v) −_v A)) · (norm ‘S)) < u → (abs ‘((G ‘v) − (A ·_i S))) < u))
66	65	adantrr 312	. . . . . . . . . . . . . . . . . 18 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ v ∈ ℕ) ∧ (u ∈ ℝ ∧ 0 < u)) → (((norm ‘((F ‘v) −_v A)) · (norm ‘S)) < u → (abs ‘((G ‘v) − (A ·_i S))) < u))
67	66	an1rs 373	. . . . . . . . . . . . . . . . 17 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ (u ∈ ℝ ∧ 0 < u)) ∧ v ∈ ℕ) → (((norm ‘((F ‘v) −_v A)) · (norm ‘S)) < u → (abs ‘((G ‘v) − (A ·_i S))) < u))
68	39, 67	sylbird 180	. . . . . . . . . . . . . . . 16 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ (u ∈ ℝ ∧ 0 < u)) ∧ v ∈ ℕ) → ((norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)) → (abs ‘((G ‘v) − (A ·_i S))) < u))
69	68	syl3d 26	. . . . . . . . . . . . . . 15 ⊢ ((((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ (u ∈ ℝ ∧ 0 < u)) ∧ v ∈ ℕ) → ((w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S))) → (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u)))
70	69	r19.20dva 1256	. . . . . . . . . . . . . 14 ⊢ (((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ (u ∈ ℝ ∧ 0 < u)) → (∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S))) → ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u)))
71	70	r19.22sdv 1279	. . . . . . . . . . . . 13 ⊢ (((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) ∧ (u ∈ ℝ ∧ 0 < u)) → (∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S))) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u)))
72	71	exp 291	. . . . . . . . . . . 12 ⊢ ((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) → ((u ∈ ℝ ∧ 0 < u) → (∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S))) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u))))
73	72	a2d 15	. . . . . . . . . . 11 ⊢ ((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) → (((u ∈ ℝ ∧ 0 < u) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))) → ((u ∈ ℝ ∧ 0 < u) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u))))
74	24, 73	syld 27	. . . . . . . . . 10 ⊢ ((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) → ((((u / (norm ‘S)) ∈ ℝ ∧ 0 < (u / (norm ‘S))) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))) → ((u ∈ ℝ ∧ 0 < u) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u))))
75	74	exp4a 295	. . . . . . . . 9 ⊢ ((0 < (norm ‘S) ∧ F:ℕ–→ ℋ ) → ((((u / (norm ‘S)) ∈ ℝ ∧ 0 < (u / (norm ‘S))) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))) → (u ∈ ℝ → (0 < u → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u)))))
76		normgt0t 5078	. . . . . . . . . 10 ⊢ (S ∈ ℋ → (¬ S = 0_v ↔ 0 < (norm ‘S)))
77	2, 76	ax-mp 6	. . . . . . . . 9 ⊢ (¬ S = 0_v ↔ 0 < (norm ‘S))
78	75, 77	sylanb 344	. . . . . . . 8 ⊢ ((¬ S = 0_v ∧ F:ℕ–→ ℋ ) → ((((u / (norm ‘S)) ∈ ℝ ∧ 0 < (u / (norm ‘S))) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))) → (u ∈ ℝ → (0 < u → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u)))))
79	78	adantrr 312	. . . . . . 7 ⊢ ((¬ S = 0_v ∧ (F:ℕ–→ ℋ ∧ A ∈ ℋ )) → ((((u / (norm ‘S)) ∈ ℝ ∧ 0 < (u / (norm ‘S))) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))) → (u ∈ ℝ → (0 < u → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u)))))
80		breq2 2066	. . . . . . . . . 10 ⊢ (z = (u / (norm ‘S)) → (0 < z ↔ 0 < (u / (norm ‘S))))
81		breq2 2066	. . . . . . . . . . . . 13 ⊢ (z = (u / (norm ‘S)) → ((norm ‘((F ‘v) −_v A)) < z ↔ (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S))))
82	81	imbi2d 464	. . . . . . . . . . . 12 ⊢ (z = (u / (norm ‘S)) → ((w ≤ v → (norm ‘((F ‘v) −_v A)) < z) ↔ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))))
83	82	biraldv 1219	. . . . . . . . . . 11 ⊢ (z = (u / (norm ‘S)) → (∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z) ↔ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))))
84	83	birexdv 1220	. . . . . . . . . 10 ⊢ (z = (u / (norm ‘S)) → (∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z) ↔ ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))))
85	80, 84	imbi12d 474	. . . . . . . . 9 ⊢ (z = (u / (norm ‘S)) → ((0 < z → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z)) ↔ (0 < (u / (norm ‘S)) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S))))))
86	85	rcla4v 1402	. . . . . . . 8 ⊢ (∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z)) → ((u / (norm ‘S)) ∈ ℝ → (0 < (u / (norm ‘S)) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S))))))
87	86	imp3a 279	. . . . . . 7 ⊢ (∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z)) → (((u / (norm ‘S)) ∈ ℝ ∧ 0 < (u / (norm ‘S))) → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < (u / (norm ‘S)))))
88	79, 87	syl5 22	. . . . . 6 ⊢ ((¬ S = 0_v ∧ (F:ℕ–→ ℋ ∧ A ∈ ℋ )) → (∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z)) → (u ∈ ℝ → (0 < u → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u)))))
89	88	r19.21adv 1262	. . . . 5 ⊢ ((¬ S = 0_v ∧ (F:ℕ–→ ℋ ∧ A ∈ ℋ )) → (∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z)) → ∀u ∈ ℝ (0 < u → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u))))
90	89	exp 291	. . . 4 ⊢ (¬ S = 0_v → ((F:ℕ–→ ℋ ∧ A ∈ ℋ ) → (∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z)) → ∀u ∈ ℝ (0 < u → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u)))))
91	90	imp3a 279	. . 3 ⊢ (¬ S = 0_v → (((F:ℕ–→ ℋ ∧ A ∈ ℋ ) ∧ ∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z))) → ∀u ∈ ℝ (0 < u → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u))))
92	9, 91	jcad 455	. 2 ⊢ (¬ S = 0_v → (((F:ℕ–→ ℋ ∧ A ∈ ℋ ) ∧ ∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z))) → ((G:ℕ–→ℂ ∧ (A ·_i S) ∈ ℂ) ∧ ∀u ∈ ℝ (0 < u → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u)))))
93		occllem6.4	. . 3 ⊢ F ∈ V
94	4	elisseti 1355	. . 3 ⊢ A ∈ V
95	93, 94	hlim 5108	. 2 ⊢ (F ⇝_v A ↔ ((F:ℕ–→ ℋ ∧ A ∈ ℋ ) ∧ ∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (norm ‘((F ‘v) −_v A)) < z))))
96		nnex 4431	. . . . 5 ⊢ ℕ ∈ V
97		moeq 1431	. . . . . 6 ⊢ ∃*y y = ((F ‘x) ·_i S)
98	97	a1i 7	. . . . 5 ⊢ (x ∈ ℕ → ∃*y y = ((F ‘x) ·_i S))
99	96, 98	funopabex 2742	. . . 4 ⊢ {⟨x, y⟩∣(x ∈ ℕ ∧ y = ((F ‘x) ·_i S))} ∈ V
100	1, 99	eqeltr 1159	. . 3 ⊢ G ∈ V
101		oprex 3018	. . 3 ⊢ (A ·_i S) ∈ V
102	100, 101	clim 4877	. 2 ⊢ (G ⇝ (A ·_i S) ↔ ((G:ℕ–→ℂ ∧ (A ·_i S) ∈ ℂ) ∧ ∀u ∈ ℝ (0 < u → ∃w ∈ ℕ ∀v ∈ ℕ (w ≤ v → (abs ‘((G ‘v) − (A ·_i S))) < u))))
103	92, 95, 102	3imtr4g 426	1 ⊢ (¬ S = 0_v → (F ⇝_v A → G ⇝ (A ·_i S)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 ∃*wmo 1008 = wceq 1091 ∈ wcel 1092 ≠ wne 1190 ∀wral 1201 ∃wrex 1202 Vcvv 1348 class class class wbr 2054 {copab 2055 –→wf 2418 ‘cfv 2422 (class class class)co 3001 ℂcc 4026 ℝcr 4027 0cc0 4028 · cmulc 4032 < clt 4033 − cmin 4089 / cdiv 4091 ≤ cle 4092 ℕcn 4093 abscabs 4789 ⇝ cli 4875 ℋ chil 4958 0_vc0v 4961 −_v cmv 4962 ·_i csp 4963 normcno 4964 ⇝_v chli 4966

This theorem is referenced by: occllem7 5186

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079 ax-hvaddcl 4984 ax-hvzercl 4987 ax-hvmulcl 4989 ax-hvmulass 4992 ax-hvmulzer 4995 ax-hicl 5043 ax-his1 5045 ax-his2 5046 ax-his3 5047 ax-his4 5048

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-sup 2154 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1st 3087 df-2nd 3088 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-i 4037 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-div 4216 df-le 4277 df-n 4423 df-2 4462 df-3 4463 df-4 4464 df-n0 4535 df-z 4564 df-seq 4661 df-exp 4676 df-sqr 4728 df-re 4790 df-im 4791 df-cj 4792 df-abs 4793 df-clim 4876 df-hvsub 4996 df-hnorm 5074 df-hlim 5107

metamath.org