Theorem sm1cnilem 8343

Description: Lemma for sm1cni 8344.

Hypotheses

Ref	Expression
sm1cni.1	⊢ X = (Base ‘U)
sm1cni.4	⊢ S = ( ·s ‘U)
sm1cni.7	⊢ C = (abs ∘ − )
sm1cni.8	⊢ D = (IndMet ‘U)
sm1cni.j	⊢ J = (Open ‘C)
sm1cni.k	⊢ K = (Open ‘D)
sm1cni.f	⊢ F = {⟨w, v⟩∣(w ∈ ℂ ⋀ v = (wSA))}
sm1cni.9	⊢ U ∈ NrmCVec
sm1cni.a	⊢ A ∈ X
sm1cni.2	⊢ G = ( +v ‘U)
sm1cnilem.6	⊢ N = (norm ‘U)

Assertion

Ref	Expression
sm1cnilem	⊢ F ∈ (J Cn K)

Distinct variable groups:   w,v,A   v,S,w   v,X,w

Proof of Theorem sm1cnilem

Step	Hyp	Ref	Expression
1		sm1cni.7	. . . 4 ⊢ C = (abs ∘ − )
2	1	cnmet 7901	. . 3 ⊢ C ∈ Met
3		sm1cni.9	. . . 4 ⊢ U ∈ NrmCVec
4		sm1cni.8	. . . . 5 ⊢ D = (IndMet ‘U)
5	4	imsmet 8320	. . . 4 ⊢ (U ∈ NrmCVec → D ∈ Met)
6	3, 5	ax-mp 7	. . 3 ⊢ D ∈ Met
7	1	cnmetba 7900	. . . 4 ⊢ ℂ = dom dom C
8		sm1cni.j	. . . 4 ⊢ J = (Open ‘C)
9		sm1cni.1	. . . . 5 ⊢ X = (Base ‘U)
10	9, 4, 3	imsbai 8318	. . . 4 ⊢ X = dom dom D
11		sm1cni.k	. . . 4 ⊢ K = (Open ‘D)
12	7, 8, 10, 11	metcn 7886	. . 3 ⊢ ((C ∈ Met ⋀ D ∈ Met) → (F ∈ (J Cn K) ↔ (F:ℂ–→X ⋀ ∀r ∈ ℂ ∀s ∈ ℝ (0 < s → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((rCu) < t → ((F ‘r)D(F ‘u)) < s))))))
13	2, 6, 12	mp2an 699	. 2 ⊢ (F ∈ (J Cn K) ↔ (F:ℂ–→X ⋀ ∀r ∈ ℂ ∀s ∈ ℝ (0 < s → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((rCu) < t → ((F ‘r)D(F ‘u)) < s)))))
14		sm1cni.f	. . 3 ⊢ F = {⟨w, v⟩∣(w ∈ ℂ ⋀ v = (wSA))}
15		sm1cni.a	. . . 4 ⊢ A ∈ X
16		sm1cni.4	. . . . 5 ⊢ S = ( ·s ‘U)
17	9, 16	nvscl 8243	. . . 4 ⊢ ((U ∈ NrmCVec ⋀ w ∈ ℂ ⋀ A ∈ X) → (wSA) ∈ X)
18	3, 15, 17	mp3an13 909	. . 3 ⊢ (w ∈ ℂ → (wSA) ∈ X)
19	14, 18	fopab 3833	. 2 ⊢ F:ℂ–→X
20		opreq2 3975	. . . . . . . . . . 11 ⊢ ((N ‘A) = 0 → ((abs ‘(r − u)) · (N ‘A)) = ((abs ‘(r − u)) · 0))
21	20	breq1d 2634	. . . . . . . . . 10 ⊢ ((N ‘A) = 0 → (((abs ‘(r − u)) · (N ‘A)) < s ↔ ((abs ‘(r − u)) · 0) < s))
22	21	imbi2d 614	. . . . . . . . 9 ⊢ ((N ‘A) = 0 → (((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s) ↔ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · 0) < s)))
23	22	ralbidv 1666	. . . . . . . 8 ⊢ ((N ‘A) = 0 → (∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s) ↔ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · 0) < s)))
24	23	anbi2d 618	. . . . . . 7 ⊢ ((N ‘A) = 0 → ((0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s)) ↔ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · 0) < s))))
25	24	rexbidv 1667	. . . . . 6 ⊢ ((N ‘A) = 0 → (∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s)) ↔ ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · 0) < s))))
26		breq2 2628	. . . . . . . . 9 ⊢ (t = (s / (N ‘A)) → (0 < t ↔ 0 < (s / (N ‘A))))
27		breq2 2628	. . . . . . . . . . 11 ⊢ (t = (s / (N ‘A)) → ((abs ‘(r − u)) < t ↔ (abs ‘(r − u)) < (s / (N ‘A))))
28	27	imbi1d 615	. . . . . . . . . 10 ⊢ (t = (s / (N ‘A)) → (((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s) ↔ ((abs ‘(r − u)) < (s / (N ‘A)) → ((abs ‘(r − u)) · (N ‘A)) < s)))
29	28	ralbidv 1666	. . . . . . . . 9 ⊢ (t = (s / (N ‘A)) → (∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s) ↔ ∀u ∈ ℂ ((abs ‘(r − u)) < (s / (N ‘A)) → ((abs ‘(r − u)) · (N ‘A)) < s)))
30	26, 29	anbi12d 630	. . . . . . . 8 ⊢ (t = (s / (N ‘A)) → ((0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s)) ↔ (0 < (s / (N ‘A)) ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < (s / (N ‘A)) → ((abs ‘(r − u)) · (N ‘A)) < s))))
31	30	rcla4ev 1880	. . . . . . 7 ⊢ (((s / (N ‘A)) ∈ ℝ ⋀ (0 < (s / (N ‘A)) ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < (s / (N ‘A)) → ((abs ‘(r − u)) · (N ‘A)) < s))) → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s)))
32		sm1cnilem.6	. . . . . . . . . . 11 ⊢ N = (norm ‘U)
33	9, 32, 3, 15	nvcli 8284	. . . . . . . . . 10 ⊢ (N ‘A) ∈ ℝ
34		redivclt 5802	. . . . . . . . . 10 ⊢ ((s ∈ ℝ ⋀ (N ‘A) ∈ ℝ ⋀ (N ‘A) ≠ 0) → (s / (N ‘A)) ∈ ℝ)
35	33, 34	mp3an2 906	. . . . . . . . 9 ⊢ ((s ∈ ℝ ⋀ (N ‘A) ≠ 0) → (s / (N ‘A)) ∈ ℝ)
36	35	adantll 394	. . . . . . . 8 ⊢ (((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ (N ‘A) ≠ 0) → (s / (N ‘A)) ∈ ℝ)
37	36	adantlr 395	. . . . . . 7 ⊢ ((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) → (s / (N ‘A)) ∈ ℝ)
38		divgt0t 5857	. . . . . . . . . . 11 ⊢ (((s ∈ ℝ ⋀ 0 < s) ⋀ ((N ‘A) ∈ ℝ ⋀ 0 < (N ‘A))) → 0 < (s / (N ‘A)))
39	33, 38	mpanr1 711	. . . . . . . . . 10 ⊢ (((s ∈ ℝ ⋀ 0 < s) ⋀ 0 < (N ‘A)) → 0 < (s / (N ‘A)))
40	9, 32	nvge0 8298	. . . . . . . . . . . 12 ⊢ ((U ∈ NrmCVec ⋀ A ∈ X) → 0 ≤ (N ‘A))
41	3, 15, 40	mp2an 699	. . . . . . . . . . 11 ⊢ 0 ≤ (N ‘A)
42		0re 5452	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
43	42, 33	ltlen 5588	. . . . . . . . . . . 12 ⊢ (0 < (N ‘A) ↔ (0 ≤ (N ‘A) ⋀ (N ‘A) ≠ 0))
44	43	biimpr 152	. . . . . . . . . . 11 ⊢ ((0 ≤ (N ‘A) ⋀ (N ‘A) ≠ 0) → 0 < (N ‘A))
45	41, 44	mpan 697	. . . . . . . . . 10 ⊢ ((N ‘A) ≠ 0 → 0 < (N ‘A))
46	39, 45	sylan2 453	. . . . . . . . 9 ⊢ (((s ∈ ℝ ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) → 0 < (s / (N ‘A)))
47	46	adantlll 398	. . . . . . . 8 ⊢ ((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) → 0 < (s / (N ‘A)))
48		ltmuldivtOLD 5866	. . . . . . . . . . 11 ⊢ ((((abs ‘(r − u)) ∈ ℝ ⋀ (N ‘A) ∈ ℝ ⋀ s ∈ ℝ) ⋀ 0 < (N ‘A)) → (((abs ‘(r − u)) · (N ‘A)) < s ↔ (abs ‘(r − u)) < (s / (N ‘A))))
49		subclt 5379	. . . . . . . . . . . . . . . 16 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → (r − u) ∈ ℂ)
50		absclt 6833	. . . . . . . . . . . . . . . 16 ⊢ ((r − u) ∈ ℂ → (abs ‘(r − u)) ∈ ℝ)
51	49, 50	syl 10	. . . . . . . . . . . . . . 15 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → (abs ‘(r − u)) ∈ ℝ)
52	51	adantlr 395	. . . . . . . . . . . . . 14 ⊢ (((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ u ∈ ℂ) → (abs ‘(r − u)) ∈ ℝ)
53	52	adantlr 395	. . . . . . . . . . . . 13 ⊢ ((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ u ∈ ℂ) → (abs ‘(r − u)) ∈ ℝ)
54	53	adantlr 395	. . . . . . . . . . . 12 ⊢ (((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) ⋀ u ∈ ℂ) → (abs ‘(r − u)) ∈ ℝ)
55	33	a1i 8	. . . . . . . . . . . 12 ⊢ (((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) ⋀ u ∈ ℂ) → (N ‘A) ∈ ℝ)
56		simplr 415	. . . . . . . . . . . . 13 ⊢ (((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) → s ∈ ℝ)
57	56	ad2antrr 406	. . . . . . . . . . . 12 ⊢ (((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) ⋀ u ∈ ℂ) → s ∈ ℝ)
58	54, 55, 57	3jca 821	. . . . . . . . . . 11 ⊢ (((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) ⋀ u ∈ ℂ) → ((abs ‘(r − u)) ∈ ℝ ⋀ (N ‘A) ∈ ℝ ⋀ s ∈ ℝ))
59	45	ad2antlr 407	. . . . . . . . . . 11 ⊢ (((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) ⋀ u ∈ ℂ) → 0 < (N ‘A))
60	48, 58, 59	sylanc 473	. . . . . . . . . 10 ⊢ (((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) ⋀ u ∈ ℂ) → (((abs ‘(r − u)) · (N ‘A)) < s ↔ (abs ‘(r − u)) < (s / (N ‘A))))
61	60	biimprd 154	. . . . . . . . 9 ⊢ (((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) ⋀ u ∈ ℂ) → ((abs ‘(r − u)) < (s / (N ‘A)) → ((abs ‘(r − u)) · (N ‘A)) < s))
62	61	r19.21aiva 1717	. . . . . . . 8 ⊢ ((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) → ∀u ∈ ℂ ((abs ‘(r − u)) < (s / (N ‘A)) → ((abs ‘(r − u)) · (N ‘A)) < s))
63	47, 62	jca 288	. . . . . . 7 ⊢ ((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) → (0 < (s / (N ‘A)) ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < (s / (N ‘A)) → ((abs ‘(r − u)) · (N ‘A)) < s)))
64	31, 37, 63	sylanc 473	. . . . . 6 ⊢ ((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ (N ‘A) ≠ 0) → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s)))
65	51	recnd 5327	. . . . . . . . . . . . 13 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → (abs ‘(r − u)) ∈ ℂ)
66		mul01t 5455	. . . . . . . . . . . . 13 ⊢ ((abs ‘(r − u)) ∈ ℂ → ((abs ‘(r − u)) · 0) = 0)
67	65, 66	syl 10	. . . . . . . . . . . 12 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → ((abs ‘(r − u)) · 0) = 0)
68	67	adantlr 395	. . . . . . . . . . 11 ⊢ (((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ u ∈ ℂ) → ((abs ‘(r − u)) · 0) = 0)
69	68	adantlr 395	. . . . . . . . . 10 ⊢ ((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ u ∈ ℂ) → ((abs ‘(r − u)) · 0) = 0)
70		simplr 415	. . . . . . . . . 10 ⊢ ((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ u ∈ ℂ) → 0 < s)
71	69, 70	eqbrtrd 2640	. . . . . . . . 9 ⊢ ((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ u ∈ ℂ) → ((abs ‘(r − u)) · 0) < s)
72	71	a1d 12	. . . . . . . 8 ⊢ ((((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) ⋀ u ∈ ℂ) → ((abs ‘(r − u)) < 1 → ((abs ‘(r − u)) · 0) < s))
73	72	r19.21aiva 1717	. . . . . . 7 ⊢ (((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) → ∀u ∈ ℂ ((abs ‘(r − u)) < 1 → ((abs ‘(r − u)) · 0) < s))
74		lt01 5692	. . . . . . . 8 ⊢ 0 < 1
75		1re 5447	. . . . . . . . 9 ⊢ 1 ∈ ℝ
76		breq2 2628	. . . . . . . . . . 11 ⊢ (t = 1 → (0 < t ↔ 0 < 1))
77		breq2 2628	. . . . . . . . . . . . 13 ⊢ (t = 1 → ((abs ‘(r − u)) < t ↔ (abs ‘(r − u)) < 1))
78	77	imbi1d 615	. . . . . . . . . . . 12 ⊢ (t = 1 → (((abs ‘(r − u)) < t → ((abs ‘(r − u)) · 0) < s) ↔ ((abs ‘(r − u)) < 1 → ((abs ‘(r − u)) · 0) < s)))
79	78	ralbidv 1666	. . . . . . . . . . 11 ⊢ (t = 1 → (∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · 0) < s) ↔ ∀u ∈ ℂ ((abs ‘(r − u)) < 1 → ((abs ‘(r − u)) · 0) < s)))
80	76, 79	anbi12d 630	. . . . . . . . . 10 ⊢ (t = 1 → ((0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · 0) < s)) ↔ (0 < 1 ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < 1 → ((abs ‘(r − u)) · 0) < s))))
81	80	rcla4ev 1880	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ⋀ (0 < 1 ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < 1 → ((abs ‘(r − u)) · 0) < s))) → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · 0) < s)))
82	75, 81	mpan 697	. . . . . . . 8 ⊢ ((0 < 1 ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < 1 → ((abs ‘(r − u)) · 0) < s)) → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · 0) < s)))
83	74, 82	mpan 697	. . . . . . 7 ⊢ (∀u ∈ ℂ ((abs ‘(r − u)) < 1 → ((abs ‘(r − u)) · 0) < s) → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · 0) < s)))
84	73, 83	syl 10	. . . . . 6 ⊢ (((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · 0) < s)))
85	25, 64, 84	pm2.61ne 1636	. . . . 5 ⊢ (((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s)))
86	1	cnmetdval 7899	. . . . . . . . . . 11 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → (rCu) = (abs ‘(r − u)))
87	86	breq1d 2634	. . . . . . . . . 10 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → ((rCu) < t ↔ (abs ‘(r − u)) < t))
88		opreq1 3974	. . . . . . . . . . . . . 14 ⊢ (w = r → (wSA) = (rSA))
89		oprex 3989	. . . . . . . . . . . . . 14 ⊢ (rSA) ∈ V
90	88, 14, 89	fvopab4 3786	. . . . . . . . . . . . 13 ⊢ (r ∈ ℂ → (F ‘r) = (rSA))
91		opreq1 3974	. . . . . . . . . . . . . 14 ⊢ (w = u → (wSA) = (uSA))
92		oprex 3989	. . . . . . . . . . . . . 14 ⊢ (uSA) ∈ V
93	91, 14, 92	fvopab4 3786	. . . . . . . . . . . . 13 ⊢ (u ∈ ℂ → (F ‘u) = (uSA))
94	90, 93	opreqan12d 3985	. . . . . . . . . . . 12 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → ((F ‘r)D(F ‘u)) = ((rSA)D(uSA)))
95		sm1cni.2	. . . . . . . . . . . . . . . 16 ⊢ G = ( +v ‘U)
96	9, 95, 16, 32, 4	imsdval2 8314	. . . . . . . . . . . . . . 15 ⊢ ((U ∈ NrmCVec ⋀ (rSA) ∈ X ⋀ (uSA) ∈ X) → ((rSA)D(uSA)) = (N ‘((rSA)G(-1S(uSA)))))
97	3, 96	mp3an1 905	. . . . . . . . . . . . . 14 ⊢ (((rSA) ∈ X ⋀ (uSA) ∈ X) → ((rSA)D(uSA)) = (N ‘((rSA)G(-1S(uSA)))))
98	9, 16	nvscl 8243	. . . . . . . . . . . . . . 15 ⊢ ((U ∈ NrmCVec ⋀ r ∈ ℂ ⋀ A ∈ X) → (rSA) ∈ X)
99	3, 15, 98	mp3an13 909	. . . . . . . . . . . . . 14 ⊢ (r ∈ ℂ → (rSA) ∈ X)
100	9, 16	nvscl 8243	. . . . . . . . . . . . . . 15 ⊢ ((U ∈ NrmCVec ⋀ u ∈ ℂ ⋀ A ∈ X) → (uSA) ∈ X)
101	3, 15, 100	mp3an13 909	. . . . . . . . . . . . . 14 ⊢ (u ∈ ℂ → (uSA) ∈ X)
102	97, 99, 101	syl2an 456	. . . . . . . . . . . . 13 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → ((rSA)D(uSA)) = (N ‘((rSA)G(-1S(uSA)))))
103		eqid 1478	. . . . . . . . . . . . . . . . . 18 ⊢ (1st ‘U) = (1st ‘U)
104	103	nvvc 8230	. . . . . . . . . . . . . . . . 17 ⊢ (U ∈ NrmCVec → (1st ‘U) ∈ CVec)
105	3, 104	ax-mp 7	. . . . . . . . . . . . . . . 16 ⊢ (1st ‘U) ∈ CVec
106	95	vafval 8218	. . . . . . . . . . . . . . . . 17 ⊢ G = (1st ‘(1st ‘U))
107	16	smfval 8220	. . . . . . . . . . . . . . . . 17 ⊢ S = (2nd ‘(1st ‘U))
108	9, 95	bafval 8219	. . . . . . . . . . . . . . . . 17 ⊢ X = ran G
109	106, 107, 108	vcsubdir 8171	. . . . . . . . . . . . . . . 16 ⊢ (((1st ‘U) ∈ CVec ⋀ (r ∈ ℂ ⋀ u ∈ ℂ ⋀ A ∈ X)) → ((r − u)SA) = ((rSA)G(-1S(uSA))))
110	105, 109	mpan 697	. . . . . . . . . . . . . . 15 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ ⋀ A ∈ X) → ((r − u)SA) = ((rSA)G(-1S(uSA))))
111	15, 110	mp3an3 907	. . . . . . . . . . . . . 14 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → ((r − u)SA) = ((rSA)G(-1S(uSA))))
112	111	fveq2d 3734	. . . . . . . . . . . . 13 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → (N ‘((r − u)SA)) = (N ‘((rSA)G(-1S(uSA)))))
113	9, 16, 32	nvs 8286	. . . . . . . . . . . . . . 15 ⊢ ((U ∈ NrmCVec ⋀ (r − u) ∈ ℂ ⋀ A ∈ X) → (N ‘((r − u)SA)) = ((abs ‘(r − u)) · (N ‘A)))
114	3, 15, 113	mp3an13 909	. . . . . . . . . . . . . 14 ⊢ ((r − u) ∈ ℂ → (N ‘((r − u)SA)) = ((abs ‘(r − u)) · (N ‘A)))
115	49, 114	syl 10	. . . . . . . . . . . . 13 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → (N ‘((r − u)SA)) = ((abs ‘(r − u)) · (N ‘A)))
116	102, 112, 115	3eqtr2d 1516	. . . . . . . . . . . 12 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → ((rSA)D(uSA)) = ((abs ‘(r − u)) · (N ‘A)))
117	94, 116	eqtrd 1510	. . . . . . . . . . 11 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → ((F ‘r)D(F ‘u)) = ((abs ‘(r − u)) · (N ‘A)))
118	117	breq1d 2634	. . . . . . . . . 10 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → (((F ‘r)D(F ‘u)) < s ↔ ((abs ‘(r − u)) · (N ‘A)) < s))
119	87, 118	imbi12d 628	. . . . . . . . 9 ⊢ ((r ∈ ℂ ⋀ u ∈ ℂ) → (((rCu) < t → ((F ‘r)D(F ‘u)) < s) ↔ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s)))
120	119	ralbidva 1662	. . . . . . . 8 ⊢ (r ∈ ℂ → (∀u ∈ ℂ ((rCu) < t → ((F ‘r)D(F ‘u)) < s) ↔ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s)))
121	120	anbi2d 618	. . . . . . 7 ⊢ (r ∈ ℂ → ((0 < t ⋀ ∀u ∈ ℂ ((rCu) < t → ((F ‘r)D(F ‘u)) < s)) ↔ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s))))
122	121	rexbidv 1667	. . . . . 6 ⊢ (r ∈ ℂ → (∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((rCu) < t → ((F ‘r)D(F ‘u)) < s)) ↔ ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s))))
123	122	ad2antrr 406	. . . . 5 ⊢ (((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) → (∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((rCu) < t → ((F ‘r)D(F ‘u)) < s)) ↔ ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((abs ‘(r − u)) < t → ((abs ‘(r − u)) · (N ‘A)) < s))))
124	85, 123	mpbird 196	. . . 4 ⊢ (((r ∈ ℂ ⋀ s ∈ ℝ) ⋀ 0 < s) → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((rCu) < t → ((F ‘r)D(F ‘u)) < s)))
125	124	ex 373	. . 3 ⊢ ((r ∈ ℂ ⋀ s ∈ ℝ) → (0 < s → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((rCu) < t → ((F ‘r)D(F ‘u)) < s))))
126	125	rgen2 1726	. 2 ⊢ ∀r ∈ ℂ ∀s ∈ ℝ (0 < s → ∃t ∈ ℝ (0 < t ⋀ ∀u ∈ ℂ ((rCu) < t → ((F ‘r)D(F ‘u)) < s)))
127	13, 19, 126	mpbir2an 732	1 ⊢ F ∈ (J Cn K)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ⋀ w3a 777   = wceq 958   ∈ wcel 960   ≠ wne 1588  ∀wral 1648  ∃wrex 1649   class class class wbr 2624  {copab 2671   ∘ ccom 3180  –→wf 3184   ‘cfv 3188  (class class class)co 3969  1^st c1st 4083  ℂcc 5244  ℝcr 5245  0cc0 5246  1c1 5247   · cmul 5251   − cmin 5304  -cneg 5305   / cdiv 5306   ≤ cle 5307   < clt 5498  abscabs 6751   Cn ccn 7749  Metcme 7786  Opencopn 7789  CVeccvc 8160  NrmCVeccnv 8199   +_v cpv 8200  Basecba 8201   ·_s cns 8202  normcnm 8205  IndMetcims 8206

This theorem is referenced by:  sm1cni 8344

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224