Theorem seff

Description: Let set S be the real or complex numbers. Then the exponential function restricted to S is a mapping from S to S . (Contributed by Steve Rodriguez, 6-Nov-2015)

	Ref	Expression
Hypothesis	seff.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
Assertion	seff	$$⊢\phi \to \left({\exp \upharpoonright }_S\right):S⟶S$$

Proof

Step	Hyp	Ref	Expression
1		seff.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		elpri	$$⊢S\in \left\{ℝ,ℂ\right\}\to \left(S=ℝ\vee S=ℂ\right)$$
3		reeff1	$$⊢\left({\exp \upharpoonright }_{ℝ}\right):ℝ\underset{1-1}{⟶}{ℝ}^{+}$$
4		f1f	$$⊢\left({\exp \upharpoonright }_{ℝ}\right):ℝ\underset{1-1}{⟶}{ℝ}^{+}\to \left({\exp \upharpoonright }_{ℝ}\right):ℝ⟶{ℝ}^{+}$$
5		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
6		fss	$$⊢\left(\left({\exp \upharpoonright }_{ℝ}\right):ℝ⟶{ℝ}^{+}\wedge {ℝ}^{+}\subseteq ℝ\right)\to \left({\exp \upharpoonright }_{ℝ}\right):ℝ⟶ℝ$$
7	5 6	mpan2	$$⊢\left({\exp \upharpoonright }_{ℝ}\right):ℝ⟶{ℝ}^{+}\to \left({\exp \upharpoonright }_{ℝ}\right):ℝ⟶ℝ$$
8	3 4 7	mp2b	$$⊢\left({\exp \upharpoonright }_{ℝ}\right):ℝ⟶ℝ$$
9		feq23	$$⊢\left(S=ℝ\wedge S=ℝ\right)\to \left(\left({\exp \upharpoonright }_{ℝ}\right):S⟶S\leftrightarrow \left({\exp \upharpoonright }_{ℝ}\right):ℝ⟶ℝ\right)$$
10	9	anidms	$$⊢S=ℝ\to \left(\left({\exp \upharpoonright }_{ℝ}\right):S⟶S\leftrightarrow \left({\exp \upharpoonright }_{ℝ}\right):ℝ⟶ℝ\right)$$
11	8 10	mpbiri	$$⊢S=ℝ\to \left({\exp \upharpoonright }_{ℝ}\right):S⟶S$$
12		reseq2	$$⊢S=ℝ\to {\exp \upharpoonright }_S={\exp \upharpoonright }_{ℝ}$$
13	12	feq1d	$$⊢S=ℝ\to \left(\left({\exp \upharpoonright }_S\right):S⟶S\leftrightarrow \left({\exp \upharpoonright }_{ℝ}\right):S⟶S\right)$$
14	11 13	mpbird	$$⊢S=ℝ\to \left({\exp \upharpoonright }_S\right):S⟶S$$
15		eff	$$⊢\exp :ℂ⟶ℂ$$
16		frel	$$⊢\exp :ℂ⟶ℂ\to \mathrm{Rel}\exp$$
17		resdm	$$⊢\mathrm{Rel}\exp \to {\exp \upharpoonright }_{\mathrm{dom}\exp }=\exp$$
18	15 16 17	mp2b	$$⊢{\exp \upharpoonright }_{\mathrm{dom}\exp }=\exp$$
19	15	fdmi	$$⊢\mathrm{dom}\exp =ℂ$$
20	19	reseq2i	$$⊢{\exp \upharpoonright }_{\mathrm{dom}\exp }={\exp \upharpoonright }_{ℂ}$$
21	18 20	eqtr3i	$$⊢\exp ={\exp \upharpoonright }_{ℂ}$$
22	21	feq1i	$$⊢\exp :ℂ⟶ℂ\leftrightarrow \left({\exp \upharpoonright }_{ℂ}\right):ℂ⟶ℂ$$
23	15 22	mpbi	$$⊢\left({\exp \upharpoonright }_{ℂ}\right):ℂ⟶ℂ$$
24		feq23	$$⊢\left(S=ℂ\wedge S=ℂ\right)\to \left(\left({\exp \upharpoonright }_{ℂ}\right):S⟶S\leftrightarrow \left({\exp \upharpoonright }_{ℂ}\right):ℂ⟶ℂ\right)$$
25	24	anidms	$$⊢S=ℂ\to \left(\left({\exp \upharpoonright }_{ℂ}\right):S⟶S\leftrightarrow \left({\exp \upharpoonright }_{ℂ}\right):ℂ⟶ℂ\right)$$
26	23 25	mpbiri	$$⊢S=ℂ\to \left({\exp \upharpoonright }_{ℂ}\right):S⟶S$$
27		reseq2	$$⊢S=ℂ\to {\exp \upharpoonright }_S={\exp \upharpoonright }_{ℂ}$$
28	27	feq1d	$$⊢S=ℂ\to \left(\left({\exp \upharpoonright }_S\right):S⟶S\leftrightarrow \left({\exp \upharpoonright }_{ℂ}\right):S⟶S\right)$$
29	26 28	mpbird	$$⊢S=ℂ\to \left({\exp \upharpoonright }_S\right):S⟶S$$
30	14 29	jaoi	$$⊢\left(S=ℝ\vee S=ℂ\right)\to \left({\exp \upharpoonright }_S\right):S⟶S$$
31	1 2 30	3syl	$$⊢\phi \to \left({\exp \upharpoonright }_S\right):S⟶S$$