Theorem cncfmet 7905

Description: Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.)

Hypotheses

Ref	Expression
cncfmet.1	|- C = ((abs o. - ) |` (A X. A))
cncfmet.2	|- D = ((abs o. - ) |` (B X. B))
cncfmet.3	|- J = (Open` C)
cncfmet.4	|- K = (Open` D)

Assertion

Ref	Expression
cncfmet	|- ((A (_ CC /\ B (_ CC) -> (A-cn->B) = (J Cn K))

Proof of Theorem cncfmet

Step	Hyp	Ref	Expression
1		feq23 3623	. . . . . . . 8 |- ((dom dom C = A /\ dom dom D = B) -> (f:dom dom C-->dom dom D <-> f:A-->B))
2		ssxp 3256	. . . . . . . . . . . . . 14 |- ((A (_ CC /\ A (_ CC) -> (A X. A) (_ (CC X. CC))
3	2	anidms 434	. . . . . . . . . . . . 13 |- (A (_ CC -> (A X. A) (_ (CC X. CC))
4		df-ss 2053	. . . . . . . . . . . . 13 |- ((A X. A) (_ (CC X. CC) <-> ((A X. A) i^i (CC X. CC)) = (A X. A))
5	3, 4	sylib 198	. . . . . . . . . . . 12 |- (A (_ CC -> ((A X. A) i^i (CC X. CC)) = (A X. A))
6		absf 6906	. . . . . . . . . . . . . . 15 |- abs:CC-->RR
7		subopr 5370	. . . . . . . . . . . . . . 15 |- - :(CC X. CC)-->CC
8		fco 3636	. . . . . . . . . . . . . . 15 |- ((abs:CC-->RR /\ - :(CC X. CC)-->CC) -> (abs o. - ):(CC X. CC)-->RR)
9	6, 7, 8	mp2an 697	. . . . . . . . . . . . . 14 |- (abs o. - ):(CC X. CC)-->RR
10	9	fdmi 3632	. . . . . . . . . . . . 13 |- dom (abs o. - ) = (CC X. CC)
11	10	ineq2i 2214	. . . . . . . . . . . 12 |- ((A X. A) i^i dom (abs o. - )) = ((A X. A) i^i (CC X. CC))
12	5, 11	syl5eq 1519	. . . . . . . . . . 11 |- (A (_ CC -> ((A X. A) i^i dom (abs o. - )) = (A X. A))
13		cncfmet.1	. . . . . . . . . . . . 13 |- C = ((abs o. - ) |` (A X. A))
14	13	dmeqi 3312	. . . . . . . . . . . 12 |- dom C = dom ((abs o. - ) |` (A X. A))
15		dmres 3380	. . . . . . . . . . . 12 |- dom ((abs o. - ) |` (A X. A)) = ((A X. A) i^i dom (abs o. - ))
16	14, 15	eqtr 1495	. . . . . . . . . . 11 |- dom C = ((A X. A) i^i dom (abs o. - ))
17	12, 16	syl5eq 1519	. . . . . . . . . 10 |- (A (_ CC -> dom C = (A X. A))
18	17	dmeqd 3313	. . . . . . . . 9 |- (A (_ CC -> dom dom C = dom ( A X. A))
19		dmxpid 3333	. . . . . . . . 9 |- dom ( A X. A) = A
20	18, 19	syl6eq 1523	. . . . . . . 8 |- (A (_ CC -> dom dom C = A)
21		ssxp 3256	. . . . . . . . . . . . . 14 |- ((B (_ CC /\ B (_ CC) -> (B X. B) (_ (CC X. CC))
22	21	anidms 434	. . . . . . . . . . . . 13 |- (B (_ CC -> (B X. B) (_ (CC X. CC))
23		df-ss 2053	. . . . . . . . . . . . 13 |- ((B X. B) (_ (CC X. CC) <-> ((B X. B) i^i (CC X. CC)) = (B X. B))
24	22, 23	sylib 198	. . . . . . . . . . . 12 |- (B (_ CC -> ((B X. B) i^i (CC X. CC)) = (B X. B))
25	10	ineq2i 2214	. . . . . . . . . . . 12 |- ((B X. B) i^i dom (abs o. - )) = ((B X. B) i^i (CC X. CC))
26	24, 25	syl5eq 1519	. . . . . . . . . . 11 |- (B (_ CC -> ((B X. B) i^i dom (abs o. - )) = (B X. B))
27		cncfmet.2	. . . . . . . . . . . . 13 |- D = ((abs o. - ) |` (B X. B))
28	27	dmeqi 3312	. . . . . . . . . . . 12 |- dom D = dom ((abs o. - ) |` (B X. B))
29		dmres 3380	. . . . . . . . . . . 12 |- dom ((abs o. - ) |` (B X. B)) = ((B X. B) i^i dom (abs o. - ))
30	28, 29	eqtr 1495	. . . . . . . . . . 11 |- dom D = ((B X. B) i^i dom (abs o. - ))
31	26, 30	syl5eq 1519	. . . . . . . . . 10 |- (B (_ CC -> dom D = (B X. B))
32	31	dmeqd 3313	. . . . . . . . 9 |- (B (_ CC -> dom dom D = dom ( B X. B))
33		dmxpid 3333	. . . . . . . . 9 |- dom ( B X. B) = B
34	32, 33	syl6eq 1523	. . . . . . . 8 |- (B (_ CC -> dom dom D = B)
35	1, 20, 34	syl2an 454	. . . . . . 7 |- ((A (_ CC /\ B (_ CC) -> (f:dom dom C-->dom dom D <-> f:A-->B))
36	35	anbi1d 617	. . . . . 6 |- ((A (_ CC /\ B (_ CC) -> ((f:dom dom C-->dom dom D /\ A.x e. dom dom CA.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom C((xCw) < z -> ((f` x)D(f` w)) < y)))) <-> (f:A-->B /\ A.x e. dom dom CA.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom C((xCw) < z -> ((f` x)D(f` w)) < y))))))
37	20	3ad2ant1 800	. . . . . . . . . . . 12 |- ((A (_ CC /\ B (_ CC /\ f:A-->B) -> dom dom C = A)
38	37	eleq2d 1541	. . . . . . . . . . 11 |- ((A (_ CC /\ B (_ CC /\ f:A-->B) -> (x e. dom dom C <-> x e. A))
39	38	imbi1d 613	. . . . . . . . . 10 |- ((A (_ CC /\ B (_ CC /\ f:A-->B) -> ((x e. dom dom C -> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom C((xCw) < z -> ((f` x)D(f` w)) < y)))) <-> (x e. A -> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. dom dom C((xCw) < z -> ((f` x)D(f` w)) < y))))))
40	37	adantr 389	. . . . . . . . . . . . . . . . . . . . 21 |- (((A (_ CC /\ B (_ CC /\ f:A-->B) /\ x e. A) -> dom dom C = A)
41	40	eleq2d 1541	. . . . . . . . . . . . . . . . . . . 20 |- (((A (_ CC /\ B (_ CC /\ f:A-->B) /\ x e. A) -> (w e. dom dom C <-> w e. A))
42	41	imbi1d 613	. . . . . . . . . . . . . . . . . . 19 |- (((A (_ CC /\ B (_ CC /\ f:A-->B) /\ x e. A) -> ((w e. dom dom C -> ((xCw) < z -> ((f` x)D(f` w)) < y)) <-> (w e. A -> ((xCw) < z -> ((f` x)D(f` w)) < y))))
43		oprvalres 4033	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x e. A /\ w e. A) -> (x((abs o. - ) |` (A X. A))w) = (x(abs o. - )w))
44	13	opreqi 3974	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (xCw) = (x((abs o. - ) |` (A X. A))w)
45	43, 44	syl5eq 1519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x e. A /\ w e. A) -> (xCw) = (x(abs o. - )w))
46	45	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A (_ CC /\ (x e. A /\ w e. A)) -> (xCw) = (x(abs o. - )w))
47		ssel 2063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A (_ CC -> (x e. A -> x e. CC))
48		ssel 2063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A (_ CC -> (w e. A -> w e. CC))
49	47, 48	anim12d 558	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A (_ CC -> ((x e. A /\ w e. A) -> (x e. CC /\ w e. CC)))
50	49	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A (_ CC /\ (x e. A /\ w e. A)) -> (x e. CC /\ w e. CC))
51		eqid 1475	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (abs o. - ) = (abs o. - )
52	51	cnmetdval 7902	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x e. CC /\ w e. CC) -> (x(abs o. - )w) = (abs` (x - w)))
53	50, 52	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A (_ CC /\ (x e. A /\ w e. A)) -> (x(abs o. - )w) = (abs` (x - w)))
54	46, 53	eqtrd 1507	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A (_ CC /\ (x e. A /\ w e. A)) -> (xCw) = (abs` (x - w)))
55	54	3ad2antl1 809	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A (_ CC /\ B (_ CC /\ f:A-->B) /\ (x e. A /\ w e. A)) -> (xCw) = (abs` (x - w)))
56	55	breq1d 2629	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((A (_ CC /\ B (_ CC /\ f:A-->B) /\ (x e. A /\ w e. A)) -> ((xCw) < z <-> (abs` (x - w)) < z))
57		ffvelrn 3814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f:A-->B /\ x e. A) -> (f` x) e. B)
58	57	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:A-->B -> (x e. A -> (f` x) e. B))
59		ffvelrn 3814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f:A-->B /\ w e. A) -> (f` w) e. B)
60	59	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:A-->B -> (w e. A -> (f` w) e. B))
61	58, 60	anim12d 558	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:A-->B -> ((x e. A /\ w e. A) -> ((f` x) e. B /\ (f` w) e. B)))
62	61	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f:A-->B /\ (x e. A /\ w e. A)) -> ((f` x) e. B /\ (f` w) e. B))
63	62	3ad2antl3 811	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((A (_ CC /\ B (_ CC /\ f:A-->B) /\ (x e. A /\ w e. A)) -> ((f` x) e. B /\ (f` w) e. B))
64		oprvalres 4033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((f` x) e. B /\ (f` w)