Theorem nvcni3 8339

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

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
nvcni3	|- (((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` (yRP)) < x -> (N` ((F` y)S(F` P))) < 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 nvcni3

Step	Hyp	Ref	Expression
1		nvcni.1	. . 3 |- X = (Base` U)
2		nvcni.m	. . 3 |- M = (norm` U)
3		nvcni.n	. . 3 |- N = (norm` W)
4		nvcni.r	. . 3 |- R = (-v` U)
5		nvcni.s	. . 3 |- S = (-v` W)
6		nvcni.8	. . 3 |- C = (IndMet` U)
7		nvcni.d	. . 3 |- D = (IndMet` W)
8		nvcni.j	. . 3 |- J = (Open` C)
9		nvcni.k	. . 3 |- K = (Open` D)
10	1, 2, 3, 4, 5, 6, 7, 8, 9	nvcni 8337	. 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 ((M` (PRy)) < x -> (N` ((F` P)S(F` y))) < A)))
11	1, 4, 2	nvsub 8303	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ P e. X /\ y e. X) -> (M` (PRy)) = (M` (yRP)))
12	11	breq1d 2642	. . . . . . . . . 10 |- ((U e. NrmCVec /\ P e. X /\ y e. X) -> ((M` (PRy)) < x <-> (M` (yRP)) < x))
13	12	3expb 838	. . . . . . . . 9 |- ((U e. NrmCVec /\ (P e. X /\ y e. X)) -> ((M` (PRy)) < x <-> (M` (yRP)) < x))
14	13	3ad2antl1 813	. . . . . . . 8 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ (P e. X /\ y e. X)) -> ((M` (PRy)) < x <-> (M` (yRP)) < x))
15		eqid 1482	. . . . . . . . . . . . . . . . 17 |- (Base` W) = (Base` W)
16	15, 5, 3	nvsub 8303	. . . . . . . . . . . . . . . 16 |- ((W e. NrmCVec /\ (F` P) e. (Base` W) /\ (F` y) e. (Base` W)) -> (N` ((F` P)S(F` y))) = (N` ((F` y)S(F` P))))
17	16	3expb 838	. . . . . . . . . . . . . . 15 |- ((W e. NrmCVec /\ ((F` P) e. (Base` W) /\ (F` y) e. (Base` W))) -> (N` ((F` P)S(F` y))) = (N` ((F` y)S(F` P))))
18		ffvelrn 3828	. . . . . . . . . . . . . . . . 17 |- ((F:X-->(Base` W) /\ P e. X) -> (F` P) e. (Base` W))
19		ffvelrn 3828	. . . . . . . . . . . . . . . . 17 |- ((F:X-->(Base` W) /\ y e. X) -> (F` y) e. (Base` W))
20	18, 19	anim12i 333	. . . . . . . . . . . . . . . 16 |- (((F:X-->(Base` W) /\ P e. X) /\ (F:X-->(Base` W) /\ y e. X)) -> ((F` P) e. (Base` W) /\ (F` y) e. (Base` W)))
21	20	anandis 515	. . . . . . . . . . . . . . 15 |- ((F:X-->(Base` W) /\ (P e. X /\ y e. X)) -> ((F` P) e. (Base` W) /\ (F` y) e. (Base` W)))
22	17, 21	sylan2 454	. . . . . . . . . . . . . 14 |- ((W e. NrmCVec /\ (F:X-->(Base` W) /\ (P e. X /\ y e. X))) -> (N` ((F` P)S(F` y))) = (N` ((F` y)S(F` P))))
23	22	anassrs 444	. . . . . . . . . . . . 13 |- (((W e. NrmCVec /\ F:X-->(Base` W)) /\ (P e. X /\ y e. X)) -> (N` ((F` P)S(F` y))) = (N` ((F` y)S(F` P))))
24	23	ex 373	. . . . . . . . . . . 12 |- ((W e. NrmCVec /\ F:X-->(Base` W)) -> ((P e. X /\ y e. X) -> (N` ((F` P)S(F` y))) = (N` ((F` y)S(F` P)))))
25	24	3adant1 801	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ W e. NrmCVec /\ F:X-->(Base` W)) -> ((P e. X /\ y e. X) -> (N` ((F` P)S(F` y))) = (N` ((F` y)S(F` P)))))
26	1, 15, 6, 7, 8, 9	nvcnf 8335	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) -> F:X-->(Base` W))
27	25, 26	syld3an3 874	. . . . . . . . . 10 |- ((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) -> ((P e. X /\ y e. X) -> (N` ((F` P)S(F` y))) = (N` ((F` y)S(F` P)))))
28	27	imp 350	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ (P e. X /\ y e. X)) -> (N` ((F` P)S(F` y))) = (N` ((F` y)S(F` P))))
29	28	breq1d 2642	. . . . . . . 8 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ (P e. X /\ y e. X)) -> ((N` ((F` P)S(F` y))) < A <-> (N` ((F` y)S(F` P))) < A))
30	14, 29	imbi12d 629	. . . . . . 7 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ (P e. X /\ y e. X)) -> (((M` (PRy)) < x -> (N` ((F` P)S(F` y))) < A) <-> ((M` (yRP)) < x -> (N` ((F` y)S(F` P))) < A)))
31	30	anassrs 444	. . . . . 6 |- ((((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ P e. X) /\ y e. X) -> (((M` (PRy)) < x -> (N` ((F` P)S(F` y))) < A) <-> ((M` (yRP)) < x -> (N` ((F` y)S(F` P))) < A)))
32	31	ralbidva 1666	. . . . 5 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ P e. X) -> (A.y e. X ((M` (PRy)) < x -> (N` ((F` P)S(F` y))) < A) <-> A.y e. X ((M` (yRP)) < x -> (N` ((F` y)S(F` P))) < A)))
33	32	anbi2d 619	. . . 4 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ P e. X) -> ((0 < x /\ A.y e. X ((M` (PRy)) < x -> (N` ((F` P)S(F` y))) < A)) <-> (0 < x /\ A.y e. X ((M` (yRP)) < x -> (N` ((F` y)S(F` P))) < A))))
34	33	rexbidv 1671	. . 3 |- (((U e. NrmCVec /\ W e. NrmCVec /\ F e. (J Cn K)) /\ P e. X) -> (E.x e. RR (0 < x /\ A.y e. X ((M` (PRy)) < x -> (N` ((F` P)S(F` y))) < A)) <-> E.x e. RR (0 < x /\ A.y e. X ((M` (yRP)) < x -> (N` ((F` y)S(F` P))) < A))))
35	34	3ad2antr1 816	. 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 ((M` (PRy)) < x -> (N` ((F` P)S(F` y))) < A)) <-> E.x e. RR (0 < x /\ A.y e. X ((M` (yRP)) < x -> (N` ((F` y)S(F` P))) < A))))
36	10, 35	mpbid 195	1 |- (((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` (yRP)) < x -> (N` ((F` y)S(F` P))) < A)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 779   = wceq 960   e. wcel 962  A.wral 1652  E.wrex 1653   class class class wbr 2632  -->wf 3192  ` cfv 3196  (class class class)co 3977  RRcr 5246  0cc0 5247   < clt 5499   Cn ccn 7761  Opencopn 7801  NrmCVeccnv 8211  Basecba 8213  -vcnsb 8216  normcnm 8217  IndMetcims 8218

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979</