eff1olem

Description: The exponential function maps the set S , of complex numbers with imaginary part in a real interval of length 2 x. _pi , one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008) (Proof shortened by Mario Carneiro, 13-May-2014)

	Ref	Expression
Hypotheses	eff1olem.1	$⊢ F = (w \in D ⟼ e^{i w})$
	eff1olem.2	$⊢ S = ℑ^{-1} [D]$
	eff1olem.3	$⊢ φ \to D \subseteq ℝ$
	eff1olem.4	$⊢ (φ \land (x \in D \land y \in D)) \to \|x - y\| < 2 π$
	eff1olem.5	$⊢ (φ \land z \in ℝ) \to \exists y \in D \frac{z - y}{2 π} \in ℤ$
Assertion	eff1olem	$⊢ φ \to ({\exp ↾}_{S}) : S \underset{1-1 onto}{⟶} ℂ ∖ \{0\}$

Proof

Step	Hyp	Ref	Expression
1		eff1olem.1	$⊢ F = (w \in D ⟼ e^{i w})$
2		eff1olem.2	$⊢ S = ℑ^{-1} [D]$
3		eff1olem.3	$⊢ φ \to D \subseteq ℝ$
4		eff1olem.4	$⊢ (φ \land (x \in D \land y \in D)) \to \|x - y\| < 2 π$
5		eff1olem.5	$⊢ (φ \land z \in ℝ) \to \exists y \in D \frac{z - y}{2 π} \in ℤ$
6		cnvimass	$⊢ ℑ^{-1} [D] \subseteq dom ℑ$
7		imf	$⊢ ℑ : ℂ ⟶ ℝ$
8	7	fdmi	$⊢ dom ℑ = ℂ$
9	8	eqcomi	$⊢ ℂ = dom ℑ$
10	6 2 9	3sstr4i	$⊢ S \subseteq ℂ$
11		eff2	$⊢ \exp : ℂ ⟶ ℂ ∖ \{0\}$
12	11	a1i	$⊢ S \subseteq ℂ \to \exp : ℂ ⟶ ℂ ∖ \{0\}$
13	12	feqmptd	$⊢ S \subseteq ℂ \to \exp = (y \in ℂ ⟼ e^{y})$
14	13	reseq1d	$⊢ S \subseteq ℂ \to {\exp ↾}_{S} = {(y \in ℂ ⟼ e^{y}) ↾}_{S}$
15		resmpt	$⊢ S \subseteq ℂ \to {(y \in ℂ ⟼ e^{y}) ↾}_{S} = (y \in S ⟼ e^{y})$
16	14 15	eqtrd	$⊢ S \subseteq ℂ \to {\exp ↾}_{S} = (y \in S ⟼ e^{y})$
17	10 16	ax-mp	$⊢ {\exp ↾}_{S} = (y \in S ⟼ e^{y})$
18	10	sseli	$⊢ y \in S \to y \in ℂ$
19	11	ffvelcdmi	$⊢ y \in ℂ \to e^{y} \in (ℂ ∖ \{0\})$
20	18 19	syl	$⊢ y \in S \to e^{y} \in (ℂ ∖ \{0\})$
21	20	adantl	$⊢ (φ \land y \in S) \to e^{y} \in (ℂ ∖ \{0\})$
22		eldifsn	$⊢ x \in (ℂ ∖ \{0\}) \leftrightarrow (x \in ℂ \land x \neq 0)$
23	22	bilani	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to (x \in ℂ \land x \neq 0)$
24	23	simpld	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to x \in ℂ$
25	23	simprd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to x \neq 0$
26	24 25	absrpcld	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \|x\| \in ℝ^{+}$
27		reeff1o	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{1-1 onto}{⟶} ℝ^{+}$
28		f1ocnv	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{1-1 onto}{⟶} ℝ^{+} \to {({\exp ↾}_{ℝ})}^{-1} : ℝ^{+} \underset{1-1 onto}{⟶} ℝ$
29		f1of	$⊢ {({\exp ↾}_{ℝ})}^{-1} : ℝ^{+} \underset{1-1 onto}{⟶} ℝ \to {({\exp ↾}_{ℝ})}^{-1} : ℝ^{+} ⟶ ℝ$
30	27 28 29	mp2b	$⊢ {({\exp ↾}_{ℝ})}^{-1} : ℝ^{+} ⟶ ℝ$
31	30	ffvelcdmi	$⊢ \|x\| \in ℝ^{+} \to {({\exp ↾}_{ℝ})}^{-1} (\|x\|) \in ℝ$
32	26 31	syl	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to {({\exp ↾}_{ℝ})}^{-1} (\|x\|) \in ℝ$
33	32	recnd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to {({\exp ↾}_{ℝ})}^{-1} (\|x\|) \in ℂ$
34		ax-icn	$⊢ i \in ℂ$
35	3	adantr	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to D \subseteq ℝ$
36		eqid	$⊢ {abs}^{-1} [\{1\}] = {abs}^{-1} [\{1\}]$
37		eqid	$⊢ {\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]} = {\sin ↾}_{[- \frac{π}{2}, \frac{π}{2}]}$
38	1 36 3 4 5 37	efif1olem4	$⊢ φ \to F : D \underset{1-1 onto}{⟶} {abs}^{-1} [\{1\}]$
39		f1ocnv	$⊢ F : D \underset{1-1 onto}{⟶} {abs}^{-1} [\{1\}] \to F^{-1} : {abs}^{-1} [\{1\}] \underset{1-1 onto}{⟶} D$
40		f1of	$⊢ F^{-1} : {abs}^{-1} [\{1\}] \underset{1-1 onto}{⟶} D \to F^{-1} : {abs}^{-1} [\{1\}] ⟶ D$
41	38 39 40	3syl	$⊢ φ \to F^{-1} : {abs}^{-1} [\{1\}] ⟶ D$
42	41	adantr	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to F^{-1} : {abs}^{-1} [\{1\}] ⟶ D$
43	24	abscld	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \|x\| \in ℝ$
44	43	recnd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \|x\| \in ℂ$
45	24 25	absne0d	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \|x\| \neq 0$
46	24 44 45	divcld	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \frac{x}{\|x\|} \in ℂ$
47	24 44 45	absdivd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \|\frac{x}{\|x\|}\| = \frac{\|x\|}{\|\|x\|\|}$
48		absidm	$⊢ x \in ℂ \to \|\|x\|\| = \|x\|$
49	24 48	syl	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \|\|x\|\| = \|x\|$
50	49	oveq2d	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \frac{\|x\|}{\|\|x\|\|} = \frac{\|x\|}{\|x\|}$
51	44 45	dividd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \frac{\|x\|}{\|x\|} = 1$
52	47 50 51	3eqtrd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \|\frac{x}{\|x\|}\| = 1$
53		absf	$⊢ abs : ℂ ⟶ ℝ$
54		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
55		fniniseg	$⊢ abs Fn ℂ \to (\frac{x}{\|x\|} \in {abs}^{-1} [\{1\}] \leftrightarrow (\frac{x}{\|x\|} \in ℂ \land \|\frac{x}{\|x\|}\| = 1))$
56	53 54 55	mp2b	$⊢ \frac{x}{\|x\|} \in {abs}^{-1} [\{1\}] \leftrightarrow (\frac{x}{\|x\|} \in ℂ \land \|\frac{x}{\|x\|}\| = 1)$
57	46 52 56	sylanbrc	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \frac{x}{\|x\|} \in {abs}^{-1} [\{1\}]$
58	42 57	ffvelcdmd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to F^{-1} (\frac{x}{\|x\|}) \in D$
59	35 58	sseldd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to F^{-1} (\frac{x}{\|x\|}) \in ℝ$
60	59	recnd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to F^{-1} (\frac{x}{\|x\|}) \in ℂ$
61		mulcl	$⊢ (i \in ℂ \land F^{-1} (\frac{x}{\|x\|}) \in ℂ) \to i F^{-1} (\frac{x}{\|x\|}) \in ℂ$
62	34 60 61	sylancr	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to i F^{-1} (\frac{x}{\|x\|}) \in ℂ$
63	33 62	addcld	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \in ℂ$
64	32 59	crimd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to ℑ ({({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|})) = F^{-1} (\frac{x}{\|x\|})$
65	64 58	eqeltrd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to ℑ ({({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|})) \in D$
66		ffn	$⊢ ℑ : ℂ ⟶ ℝ \to ℑ Fn ℂ$
67		elpreima	$⊢ ℑ Fn ℂ \to ({({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \in ℑ^{-1} [D] \leftrightarrow ({({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \in ℂ \land ℑ ({({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|})) \in D))$
68	7 66 67	mp2b	$⊢ {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \in ℑ^{-1} [D] \leftrightarrow ({({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \in ℂ \land ℑ ({({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|})) \in D)$
69	63 65 68	sylanbrc	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \in ℑ^{-1} [D]$
70	69 2	eleqtrrdi	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \in S$
71		efadd	$⊢ ({({\exp ↾}_{ℝ})}^{-1} (\|x\|) \in ℂ \land i F^{-1} (\frac{x}{\|x\|}) \in ℂ) \to e^{{({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|})} = e^{{({\exp ↾}_{ℝ})}^{-1} (\|x\|)} e^{i F^{-1} (\frac{x}{\|x\|})}$
72	33 62 71	syl2anc	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to e^{{({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|})} = e^{{({\exp ↾}_{ℝ})}^{-1} (\|x\|)} e^{i F^{-1} (\frac{x}{\|x\|})}$
73	32	fvresd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to ({\exp ↾}_{ℝ}) ({({\exp ↾}_{ℝ})}^{-1} (\|x\|)) = e^{{({\exp ↾}_{ℝ})}^{-1} (\|x\|)}$
74		f1ocnvfv2	$⊢ (({\exp ↾}_{ℝ}) : ℝ \underset{1-1 onto}{⟶} ℝ^{+} \land \|x\| \in ℝ^{+}) \to ({\exp ↾}_{ℝ}) ({({\exp ↾}_{ℝ})}^{-1} (\|x\|)) = \|x\|$
75	27 26 74	sylancr	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to ({\exp ↾}_{ℝ}) ({({\exp ↾}_{ℝ})}^{-1} (\|x\|)) = \|x\|$
76	73 75	eqtr3d	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to e^{{({\exp ↾}_{ℝ})}^{-1} (\|x\|)} = \|x\|$
77		oveq2	$⊢ z = F^{-1} (\frac{x}{\|x\|}) \to i z = i F^{-1} (\frac{x}{\|x\|})$
78	77	fveq2d	$⊢ z = F^{-1} (\frac{x}{\|x\|}) \to e^{i z} = e^{i F^{-1} (\frac{x}{\|x\|})}$
79		oveq2	$⊢ w = z \to i w = i z$
80	79	fveq2d	$⊢ w = z \to e^{i w} = e^{i z}$
81	80	cbvmptv	$⊢ (w \in D ⟼ e^{i w}) = (z \in D ⟼ e^{i z})$
82	1 81	eqtri	$⊢ F = (z \in D ⟼ e^{i z})$
83		fvex	$⊢ e^{i F^{-1} (\frac{x}{\|x\|})} \in V$
84	78 82 83	fvmpt	$⊢ F^{-1} (\frac{x}{\|x\|}) \in D \to F (F^{-1} (\frac{x}{\|x\|})) = e^{i F^{-1} (\frac{x}{\|x\|})}$
85	58 84	syl	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to F (F^{-1} (\frac{x}{\|x\|})) = e^{i F^{-1} (\frac{x}{\|x\|})}$
86	38	adantr	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to F : D \underset{1-1 onto}{⟶} {abs}^{-1} [\{1\}]$
87		f1ocnvfv2	$⊢ (F : D \underset{1-1 onto}{⟶} {abs}^{-1} [\{1\}] \land \frac{x}{\|x\|} \in {abs}^{-1} [\{1\}]) \to F (F^{-1} (\frac{x}{\|x\|})) = \frac{x}{\|x\|}$
88	86 57 87	syl2anc	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to F (F^{-1} (\frac{x}{\|x\|})) = \frac{x}{\|x\|}$
89	85 88	eqtr3d	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to e^{i F^{-1} (\frac{x}{\|x\|})} = \frac{x}{\|x\|}$
90	76 89	oveq12d	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to e^{{({\exp ↾}_{ℝ})}^{-1} (\|x\|)} e^{i F^{-1} (\frac{x}{\|x\|})} = \|x\| (\frac{x}{\|x\|})$
91	24 44 45	divcan2d	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \|x\| (\frac{x}{\|x\|}) = x$
92	72 90 91	3eqtrrd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to x = e^{{({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|})}$
93	92	adantrl	$⊢ (φ \land (y \in S \land x \in (ℂ ∖ \{0\}))) \to x = e^{{({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|})}$
94		fveq2	$⊢ y = {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \to e^{y} = e^{{({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|})}$
95	94	eqeq2d	$⊢ y = {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \to (x = e^{y} \leftrightarrow x = e^{{({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|})})$
96	93 95	syl5ibrcom	$⊢ (φ \land (y \in S \land x \in (ℂ ∖ \{0\}))) \to (y = {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \to x = e^{y})$
97	18	adantl	$⊢ (φ \land y \in S) \to y \in ℂ$
98	97	replimd	$⊢ (φ \land y \in S) \to y = ℜ (y) + i ℑ (y)$
99		absef	$⊢ y \in ℂ \to \|e^{y}\| = e^{ℜ (y)}$
100	97 99	syl	$⊢ (φ \land y \in S) \to \|e^{y}\| = e^{ℜ (y)}$
101	97	recld	$⊢ (φ \land y \in S) \to ℜ (y) \in ℝ$
102	101	fvresd	$⊢ (φ \land y \in S) \to ({\exp ↾}_{ℝ}) (ℜ (y)) = e^{ℜ (y)}$
103	100 102	eqtr4d	$⊢ (φ \land y \in S) \to \|e^{y}\| = ({\exp ↾}_{ℝ}) (ℜ (y))$
104	103	fveq2d	$⊢ (φ \land y \in S) \to {({\exp ↾}_{ℝ})}^{-1} (\|e^{y}\|) = {({\exp ↾}_{ℝ})}^{-1} (({\exp ↾}_{ℝ}) (ℜ (y)))$
105		f1ocnvfv1	$⊢ (({\exp ↾}_{ℝ}) : ℝ \underset{1-1 onto}{⟶} ℝ^{+} \land ℜ (y) \in ℝ) \to {({\exp ↾}_{ℝ})}^{-1} (({\exp ↾}_{ℝ}) (ℜ (y))) = ℜ (y)$
106	27 101 105	sylancr	$⊢ (φ \land y \in S) \to {({\exp ↾}_{ℝ})}^{-1} (({\exp ↾}_{ℝ}) (ℜ (y))) = ℜ (y)$
107	104 106	eqtrd	$⊢ (φ \land y \in S) \to {({\exp ↾}_{ℝ})}^{-1} (\|e^{y}\|) = ℜ (y)$
108	97	imcld	$⊢ (φ \land y \in S) \to ℑ (y) \in ℝ$
109	108	recnd	$⊢ (φ \land y \in S) \to ℑ (y) \in ℂ$
110		mulcl	$⊢ (i \in ℂ \land ℑ (y) \in ℂ) \to i ℑ (y) \in ℂ$
111	34 109 110	sylancr	$⊢ (φ \land y \in S) \to i ℑ (y) \in ℂ$
112		efcl	$⊢ i ℑ (y) \in ℂ \to e^{i ℑ (y)} \in ℂ$
113	111 112	syl	$⊢ (φ \land y \in S) \to e^{i ℑ (y)} \in ℂ$
114	101	recnd	$⊢ (φ \land y \in S) \to ℜ (y) \in ℂ$
115		efcl	$⊢ ℜ (y) \in ℂ \to e^{ℜ (y)} \in ℂ$
116	114 115	syl	$⊢ (φ \land y \in S) \to e^{ℜ (y)} \in ℂ$
117		efne0	$⊢ ℜ (y) \in ℂ \to e^{ℜ (y)} \neq 0$
118	114 117	syl	$⊢ (φ \land y \in S) \to e^{ℜ (y)} \neq 0$
119	113 116 118	divcan3d	$⊢ (φ \land y \in S) \to \frac{e^{ℜ (y)} e^{i ℑ (y)}}{e^{ℜ (y)}} = e^{i ℑ (y)}$
120	98	fveq2d	$⊢ (φ \land y \in S) \to e^{y} = e^{ℜ (y) + i ℑ (y)}$
121		efadd	$⊢ (ℜ (y) \in ℂ \land i ℑ (y) \in ℂ) \to e^{ℜ (y) + i ℑ (y)} = e^{ℜ (y)} e^{i ℑ (y)}$
122	114 111 121	syl2anc	$⊢ (φ \land y \in S) \to e^{ℜ (y) + i ℑ (y)} = e^{ℜ (y)} e^{i ℑ (y)}$
123	120 122	eqtrd	$⊢ (φ \land y \in S) \to e^{y} = e^{ℜ (y)} e^{i ℑ (y)}$
124	123 100	oveq12d	$⊢ (φ \land y \in S) \to \frac{e^{y}}{\|e^{y}\|} = \frac{e^{ℜ (y)} e^{i ℑ (y)}}{e^{ℜ (y)}}$
125		elpreima	$⊢ ℑ Fn ℂ \to (y \in ℑ^{-1} [D] \leftrightarrow (y \in ℂ \land ℑ (y) \in D))$
126	7 66 125	mp2b	$⊢ y \in ℑ^{-1} [D] \leftrightarrow (y \in ℂ \land ℑ (y) \in D)$
127	126	simprbi	$⊢ y \in ℑ^{-1} [D] \to ℑ (y) \in D$
128	127 2	eleq2s	$⊢ y \in S \to ℑ (y) \in D$
129	128	adantl	$⊢ (φ \land y \in S) \to ℑ (y) \in D$
130		oveq2	$⊢ w = ℑ (y) \to i w = i ℑ (y)$
131	130	fveq2d	$⊢ w = ℑ (y) \to e^{i w} = e^{i ℑ (y)}$
132		fvex	$⊢ e^{i ℑ (y)} \in V$
133	131 1 132	fvmpt	$⊢ ℑ (y) \in D \to F (ℑ (y)) = e^{i ℑ (y)}$
134	129 133	syl	$⊢ (φ \land y \in S) \to F (ℑ (y)) = e^{i ℑ (y)}$
135	119 124 134	3eqtr4d	$⊢ (φ \land y \in S) \to \frac{e^{y}}{\|e^{y}\|} = F (ℑ (y))$
136	135	fveq2d	$⊢ (φ \land y \in S) \to F^{-1} (\frac{e^{y}}{\|e^{y}\|}) = F^{-1} (F (ℑ (y)))$
137		f1ocnvfv1	$⊢ (F : D \underset{1-1 onto}{⟶} {abs}^{-1} [\{1\}] \land ℑ (y) \in D) \to F^{-1} (F (ℑ (y))) = ℑ (y)$
138	38 128 137	syl2an	$⊢ (φ \land y \in S) \to F^{-1} (F (ℑ (y))) = ℑ (y)$
139	136 138	eqtrd	$⊢ (φ \land y \in S) \to F^{-1} (\frac{e^{y}}{\|e^{y}\|}) = ℑ (y)$
140	139	oveq2d	$⊢ (φ \land y \in S) \to i F^{-1} (\frac{e^{y}}{\|e^{y}\|}) = i ℑ (y)$
141	107 140	oveq12d	$⊢ (φ \land y \in S) \to {({\exp ↾}_{ℝ})}^{-1} (\|e^{y}\|) + i F^{-1} (\frac{e^{y}}{\|e^{y}\|}) = ℜ (y) + i ℑ (y)$
142	98 141	eqtr4d	$⊢ (φ \land y \in S) \to y = {({\exp ↾}_{ℝ})}^{-1} (\|e^{y}\|) + i F^{-1} (\frac{e^{y}}{\|e^{y}\|})$
143		fveq2	$⊢ x = e^{y} \to \|x\| = \|e^{y}\|$
144	143	fveq2d	$⊢ x = e^{y} \to {({\exp ↾}_{ℝ})}^{-1} (\|x\|) = {({\exp ↾}_{ℝ})}^{-1} (\|e^{y}\|)$
145		id	$⊢ x = e^{y} \to x = e^{y}$
146	145 143	oveq12d	$⊢ x = e^{y} \to \frac{x}{\|x\|} = \frac{e^{y}}{\|e^{y}\|}$
147	146	fveq2d	$⊢ x = e^{y} \to F^{-1} (\frac{x}{\|x\|}) = F^{-1} (\frac{e^{y}}{\|e^{y}\|})$
148	147	oveq2d	$⊢ x = e^{y} \to i F^{-1} (\frac{x}{\|x\|}) = i F^{-1} (\frac{e^{y}}{\|e^{y}\|})$
149	144 148	oveq12d	$⊢ x = e^{y} \to {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) = {({\exp ↾}_{ℝ})}^{-1} (\|e^{y}\|) + i F^{-1} (\frac{e^{y}}{\|e^{y}\|})$
150	149	eqeq2d	$⊢ x = e^{y} \to (y = {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \leftrightarrow y = {({\exp ↾}_{ℝ})}^{-1} (\|e^{y}\|) + i F^{-1} (\frac{e^{y}}{\|e^{y}\|}))$
151	142 150	syl5ibrcom	$⊢ (φ \land y \in S) \to (x = e^{y} \to y = {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}))$
152	151	adantrr	$⊢ (φ \land (y \in S \land x \in (ℂ ∖ \{0\}))) \to (x = e^{y} \to y = {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}))$
153	96 152	impbid	$⊢ (φ \land (y \in S \land x \in (ℂ ∖ \{0\}))) \to (y = {({\exp ↾}_{ℝ})}^{-1} (\|x\|) + i F^{-1} (\frac{x}{\|x\|}) \leftrightarrow x = e^{y})$
154	17 21 70 153	f1o2d	$⊢ φ \to ({\exp ↾}_{S}) : S \underset{1-1 onto}{⟶} ℂ ∖ \{0\}$

Metamath Proof Explorer

Theorem eff1olem

Proof