Theorem nvcni2 8330

Description: Epsilon-delta property of a continuous operator. (Normed complex vector space version of metcni 7894.)

Hypotheses

Ref	Expression
nvcni.1	|- X = (Base` U)
nvcni.m	|- M = (norm` U)
nvcni.n	|- N = (norm` W)
nvcni.r	|- R = (-v` U)
nvcni.s	|- S = (-v` W)
nvcni.8	|- C = (IndMet` U)
nvcni.d	|- D = (IndMet` W)
nvcni.j	|- J = (Open` C)
nvcni.k	|- K = (Open` D)

Assertion

Ref	Expression
nvcni2	|- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ (P e. X /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. X ((M` (PRy)) <_ x -> (N` ((F` P)S(F` y))) <_ A)))

Distinct variable groups:   x,y,A   x,C,y   x,D,y   x,F,y   x,J,y   x,K,y   x,P,y   x,U,y   x,W,y   x,X,y

Proof of Theorem nvcni2

Step	Hyp	Ref	Expression
1		eqid 1475	. . . . . . 7 |- dom dom C = dom dom C
2		nvcni.j	. . . . . . 7 |- J = (Open` C)
3		eqid 1475	. . . . . . 7 |- dom dom D = dom dom D
4		nvcni.k	. . . . . . 7 |- K = (Open` D)
5	1, 2, 3, 4	metcni2 7895	. . . . . 6 |- (((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ (P e. dom dom C /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((F` P)D(F` y)) <_ A)))
6	5	ex 373	. . . . 5 |- ((C e. Met /\ D e. Met /\ F e. (J Cn K)) -> ((P e. dom dom C /\ A e. RR /\ 0 < A) -> E.x e. RR (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((F` P)D(F` y)) <_ A))))
7		nvcni.8	. . . . . 6 |- C = (IndMet` U)
8	7	imsmet 8324	. . . . 5 |- (U e. NrmCVec -> C e. Met)
9		nvcni.d	. . . . . 6 |- D = (IndMet` W)
10	9	imsmet 8324	. . . . 5 |- (W e. NrmCVec -> D e. Met)
11		id 59	. . . . 5 |- (F e. (J Cn K) -> F e. (J Cn K))
12	6, 8, 10, 11	syl3an 868	. . . 4 |- ((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) -> ((P e. dom dom C /\ A e. RR /\ 0 < A) -> E.x e. RR (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((F` P)D(F` y)) <_ A))))
13		nvcni.1	. . . . . . . . 9 |- X = (Base` U)
14	13, 7	imsba 8321	. . . . . . . 8 |- (U e. NrmCVec -> X = dom dom C)
15	14	eleq2d 1541	. . . . . . 7 |- (U e. NrmCVec -> (P e. X <-> P e. dom dom C))
16	15	3anbi1d 897	. . . . . 6 |- (U e. NrmCVec -> ((P e. X /\ A e. RR /\ 0 < A) <-> (P e. dom dom C /\ A e. RR /\ 0 < A)))
17	14	raleq1d 1789	. . . . . . . 8 |- (U e. NrmCVec -> (A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A) <-> A.y e. dom dom C((PCy) <_ x -> ((F` P)D(F` y)) <_ A)))
18	17	anbi2d 616	. . . . . . 7 |- (U e. NrmCVec -> ((0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A)) <-> (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((F` P)D(F` y)) <_ A))))
19	18	rexbidv 1664	. . . . . 6 |- (U e. NrmCVec -> (E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A)) <-> E.x e. RR (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((F` P)D(F` y)) <_ A))))
20	16, 19	imbi12d 626	. . . . 5 |- (U e. NrmCVec -> (((P e. X /\ A e. RR /\ 0 < A) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A))) <-> ((P e. dom dom C /\ A e. RR /\ 0 < A) -> E.x e. RR (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((F` P)D(F` y)) <_ A)))))
21	20	3ad2ant1 800	. . . 4 |- ((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) -> (((P e. X /\ A e. RR /\ 0 < A) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A))) <-> ((P e. dom dom C /\ A e. RR /\ 0 < A) -> E.x e. RR (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((F` P)D(F` y)) <_ A)))))
22	12, 21	mpbird 196	. . 3 |- ((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) -> ((P e. X /\ A e. RR /\ 0 < A) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A))))
23	22	imp 350	. 2 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ (P e. X /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A)))
24		nvcni.r	. . . . . . . . . . . . . . 15 |- R = (-v` U)
25		nvcni.m	. . . . . . . . . . . . . . 15 |- M = (norm` U)
26	13, 24, 25, 7	imsdval 8317	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ P e. X /\ y e. X) -> (PCy) = (M` (PRy)))
27	26	3expb 834	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (P e. X /\ y e. X)) -> (PCy) = (M` (PRy)))
28	27	breq1d 2629	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ (P e. X /\ y e. X)) -> ((PCy) <_ x <-> (M` (PRy)) <_ x))
29	28	3ad2antl1 809	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F:X-->(Base` W)) /\ (P e. X /\ y e. X)) -> ((PCy) <_ x <-> (M` (PRy)) <_ x))
30		eqid 1475	. . . . . . . . . . . . . 14 |- (Base` W) = (Base` W)
31		nvcni.s	. . . . . . . . . . . . . 14 |- S = (-v` W)
32		nvcni.n	. . . . . . . . . . . . . 14 |- N = (norm` W)
33	30, 31, 32, 9	imsdval 8317	. . . . . . . . . . . . 13 |- ((W e. NrmCVec /\ (F` P) e. (Base` W) /\ (F` y) e. (Base` W)) -> ((F` P)D(F` y)) = (N` ((F` P)S(F` y))))
34		3simp2 789	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ W e. NrmCVec /\ F:X-->(Base` W)) -> W e. NrmCVec)
35	34	adantr 389	. . . . . . . . . . . . 13 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F:X-->(Base` W)) /\ (P e. X /\ y e. X)) -> W e. NrmCVec)
36		ffvelrn 3814	. . . . . . . . . . . . . . 15 |- ((F:X-->(Base` W) /\ P e. X) -> (F` P) e. (Base` W))
37	36	ad2ant2lr 410	. . . . . . . . . . . . . 14 |- (((W e. NrmCVec /\ F:X-->(Base` W)) /\ (P e. X /\ y e. X)) -> (F` P) e. (Base` W))
38	37	3adantl1 803	. . . . . . . . . . . . 13 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F:X-->(Base` W)) /\ (P e. X /\ y e. X)) -> (F` P) e. (Base` W))
39		ffvelrn 3814	. . . . . . . . . . . . . . 15 |- ((F:X-->(Base` W) /\ y e. X) -> (F` y) e. (Base` W))
40	39	ad2ant2l 408	. . . . . . . . . . . . . 14 |- (((W e. NrmCVec /\ F:X-->(Base` W)) /\ (P e. X /\ y e. X)) -> (F` y) e. (Base` W))
41	40	3adantl1 803	. . . . . . . . . . . . 13 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F:X-->(Base` W)) /\ (P e. X /\ y e. X)) -> (F` y) e. (Base` W))
42	33, 35, 38, 41	syl3anc 858	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F:X-->(Base` W)) /\ (P e. X /\ y e. X)) -> ((F` P)D(F` y)) = (N` ((F` P)S(F` y))))
43	42	breq1d 2629	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F:X-->(Base` W)) /\ (P e. X /\ y e. X)) -> (((F` P)D(F` y)) <_ A <-> (N` ((F` P)S(F` y))) <_ A))
44	29, 43	imbi12d 626	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F:X-->(Base` W)) /\ (P e. X /\ y e. X)) -> (((PCy) <_ x -> ((F` P)D(F` y)) <_ A) <-> ((M` (PRy)) <_ x -> (N` ((F` P)S(F` y))) <_ A)))
45	44	anassrs 441	. . . . . . . . 9 |- ((((U e. NrmCVec /\ W e. NrmCVec /\ F:X-->(Base` W)) /\ P e. X) /\ y e. X) -> (((PCy) <_ x -> ((F` P)D(F` y)) <_ A) <-> ((M` (PRy)) <_ x -> (N` ((F` P)S(F` y))) <_ A)))
46	45	ralbidva 1659	. . . . . . . 8 |- (((U