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

Metamath Proof Explorer

Theorem eff1olem

Proof