Theorem cnre2csqima

Description: Image of a centered square by the canonical bijection from ( RR X. RR ) to CC . (Contributed by Thierry Arnoux, 27-Sep-2017)

	Ref	Expression
Hypothesis	cnre2csqima.1	|- F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
Assertion	cnre2csqima	|- ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( Y e. ( ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) X. ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) -> ( ( abs ` ( Re ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D /\ ( abs ` ( Im ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnre2csqima.1	|- F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
2		ioossre	|- ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) C_ RR
3		ioossre	|- ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) C_ RR
4		xpinpreima2	|- ( ( ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) C_ RR /\ ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) C_ RR ) -> ( ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) X. ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) = ( ( `' ( 1st |` ( RR X. RR ) ) " ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) ) )
5	4	eleq2d	|- ( ( ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) C_ RR /\ ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) C_ RR ) -> ( Y e. ( ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) X. ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) <-> Y e. ( ( `' ( 1st |` ( RR X. RR ) ) " ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) ) ) )
6	2 3 5	mp2an	|- ( Y e. ( ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) X. ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) <-> Y e. ( ( `' ( 1st |` ( RR X. RR ) ) " ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) ) )
7		elin	|- ( Y e. ( ( `' ( 1st |` ( RR X. RR ) ) " ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) ) <-> ( Y e. ( `' ( 1st |` ( RR X. RR ) ) " ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) ) /\ Y e. ( `' ( 2nd |` ( RR X. RR ) ) " ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) ) )
8		simpl	|- ( ( x e. RR /\ y e. RR ) -> x e. RR )
9	8	recnd	|- ( ( x e. RR /\ y e. RR ) -> x e. CC )
10		ax-icn	|- _i e. CC
11	10	a1i	|- ( ( x e. RR /\ y e. RR ) -> _i e. CC )
12		simpr	|- ( ( x e. RR /\ y e. RR ) -> y e. RR )
13	12	recnd	|- ( ( x e. RR /\ y e. RR ) -> y e. CC )
14	11 13	mulcld	|- ( ( x e. RR /\ y e. RR ) -> ( _i x. y ) e. CC )
15	9 14	addcld	|- ( ( x e. RR /\ y e. RR ) -> ( x + ( _i x. y ) ) e. CC )
16		reval	|- ( ( x + ( _i x. y ) ) e. CC -> ( Re ` ( x + ( _i x. y ) ) ) = ( ( ( x + ( _i x. y ) ) + ( * ` ( x + ( _i x. y ) ) ) ) / 2 ) )
17	15 16	syl	|- ( ( x e. RR /\ y e. RR ) -> ( Re ` ( x + ( _i x. y ) ) ) = ( ( ( x + ( _i x. y ) ) + ( * ` ( x + ( _i x. y ) ) ) ) / 2 ) )
18		crre	|- ( ( x e. RR /\ y e. RR ) -> ( Re ` ( x + ( _i x. y ) ) ) = x )
19	17 18	eqtr3d	|- ( ( x e. RR /\ y e. RR ) -> ( ( ( x + ( _i x. y ) ) + ( * ` ( x + ( _i x. y ) ) ) ) / 2 ) = x )
20	19	mpoeq3ia	|- ( x e. RR , y e. RR |-> ( ( ( x + ( _i x. y ) ) + ( * ` ( x + ( _i x. y ) ) ) ) / 2 ) ) = ( x e. RR , y e. RR |-> x )
21	15	adantl	|- ( ( T. /\ ( x e. RR /\ y e. RR ) ) -> ( x + ( _i x. y ) ) e. CC )
22	1	a1i	|- ( T. -> F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) ) )
23		df-re	|- Re = ( z e. CC |-> ( ( z + ( * ` z ) ) / 2 ) )
24	23	a1i	|- ( T. -> Re = ( z e. CC |-> ( ( z + ( * ` z ) ) / 2 ) ) )
25		id	|- ( z = ( x + ( _i x. y ) ) -> z = ( x + ( _i x. y ) ) )
26		fveq2	|- ( z = ( x + ( _i x. y ) ) -> ( * ` z ) = ( * ` ( x + ( _i x. y ) ) ) )
27	25 26	oveq12d	|- ( z = ( x + ( _i x. y ) ) -> ( z + ( * ` z ) ) = ( ( x + ( _i x. y ) ) + ( * ` ( x + ( _i x. y ) ) ) ) )
28	27	oveq1d	|- ( z = ( x + ( _i x. y ) ) -> ( ( z + ( * ` z ) ) / 2 ) = ( ( ( x + ( _i x. y ) ) + ( * ` ( x + ( _i x. y ) ) ) ) / 2 ) )
29	21 22 24 28	fmpoco	|- ( T. -> ( Re o. F ) = ( x e. RR , y e. RR |-> ( ( ( x + ( _i x. y ) ) + ( * ` ( x + ( _i x. y ) ) ) ) / 2 ) ) )
30	29	mptru	|- ( Re o. F ) = ( x e. RR , y e. RR |-> ( ( ( x + ( _i x. y ) ) + ( * ` ( x + ( _i x. y ) ) ) ) / 2 ) )
31		df1stres	|- ( 1st |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> x )
32	20 30 31	3eqtr4ri	|- ( 1st |` ( RR X. RR ) ) = ( Re o. F )
33	15	rgen2	|- A. x e. RR A. y e. RR ( x + ( _i x. y ) ) e. CC
34	1	fnmpo	|- ( A. x e. RR A. y e. RR ( x + ( _i x. y ) ) e. CC -> F Fn ( RR X. RR ) )
35	33 34	ax-mp	|- F Fn ( RR X. RR )
36		fo1st	|- 1st : _V -onto-> _V
37		fofn	|- ( 1st : _V -onto-> _V -> 1st Fn _V )
38	36 37	ax-mp	|- 1st Fn _V
39		xp1st	|- ( z e. ( RR X. RR ) -> ( 1st ` z ) e. RR )
40	1	rnmpo	|- ran F = { z | E. x e. RR E. y e. RR z = ( x + ( _i x. y ) ) }
41		simpr	|- ( ( ( x e. RR /\ y e. RR ) /\ z = ( x + ( _i x. y ) ) ) -> z = ( x + ( _i x. y ) ) )
42	15	adantr	|- ( ( ( x e. RR /\ y e. RR ) /\ z = ( x + ( _i x. y ) ) ) -> ( x + ( _i x. y ) ) e. CC )
43	41 42	eqeltrd	|- ( ( ( x e. RR /\ y e. RR ) /\ z = ( x + ( _i x. y ) ) ) -> z e. CC )
44	43	ex	|- ( ( x e. RR /\ y e. RR ) -> ( z = ( x + ( _i x. y ) ) -> z e. CC ) )
45	44	rexlimivv	|- ( E. x e. RR E. y e. RR z = ( x + ( _i x. y ) ) -> z e. CC )
46	45	abssi	|- { z | E. x e. RR E. y e. RR z = ( x + ( _i x. y ) ) } C_ CC
47	40 46	eqsstri	|- ran F C_ CC
48		simpl	|- ( ( z e. ran F /\ u e. ran F ) -> z e. ran F )
49	47 48	sseldi	|- ( ( z e. ran F /\ u e. ran F ) -> z e. CC )
50		simpr	|- ( ( z e. ran F /\ u e. ran F ) -> u e. ran F )
51	47 50	sseldi	|- ( ( z e. ran F /\ u e. ran F ) -> u e. CC )
52	49 51	resubd	|- ( ( z e. ran F /\ u e. ran F ) -> ( Re ` ( z - u ) ) = ( ( Re ` z ) - ( Re ` u ) ) )
53	32 35 38 39 52	cnre2csqlem	|- ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( Y e. ( `' ( 1st |` ( RR X. RR ) ) " ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) ) -> ( abs ` ( Re ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D ) )
54		imval	|- ( ( x + ( _i x. y ) ) e. CC -> ( Im ` ( x + ( _i x. y ) ) ) = ( Re ` ( ( x + ( _i x. y ) ) / _i ) ) )
55	15 54	syl	|- ( ( x e. RR /\ y e. RR ) -> ( Im ` ( x + ( _i x. y ) ) ) = ( Re ` ( ( x + ( _i x. y ) ) / _i ) ) )
56		crim	|- ( ( x e. RR /\ y e. RR ) -> ( Im ` ( x + ( _i x. y ) ) ) = y )
57	55 56	eqtr3d	|- ( ( x e. RR /\ y e. RR ) -> ( Re ` ( ( x + ( _i x. y ) ) / _i ) ) = y )
58	57	mpoeq3ia	|- ( x e. RR , y e. RR |-> ( Re ` ( ( x + ( _i x. y ) ) / _i ) ) ) = ( x e. RR , y e. RR |-> y )
59		df-im	|- Im = ( z e. CC |-> ( Re ` ( z / _i ) ) )
60	59	a1i	|- ( T. -> Im = ( z e. CC |-> ( Re ` ( z / _i ) ) ) )
61		fvoveq1	|- ( z = ( x + ( _i x. y ) ) -> ( Re ` ( z / _i ) ) = ( Re ` ( ( x + ( _i x. y ) ) / _i ) ) )
62	21 22 60 61	fmpoco	|- ( T. -> ( Im o. F ) = ( x e. RR , y e. RR |-> ( Re ` ( ( x + ( _i x. y ) ) / _i ) ) ) )
63	62	mptru	|- ( Im o. F ) = ( x e. RR , y e. RR |-> ( Re ` ( ( x + ( _i x. y ) ) / _i ) ) )
64		df2ndres	|- ( 2nd |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> y )
65	58 63 64	3eqtr4ri	|- ( 2nd |` ( RR X. RR ) ) = ( Im o. F )
66		fo2nd	|- 2nd : _V -onto-> _V
67		fofn	|- ( 2nd : _V -onto-> _V -> 2nd Fn _V )
68	66 67	ax-mp	|- 2nd Fn _V
69		xp2nd	|- ( z e. ( RR X. RR ) -> ( 2nd ` z ) e. RR )
70	49 51	imsubd	|- ( ( z e. ran F /\ u e. ran F ) -> ( Im ` ( z - u ) ) = ( ( Im ` z ) - ( Im ` u ) ) )
71	65 35 68 69 70	cnre2csqlem	|- ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( Y e. ( `' ( 2nd |` ( RR X. RR ) ) " ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) -> ( abs ` ( Im ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D ) )
72	53 71	anim12d	|- ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( ( Y e. ( `' ( 1st |` ( RR X. RR ) ) " ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) ) /\ Y e. ( `' ( 2nd |` ( RR X. RR ) ) " ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) ) -> ( ( abs ` ( Re ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D /\ ( abs ` ( Im ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D ) ) )
73	7 72	syl5bi	|- ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( Y e. ( ( `' ( 1st |` ( RR X. RR ) ) " ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) ) -> ( ( abs ` ( Re ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D /\ ( abs ` ( Im ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D ) ) )
74	6 73	syl5bi	|- ( ( X e. ( RR X. RR ) /\ Y e. ( RR X. RR ) /\ D e. RR+ ) -> ( Y e. ( ( ( ( 1st ` X ) - D ) (,) ( ( 1st ` X ) + D ) ) X. ( ( ( 2nd ` X ) - D ) (,) ( ( 2nd ` X ) + D ) ) ) -> ( ( abs ` ( Re ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D /\ ( abs ` ( Im ` ( ( F ` Y ) - ( F ` X ) ) ) ) < D ) ) )