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	⊢ 𝑃 = ( ( mulGrp ‘ ℂfld ) ↾s ℝ+ )
Assertion	reloggim	⊢ ( log ↾ ℝ+ ) ∈ ( 𝑃 GrpIso ℝfld )

Proof

Step	Hyp	Ref	Expression
1		reloggim.1	⊢ 𝑃 = ( ( mulGrp ‘ ℂfld ) ↾s ℝ+ )
2		dfrelog	⊢ ( log ↾ ℝ+ ) = ◡ ( exp ↾ ℝ )
3	1	reefgim	⊢ ( exp ↾ ℝ ) ∈ ( ℝfld GrpIso 𝑃 )
4		gimcnv	⊢ ( ( exp ↾ ℝ ) ∈ ( ℝfld GrpIso 𝑃 ) → ◡ ( exp ↾ ℝ ) ∈ ( 𝑃 GrpIso ℝfld ) )
5	3 4	ax-mp	⊢ ◡ ( exp ↾ ℝ ) ∈ ( 𝑃 GrpIso ℝfld )
6	2 5	eqeltri	⊢ ( log ↾ ℝ+ ) ∈ ( 𝑃 GrpIso ℝfld )