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 \in ℝ, y \in ℝ ⟼ x + i y)$
	Assertion	cnre2csqima	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (Y \in ((1^{st} (X) - D, 1^{st} (X) + D) \times (2^{nd} (X) - D, 2^{nd} (X) + D)) \to (\|ℜ (F (Y) - F (X))\| < D \land \|ℑ (F (Y) - F (X))\| < D))$

Proof

Step	Hyp	Ref	Expression
1		cnre2csqima.1	$⊢ F = (x \in ℝ, y \in ℝ ⟼ x + i y)$
2		ioossre	$⊢ (1^{st} (X) - D, 1^{st} (X) + D) \subseteq ℝ$
3		ioossre	$⊢ (2^{nd} (X) - D, 2^{nd} (X) + D) \subseteq ℝ$
4		xpinpreima2	$⊢ ((1^{st} (X) - D, 1^{st} (X) + D) \subseteq ℝ \land (2^{nd} (X) - D, 2^{nd} (X) + D) \subseteq ℝ) \to (1^{st} (X) - D, 1^{st} (X) + D) \times (2^{nd} (X) - D, 2^{nd} (X) + D) = {({1^{st} ↾}_{ℝ^{2}})}^{-1} [(1^{st} (X) - D, 1^{st} (X) + D)] \cap {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [(2^{nd} (X) - D, 2^{nd} (X) + D)]$
5	4	eleq2d	$⊢ ((1^{st} (X) - D, 1^{st} (X) + D) \subseteq ℝ \land (2^{nd} (X) - D, 2^{nd} (X) + D) \subseteq ℝ) \to (Y \in ((1^{st} (X) - D, 1^{st} (X) + D) \times (2^{nd} (X) - D, 2^{nd} (X) + D)) \leftrightarrow Y \in ({({1^{st} ↾}_{ℝ^{2}})}^{-1} [(1^{st} (X) - D, 1^{st} (X) + D)] \cap {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [(2^{nd} (X) - D, 2^{nd} (X) + D)]))$
6	2 3 5	mp2an	$⊢ Y \in ((1^{st} (X) - D, 1^{st} (X) + D) \times (2^{nd} (X) - D, 2^{nd} (X) + D)) \leftrightarrow Y \in ({({1^{st} ↾}_{ℝ^{2}})}^{-1} [(1^{st} (X) - D, 1^{st} (X) + D)] \cap {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [(2^{nd} (X) - D, 2^{nd} (X) + D)])$
7		elin	$⊢ Y \in ({({1^{st} ↾}_{ℝ^{2}})}^{-1} [(1^{st} (X) - D, 1^{st} (X) + D)] \cap {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [(2^{nd} (X) - D, 2^{nd} (X) + D)]) \leftrightarrow (Y \in {({1^{st} ↾}_{ℝ^{2}})}^{-1} [(1^{st} (X) - D, 1^{st} (X) + D)] \land Y \in {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [(2^{nd} (X) - D, 2^{nd} (X) + D)])$
8		simpl	$⊢ (x \in ℝ \land y \in ℝ) \to x \in ℝ$
9	8	recnd	$⊢ (x \in ℝ \land y \in ℝ) \to x \in ℂ$
10		ax-icn	$⊢ i \in ℂ$
11	10	a1i	$⊢ (x \in ℝ \land y \in ℝ) \to i \in ℂ$
12		simpr	$⊢ (x \in ℝ \land y \in ℝ) \to y \in ℝ$
13	12	recnd	$⊢ (x \in ℝ \land y \in ℝ) \to y \in ℂ$
14	11 13	mulcld	$⊢ (x \in ℝ \land y \in ℝ) \to i y \in ℂ$
15	9 14	addcld	$⊢ (x \in ℝ \land y \in ℝ) \to x + i y \in ℂ$
16		reval	$⊢ x + i y \in ℂ \to ℜ (x + i y) = \frac{x + i y + \overline{x + i y}}{2}$
17	15 16	syl	$⊢ (x \in ℝ \land y \in ℝ) \to ℜ (x + i y) = \frac{x + i y + \overline{x + i y}}{2}$
18		crre	$⊢ (x \in ℝ \land y \in ℝ) \to ℜ (x + i y) = x$
19	17 18	eqtr3d	$⊢ (x \in ℝ \land y \in ℝ) \to \frac{x + i y + \overline{x + i y}}{2} = x$
20	19	mpoeq3ia	$⊢ (x \in ℝ, y \in ℝ ⟼ \frac{x + i y + \overline{x + i y}}{2}) = (x \in ℝ, y \in ℝ ⟼ x)$
21	15	adantl	$⊢ (⊤ \land (x \in ℝ \land y \in ℝ)) \to x + i y \in ℂ$
22	1	a1i	$⊢ ⊤ \to F = (x \in ℝ, y \in ℝ ⟼ x + i y)$
23		df-re	$⊢ ℜ = (z \in ℂ ⟼ \frac{z + \overline{z}}{2})$
24	23	a1i	$⊢ ⊤ \to ℜ = (z \in ℂ ⟼ \frac{z + \overline{z}}{2})$
25		id	$⊢ z = x + i y \to z = x + i y$
26		fveq2	$⊢ z = x + i y \to \overline{z} = \overline{x + i y}$
27	25 26	oveq12d	$⊢ z = x + i y \to z + \overline{z} = x + i y + \overline{x + i y}$
28	27	oveq1d	$⊢ z = x + i y \to \frac{z + \overline{z}}{2} = \frac{x + i y + \overline{x + i y}}{2}$
29	21 22 24 28	fmpoco	$⊢ ⊤ \to ℜ \circ F = (x \in ℝ, y \in ℝ ⟼ \frac{x + i y + \overline{x + i y}}{2})$
30	29	mptru	$⊢ ℜ \circ F = (x \in ℝ, y \in ℝ ⟼ \frac{x + i y + \overline{x + i y}}{2})$
31		df1stres	$⊢ {1^{st} ↾}_{ℝ^{2}} = (x \in ℝ, y \in ℝ ⟼ x)$
32	20 30 31	3eqtr4ri	$⊢ {1^{st} ↾}_{ℝ^{2}} = ℜ \circ F$
33	15	rgen2	$⊢ \forall x \in ℝ \forall y \in ℝ x + i y \in ℂ$
34	1	fnmpo	$⊢ \forall x \in ℝ \forall y \in ℝ x + i y \in ℂ \to F Fn ℝ^{2}$
35	33 34	ax-mp	$⊢ F Fn ℝ^{2}$
36		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
37		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
38	36 37	ax-mp	$⊢ 1^{st} Fn V$
39		xp1st	$⊢ z \in ℝ^{2} \to 1^{st} (z) \in ℝ$
40	1	rnmpo	$⊢ ran F = \{z \| \exists x \in ℝ \exists y \in ℝ z = x + i y\}$
41		simpr	$⊢ ((x \in ℝ \land y \in ℝ) \land z = x + i y) \to z = x + i y$
42	15	adantr	$⊢ ((x \in ℝ \land y \in ℝ) \land z = x + i y) \to x + i y \in ℂ$
43	41 42	eqeltrd	$⊢ ((x \in ℝ \land y \in ℝ) \land z = x + i y) \to z \in ℂ$
44	43	ex	$⊢ (x \in ℝ \land y \in ℝ) \to (z = x + i y \to z \in ℂ)$
45	44	rexlimivv	$⊢ \exists x \in ℝ \exists y \in ℝ z = x + i y \to z \in ℂ$
46	45	abssi	$⊢ \{z \| \exists x \in ℝ \exists y \in ℝ z = x + i y\} \subseteq ℂ$
47	40 46	eqsstri	$⊢ ran F \subseteq ℂ$
48		simpl	$⊢ (z \in ran F \land u \in ran F) \to z \in ran F$
49	47 48	sseldi	$⊢ (z \in ran F \land u \in ran F) \to z \in ℂ$
50		simpr	$⊢ (z \in ran F \land u \in ran F) \to u \in ran F$
51	47 50	sseldi	$⊢ (z \in ran F \land u \in ran F) \to u \in ℂ$
52	49 51	resubd	$⊢ (z \in ran F \land u \in ran F) \to ℜ (z - u) = ℜ (z) - ℜ (u)$
53	32 35 38 39 52	cnre2csqlem	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (Y \in {({1^{st} ↾}_{ℝ^{2}})}^{-1} [(1^{st} (X) - D, 1^{st} (X) + D)] \to \|ℜ (F (Y) - F (X))\| < D)$
54		imval	$⊢ x + i y \in ℂ \to ℑ (x + i y) = ℜ (\frac{x + i y}{i})$
55	15 54	syl	$⊢ (x \in ℝ \land y \in ℝ) \to ℑ (x + i y) = ℜ (\frac{x + i y}{i})$
56		crim	$⊢ (x \in ℝ \land y \in ℝ) \to ℑ (x + i y) = y$
57	55 56	eqtr3d	$⊢ (x \in ℝ \land y \in ℝ) \to ℜ (\frac{x + i y}{i}) = y$
58	57	mpoeq3ia	$⊢ (x \in ℝ, y \in ℝ ⟼ ℜ (\frac{x + i y}{i})) = (x \in ℝ, y \in ℝ ⟼ y)$
59		df-im	$⊢ ℑ = (z \in ℂ ⟼ ℜ (\frac{z}{i}))$
60	59	a1i	$⊢ ⊤ \to ℑ = (z \in ℂ ⟼ ℜ (\frac{z}{i}))$
61		fvoveq1	$⊢ z = x + i y \to ℜ (\frac{z}{i}) = ℜ (\frac{x + i y}{i})$
62	21 22 60 61	fmpoco	$⊢ ⊤ \to ℑ \circ F = (x \in ℝ, y \in ℝ ⟼ ℜ (\frac{x + i y}{i}))$
63	62	mptru	$⊢ ℑ \circ F = (x \in ℝ, y \in ℝ ⟼ ℜ (\frac{x + i y}{i}))$
64		df2ndres	$⊢ {2^{nd} ↾}_{ℝ^{2}} = (x \in ℝ, y \in ℝ ⟼ y)$
65	58 63 64	3eqtr4ri	$⊢ {2^{nd} ↾}_{ℝ^{2}} = ℑ \circ F$
66		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
67		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
68	66 67	ax-mp	$⊢ 2^{nd} Fn V$
69		xp2nd	$⊢ z \in ℝ^{2} \to 2^{nd} (z) \in ℝ$
70	49 51	imsubd	$⊢ (z \in ran F \land u \in ran F) \to ℑ (z - u) = ℑ (z) - ℑ (u)$
71	65 35 68 69 70	cnre2csqlem	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (Y \in {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [(2^{nd} (X) - D, 2^{nd} (X) + D)] \to \|ℑ (F (Y) - F (X))\| < D)$
72	53 71	anim12d	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to ((Y \in {({1^{st} ↾}_{ℝ^{2}})}^{-1} [(1^{st} (X) - D, 1^{st} (X) + D)] \land Y \in {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [(2^{nd} (X) - D, 2^{nd} (X) + D)]) \to (\|ℜ (F (Y) - F (X))\| < D \land \|ℑ (F (Y) - F (X))\| < D))$
73	7 72	syl5bi	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (Y \in ({({1^{st} ↾}_{ℝ^{2}})}^{-1} [(1^{st} (X) - D, 1^{st} (X) + D)] \cap {({2^{nd} ↾}_{ℝ^{2}})}^{-1} [(2^{nd} (X) - D, 2^{nd} (X) + D)]) \to (\|ℜ (F (Y) - F (X))\| < D \land \|ℑ (F (Y) - F (X))\| < D))$
74	6 73	syl5bi	$⊢ (X \in ℝ^{2} \land Y \in ℝ^{2} \land D \in ℝ^{+}) \to (Y \in ((1^{st} (X) - D, 1^{st} (X) + D) \times (2^{nd} (X) - D, 2^{nd} (X) + D)) \to (\|ℜ (F (Y) - F (X))\| < D \land \|ℑ (F (Y) - F (X))\| < D))$

Metamath Proof Explorer

Theorem cnre2csqima

Proof