Theorem nvcnpi4 8423

Description: Epsilon-delta property of a linear operator continuous at a point.)

Hypotheses

Ref	Expression
nvcnpi3.1	|- X = (Base` U)
nvcnpi3.m	|- M = (norm` U)
nvcnpi3.n	|- N = (norm` W)
nvcnpi3.r	|- R = (-v` U)
nvcnpi3.8	|- C = (IndMet` U)
nvcnpi3.d	|- D = (IndMet` W)
nvcnpi3.j	|- J = (Open` C)
nvcnpi3.k	|- K = (Open` D)
nvcnpi3.l	|- L = (U LnOp W)
nvcnpi3.t	|- T e. L

Assertion

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

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

Proof of Theorem nvcnpi4

Step	Hyp	Ref	Expression
1		eqid 1475	. . . . 5 |- dom dom C = dom dom C
2		nvcnpi3.j	. . . . 5 |- J = (Open` C)
3		eqid 1475	. . . . 5 |- dom dom D = dom dom D
4		nvcnpi3.k	. . . . 5 |- K = (Open` D)
5	1, 2, 3, 4	metcnpi4 7893	. . . 4 |- (((C e. Met /\ D e. Met /\ P e. dom dom C) /\ (T e. ((J CnP K)` P) /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((T` P)D(T` y)) <_ A)))
6		nvcnpi3.8	. . . . . . 7 |- C = (IndMet` U)
7	6	imsmet 8324	. . . . . 6 |- (U e. NrmCVec -> C e. Met)
8	7	3ad2ant1 800	. . . . 5 |- ((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) -> C e. Met)
9		nvcnpi3.d	. . . . . . 7 |- D = (IndMet` W)
10	9	imsmet 8324	. . . . . 6 |- (W e. NrmCVec -> D e. Met)
11	10	3ad2ant2 801	. . . . 5 |- ((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) -> D e. Met)
12		nvcnpi3.1	. . . . . . . . 9 |- X = (Base` U)
13	12, 6	imsba 8321	. . . . . . . 8 |- (U e. NrmCVec -> X = dom dom C)
14	13	eleq2d 1541	. . . . . . 7 |- (U e. NrmCVec -> (P e. X <-> P e. dom dom C))
15	14	biimpa 416	. . . . . 6 |- ((U e. NrmCVec /\ P e. X) -> P e. dom dom C)
16	15	3adant2 798	. . . . 5 |- ((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) -> P e. dom dom C)
17	8, 11, 16	3jca 819	. . . 4 |- ((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) -> (C e. Met /\ D e. Met /\ P e. dom dom C))
18	5, 17	sylan 448	. . 3 |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ (T e. ((J CnP K)` P) /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((T` P)D(T` y)) <_ A)))
19	13	raleq1d 1789	. . . . . . 7 |- (U e. NrmCVec -> (A.y e. X ((PCy) <_ x -> ((T` P)D(T` y)) <_ A) <-> A.y e. dom dom C((PCy) <_ x -> ((T` P)D(T` y)) <_ A)))
20	19	anbi2d 616	. . . . . 6 |- (U e. NrmCVec -> ((0 < x /\ A.y e. X ((PCy) <_ x -> ((T` P)D(T` y)) <_ A)) <-> (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((T` P)D(T` y)) <_ A))))
21	20	rexbidv 1664	. . . . 5 |- (U e. NrmCVec -> (E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((T` P)D(T` y)) <_ A)) <-> E.x e. RR (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((T` P)D(T` y)) <_ A))))
22	21	3ad2ant1 800	. . . 4 |- ((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) -> (E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((T` P)D(T` y)) <_ A)) <-> E.x e. RR (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((T` P)D(T` y)) <_ A))))
23	22	adantr 389	. . 3 |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ (T e. ((J CnP K)` P) /\ A e. RR /\ 0 < A)) -> (E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((T` P)D(T` y)) <_ A)) <-> E.x e. RR (0 < x /\ A.y e. dom dom C((PCy) <_ x -> ((T` P)D(T` y)) <_ A))))
24	18, 23	mpbird 196	. 2 |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ (T e. ((J CnP K)` P) /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((T` P)D(T` y)) <_ A)))
25		nvcnpi3.r	. . . . . . . . . . . . 13 |- R = (-v` U)
26		nvcnpi3.m	. . . . . . . . . . . . 13 |- M = (norm` U)
27	12, 25, 26, 6	imsdval 8317	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ P e. X /\ y e. X) -> (PCy) = (M` (PRy)))
28	27	3expb 834	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ (P e. X /\ y e. X)) -> (PCy) = (M` (PRy)))
29	28	adantlr 393	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (P e. X /\ y e. X)) -> (PCy) = (M` (PRy)))
30	29	breq1d 2629	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (P e. X /\ y e. X)) -> ((PCy) <_ x <-> (M` (PRy)) <_ x))
31		eqid 1475	. . . . . . . . . . . . 13 |- (Base` W) = (Base` W)
32		eqid 1475	. . . . . . . . . . . . 13 |- (-v` W) = (-v` W)
33		nvcnpi3.n	. . . . . . . . . . . . 13 |- N = (norm` W)
34	31, 32, 33, 9	imsdval 8317	. . . . . . . . . . . 12 |- ((W e. NrmCVec /\ (T` P) e. (Base` W) /\ (T` y) e. (Base` W)) -> ((T` P)D(T` y)) = (N` ((T` P)(-v` W)(T` y))))
35		simplr 413	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (P e. X /\ y e. X)) -> W e. NrmCVec)
36		ffvelrn 3814	. . . . . . . . . . . . . 14 |- ((T:X-->(Base` W) /\ P e. X) -> (T` P) e. (Base` W))
37		nvcnpi3.t	. . . . . . . . . . . . . . 15 |- T e. L
38		nvcnpi3.l	. . . . . . . . . . . . . . . 16 |- L = (U LnOp W)
39	12, 31, 38	lnof 8416	. . . . . . . . . . . . . . 15 |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) -> T:X-->(Base` W))
40	37, 39	mp3an3 905	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ W e. NrmCVec) -> T:X-->(Base` W))
41	36, 40	sylan 448	. . . . . . . . . . . . 13 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ P e. X) -> (T` P) e. (Base` W))
42	41	adantrr 395	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (P e. X /\ y e. X)) -> (T` P) e. (Base` W))
43		ffvelrn 3814	. . . . . . . . . . . . . 14 |- ((T:X-->(Base` W) /\ y e. X) -> (T` y) e. (Base` W))
44	43, 40	sylan 448	. . . . . . . . . . . . 13 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ y e. X) -> (T` y) e. (Base` W))
45	44	adantrl 394	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (P e. X /\ y e. X)) -> (T` y) e. (Base` W))
46	34, 35, 42, 45	syl3anc 858	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (P e. X /\ y e. X)) -> ((T` P)D(T` y)) = (N` ((T` P)(-v` W)(T` y))))
47	12, 25, 32, 38	lnosub 8420	. . . . . . . . . . . . 13 |- (((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) /\ (P e. X /\ y e. X)) -> (T` (PRy)) = ((T` P)(-v` W)(T` y)))
48	37, 47	mp3anl3 912	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (P e. X /\ y e. X)) -> (T` (PRy)) = ((T` P)(-v` W)(T` y)))
49	48	fveq2d 3728	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (P e. X /\ y e. X)) -> (N` (T` (PRy))) = (N` ((T` P)(-v` W)(T` y))))
50	46, 49	eqtr4d 1510	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (P e. X /\ y e. X)) -> ((T` P)D(T` y)) = (N` (T` (PRy))))
51	50	breq1d 2629	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (P e. X /\ y e. X)) -> (((T` P)D(T` y)) <_ A <-> (N` (T` (PRy))) <_ A))
52	30, 51	imbi12d 626	. . . . . . . 8 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (P e. X /\ y e. X)) -> (((PCy) <_ x -> ((T` P)D(T` y)) <_ A) <-> ((M` (PRy)) <_ x -> (N` (T` (PRy))) <_ A)))
53	52	exp43 384	. . . . . . 7 |- (U e. NrmCVec -> (W e. NrmCVec -> (P e. X -> (y e. X -> (((PCy) <_ x -> ((T` P)D(T` y)) <_ A) <-> ((M