This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℝ^{+}$
	Assertion	reloggim	$⊢ {log ↾}_{ℝ^{+}} \in (P GrpIso ℝ_{fld})$

Proof

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