Theorem reefgim

Description: The exponential function is a group isomorphism from the group of reals under addition to the group of positive reals under multiplication. (Contributed by Mario Carneiro, 21-Jun-2015) (Revised by Thierry Arnoux, 30-Jun-2019)

	Ref	Expression
Hypothesis	reefgim.1	$$⊢P={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}{ℝ}^{+}$$
Assertion	reefgim	$$⊢{\exp \upharpoonright }_{ℝ}\in \left({ℝ}_{\mathrm{fld}}\mathrm{GrpIso}P\right)$$

Proof

Step	Hyp	Ref	Expression
1		reefgim.1	$$⊢P={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}{ℝ}^{+}$$
2		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
3		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
4	3	rpmsubg	$$⊢{ℝ}^{+}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
5		cnex	$$⊢ℂ\in \mathrm{V}$$
6	5	difexi	$$⊢ℂ\setminus \left\{0\right\}\in \mathrm{V}$$
7		rpcndif0	$$⊢x\in {ℝ}^{+}\to x\in \left(ℂ\setminus \left\{0\right\}\right)$$
8	7	ssriv	$$⊢{ℝ}^{+}\subseteq ℂ\setminus \left\{0\right\}$$
9		ressabs	$$⊢\left(ℂ\setminus \left\{0\right\}\in \mathrm{V}\wedge {ℝ}^{+}\subseteq ℂ\setminus \left\{0\right\}\right)\to \left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right){\upharpoonright }_{𝑠}{ℝ}^{+}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}{ℝ}^{+}$$
10	6 8 9	mp2an	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right){\upharpoonright }_{𝑠}{ℝ}^{+}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}{ℝ}^{+}$$
11	1 10	eqtr4i	$$⊢P=\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right){\upharpoonright }_{𝑠}{ℝ}^{+}$$
12	11	subgbas	$$⊢{ℝ}^{+}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)\to {ℝ}^{+}={\mathrm{Base}}_P$$
13	4 12	ax-mp	$$⊢{ℝ}^{+}={\mathrm{Base}}_P$$
14		replusg	$$⊢+={+}_{{ℝ}_{\mathrm{fld}}}$$
15		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
16		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
17	15 16	mgpplusg	$$⊢\times ={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
18	1 17	ressplusg	$$⊢{ℝ}^{+}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)\to \times ={+}_P$$
19	4 18	ax-mp	$$⊢\times ={+}_P$$
20		resubdrg	$$⊢\left(ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\right)$$
21	20	simpli	$$⊢ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
22		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
23	22	subrgring	$$⊢ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to {ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$$
24	21 23	ax-mp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$$
25		ringgrp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℝ}_{\mathrm{fld}}\in \mathrm{Grp}$$
26	24 25	mp1i	$$⊢\top \to {ℝ}_{\mathrm{fld}}\in \mathrm{Grp}$$
27	11	subggrp	$$⊢{ℝ}^{+}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)\to P\in \mathrm{Grp}$$
28	4 27	mp1i	$$⊢\top \to P\in \mathrm{Grp}$$
29		reeff1o	$$⊢\left({\exp \upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}$$
30		f1of	$$⊢\left({\exp \upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}\to \left({\exp \upharpoonright }_{ℝ}\right):ℝ⟶{ℝ}^{+}$$
31	29 30	mp1i	$$⊢\top \to \left({\exp \upharpoonright }_{ℝ}\right):ℝ⟶{ℝ}^{+}$$
32		recn	$$⊢x\in ℝ\to x\in ℂ$$
33		recn	$$⊢y\in ℝ\to y\in ℂ$$
34		efadd	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to {\mathrm{e}}^{x+y}={\mathrm{e}}^x{\mathrm{e}}^y$$
35	32 33 34	syl2an	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to {\mathrm{e}}^{x+y}={\mathrm{e}}^x{\mathrm{e}}^y$$
36		readdcl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+y\in ℝ$$
37	36	fvresd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left({\exp \upharpoonright }_{ℝ}\right)\left(x+y\right)={\mathrm{e}}^{x+y}$$
38		fvres	$$⊢x\in ℝ\to \left({\exp \upharpoonright }_{ℝ}\right)\left(x\right)={\mathrm{e}}^x$$
39		fvres	$$⊢y\in ℝ\to \left({\exp \upharpoonright }_{ℝ}\right)\left(y\right)={\mathrm{e}}^y$$
40	38 39	oveqan12d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left({\exp \upharpoonright }_{ℝ}\right)\left(x\right)\left({\exp \upharpoonright }_{ℝ}\right)\left(y\right)={\mathrm{e}}^x{\mathrm{e}}^y$$
41	35 37 40	3eqtr4d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left({\exp \upharpoonright }_{ℝ}\right)\left(x+y\right)=\left({\exp \upharpoonright }_{ℝ}\right)\left(x\right)\left({\exp \upharpoonright }_{ℝ}\right)\left(y\right)$$
42	41	adantl	$$⊢\left(\top \wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \left({\exp \upharpoonright }_{ℝ}\right)\left(x+y\right)=\left({\exp \upharpoonright }_{ℝ}\right)\left(x\right)\left({\exp \upharpoonright }_{ℝ}\right)\left(y\right)$$
43	2 13 14 19 26 28 31 42	isghmd	$$⊢\top \to {\exp \upharpoonright }_{ℝ}\in \left({ℝ}_{\mathrm{fld}}\mathrm{GrpHom}P\right)$$
44	43	mptru	$$⊢{\exp \upharpoonright }_{ℝ}\in \left({ℝ}_{\mathrm{fld}}\mathrm{GrpHom}P\right)$$
45	2 13	isgim	$$⊢{\exp \upharpoonright }_{ℝ}\in \left({ℝ}_{\mathrm{fld}}\mathrm{GrpIso}P\right)\leftrightarrow \left({\exp \upharpoonright }_{ℝ}\in \left({ℝ}_{\mathrm{fld}}\mathrm{GrpHom}P\right)\wedge \left({\exp \upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}\right)$$
46	44 29 45	mpbir2an	$$⊢{\exp \upharpoonright }_{ℝ}\in \left({ℝ}_{\mathrm{fld}}\mathrm{GrpIso}P\right)$$