Theorem cncfmet 7857

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 3615	. . . . . . . 8 |- ((dom dom C = A /\ dom dom D = B) -> (f:dom dom C-->dom dom D <-> f:A-->B))
2		ssxp 3251	. . . . . . . . . . . . . 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 2049	. . . . . . . . . . . . 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 6851	. . . . . . . . . . . . . . 15 |- abs:CC-->RR
7		subopr 5350	. . . . . . . . . . . . . . 15 |- - :(CC X. CC)-->CC
8		fco 3627	. . . . . . . . . . . . . . 15 |- ((abs:CC-->RR /\ - :(CC X. CC)-->CC) -> (abs o. - ):(CC X. CC)-->RR)
9	6, 7, 8	mp2an 696	. . . . . . . . . . . . . 14 |- (abs o. - ):(CC X. CC)-->RR
10		fdm 3623	. . . . . . . . . . . . . 14 |- ((abs o. - ):(CC X. CC)-->RR -> dom (abs o. - ) = (CC X. CC))
11	9, 10	ax-mp 7	. . . . . . . . . . . . 13 |- dom (abs o. - ) = (CC X. CC)
12	11	ineq2i 2210	. . . . . . . . . . . 12 |- ((A X. A) i^i dom (abs o. - )) = ((A X. A) i^i (CC X. CC))
13	5, 12	syl5eq 1516	. . . . . . . . . . 11 |- (A (_ CC -> ((A X. A) i^i dom (abs o. - )) = (A X. A))
14		cncfmet.1	. . . . . . . . . . . . 13 |- C = ((abs o. - ) |` (A X. A))
15	14	dmeqi 3307	. . . . . . . . . . . 12 |- dom C = dom ((abs o. - ) |` (A X. A))
16		dmres 3372	. . . . . . . . . . . 12 |- dom ((abs o. - ) |` (A X. A)) = ((A X. A) i^i dom (abs o. - ))
17	15, 16	eqtr 1492	. . . . . . . . . . 11 |- dom C = ((A X. A) i^i dom (abs o. - ))
18	13, 17	syl5eq 1516	. . . . . . . . . 10 |- (A (_ CC -> dom C = (A X. A))
19	18	dmeqd 3308	. . . . . . . . 9 |- (A (_ CC -> dom dom C = dom ( A X. A))
20		dmxpid 3328	. . . . . . . . 9 |- dom ( A X. A) = A
21	19, 20	syl6eq 1520	. . . . . . . 8 |- (A (_ CC -> dom dom C = A)
22		ssxp 3251	. . . . . . . . . . . . . 14 |- ((B (_ CC /\ B (_ CC) -> (B X. B) (_ (CC X. CC))
23	22	anidms 434	. . . . . . . . . . . . 13 |- (B (_ CC -> (B X. B) (_ (CC X. CC))
24		df-ss 2049	. . . . . . . . . . . . 13 |- ((B X. B) (_ (CC X. CC) <-> ((B X. B) i^i (CC X. CC)) = (B X. B))
25	23, 24	sylib 198	. . . . . . . . . . . 12 |- (B (_ CC -> ((B X. B) i^i (CC X. CC)) = (B X. B))
26	11	ineq2i 2210	. . . . . . . . . . . 12 |- ((B X. B) i^i dom (abs o. - )) = ((B X. B) i^i (CC X. CC))
27	25, 26	syl5eq 1516	. . . . . . . . . . 11 |- (B (_ CC -> ((B X. B) i^i dom (abs o. - )) = (B X. B))
28		cncfmet.2	. . . . . . . . . . . . 13 |- D = ((abs o. - ) |` (B X. B))
29	28	dmeqi 3307	. . . . . . . . . . . 12 |- dom D = dom ((abs o. - ) |` (B X. B))
30		dmres 3372	. . . . . . . . . . . 12 |- dom ((abs o. - ) |` (B X. B)) = ((B X. B) i^i dom (abs o. - ))
31	29, 30	eqtr 1492	. . . . . . . . . . 11 |- dom D = ((B X. B) i^i dom (abs o. - ))
32	27, 31	syl5eq 1516	. . . . . . . . . 10 |- (B (_ CC -> dom D = (B X. B))
33	32	dmeqd 3308	. . . . . . . . 9 |- (B (_ CC -> dom dom D = dom ( B X. B))
34		dmxpid 3328	. . . . . . . . 9 |- dom ( B X. B) = B
35	33, 34	syl6eq 1520	. . . . . . . 8 |- (B (_ CC -> dom dom D = B)
36	1, 21, 35	syl2an 454	. . . . . . 7 |- ((A (_ CC /\ B (_ CC) -> (f:dom dom C-->dom dom D <-> f:A-->B))
37	36	anbi1d 616	. . . . . 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))))))
38	21	3ad2ant1 799	. . . . . . . . . . . 12 |- ((A (_ CC /\ B (_ CC /\ f:A-->B) -> dom dom C = A)
39	38	eleq2d 1538	. . . . . . . . . . 11 |- ((A (_ CC /\ B (_ CC /\ f:A-->B) -> (x e. dom dom C <-> x e. A))
40	39	imbi1d 612	. . . . . . . . . 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))))))
41	38	adantr 389	. . . . . . . . . . . . . . . . . . . . 21 |- (((A (_ CC /\ B (_ CC /\ f:A-->B) /\ x e. A) -> dom dom C = A)
42	41	eleq2d 1538	. . . . . . . . . . . . . . . . . . . 20 |- (((A (_ CC /\ B (_ CC /\ f:A-->B) /\ x e. A) -> (w e. dom dom C <-> w e. A))
43	42	imbi1d 612	. . . . . . . . . . . . . . . . . . 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))))
44		oprvalres 4024	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x e. A /\ w e. A) -> (x((abs o. - ) |` (A X. A))w) = (x(abs o. - )w))
45	14	opreqi 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (xCw) = (x((abs o. - ) |` (A X. A))w)
46	44, 45	syl5eq 1516	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x e. A /\ w e. A) -> (xCw) = (x(abs o. - )w))
47	46	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A (_ CC /\ (x e. A /\ w e. A)) -> (xCw) = (x(abs o. - )w))
48		ssel 2059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A (_ CC -> (x e. A -> x e. CC))
49		ssel 2059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A (_ CC -> (w e. A -> w e. CC))
50	48, 49	anim12d 557	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A (_ CC -> ((x e. A /\ w e. A) -> (x e. CC /\ w e. CC)))
51	50	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A (_ CC /\ (x e. A /\ w e. A)) -> (x e. CC /\ w e. CC))
52		eqid 1473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (abs o. - ) = (abs o. - )
53	52	cnmetdval 7854	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x e. CC /\ w e. CC) -> (x(abs o. - )w) = (abs` (x - w)))
54	51, 53	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A (_ CC /\ (x e. A /\ w e. A)) -> (x(abs o. - )w) = (abs` (x - w)))
55	47, 54	eqtrd 1504	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A (_ CC /\ (x e. A /\ w e. A)) -> (xCw) = (abs` (x - w)))
56	55	3ad2antl1 808	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A (_ CC /\ B (_ CC /\ f:A-->B) /\ (x e. A /\ w e. A)) -> (xCw) = (abs` (x - w)))
57	56	breq1d 2624	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((A (_ CC /\ B (_ CC /\ f:A-->B) /\ (x e. A /\ w e. A)) -> ((xCw) < z <-> (abs` (x - w)) < z))
58		ffvelrn 3805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f:A-->B /\ x e. A) -> (f` x) e. B)
59	58	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:A-->B -> (x e. A -> (f` x) e. B))
60		ffvelrn 3805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f:A-->B /\ w e. A) -> (f` w) e. B)
61	60	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:A-->B -> (w e. A -> (f` w) e. B))
62	59, 61	anim12d 557	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:A-->B -> ((x e. A /\ w e. A) -> ((f` x) e. B /\ (f` w) e. B)))
63	62	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f:A-->B /\ (x e. A /\ w e. A)) -> ((f` x) e. B /\ (f` w) e. B))
64	63	3ad2antl3 810	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((A (_ CC /\ B (_ CC /\ f:A-->B) /\ (x e. A /\ w e. A)) -> ((f` x)