Theorem reloggim

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

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

Proof

Step	Hyp	Ref	Expression
1		reloggim.1	$$⊢P={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}{ℝ}^{+}$$
2		dfrelog	$$⊢{log\upharpoonright }_{{ℝ}^{+}}={\left({\exp \upharpoonright }_{ℝ}\right)}^{-1}$$
3	1	reefgim	$$⊢{\exp \upharpoonright }_{ℝ}\in \left({ℝ}_{\mathrm{fld}}\mathrm{GrpIso}P\right)$$
4		gimcnv	$$⊢{\exp \upharpoonright }_{ℝ}\in \left({ℝ}_{\mathrm{fld}}\mathrm{GrpIso}P\right)\to {\left({\exp \upharpoonright }_{ℝ}\right)}^{-1}\in \left(P\mathrm{GrpIso}{ℝ}_{\mathrm{fld}}\right)$$
5	3 4	ax-mp	$$⊢{\left({\exp \upharpoonright }_{ℝ}\right)}^{-1}\in \left(P\mathrm{GrpIso}{ℝ}_{\mathrm{fld}}\right)$$
6	2 5	eqeltri	$$⊢{log\upharpoonright }_{{ℝ}^{+}}\in \left(P\mathrm{GrpIso}{ℝ}_{\mathrm{fld}}\right)$$