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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 reefgim.1 ⊢ 𝑃 = ( ( mulGrp ‘ ℂfld ) ↾s ℝ+ )
2 rebase ⊢ ℝ = ( Base ‘ ℝfld )
3 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
4 3 rpmsubg ⊢ ℝ+ ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
5 cnex ⊢ ℂ ∈ V
6 5 difexi ⊢ ( ℂ ∖ { 0 } ) ∈ V
7 rpcndif0 ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ( ℂ ∖ { 0 } ) )
8 7 ssriv ⊢ ℝ+ ⊆ ( ℂ ∖ { 0 } )
9 ressabs ⊢ ( ( ( ℂ ∖ { 0 } ) ∈ V ∧ ℝ+ ⊆ ( ℂ ∖ { 0 } ) ) → ( ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ↾s ℝ+ ) = ( ( mulGrp ‘ ℂfld ) ↾s ℝ+ ) )
10 6 8 9 mp2an ⊢ ( ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ↾s ℝ+ ) = ( ( mulGrp ‘ ℂfld ) ↾s ℝ+ )
11 1 10 eqtr4i ⊢ 𝑃 = ( ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ↾s ℝ+ )
12 11 subgbas ⊢ ( ℝ+ ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) → ℝ+ = ( Base ‘ 𝑃 ) )
13 4 12 ax-mp ⊢ ℝ+ = ( Base ‘ 𝑃 )
14 replusg ⊢ + = ( +g ‘ ℝfld )
15 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
16 cnfldmul ⊢ · = ( .r ‘ ℂfld )
17 15 16 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
18 1 17 ressplusg ⊢ ( ℝ+ ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) → · = ( +g ‘ 𝑃 ) )
19 4 18 ax-mp ⊢ · = ( +g ‘ 𝑃 )
20 resubdrg ⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
21 20 simpli ⊢ ℝ ∈ ( SubRing ‘ ℂfld )
22 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
23 22 subrgring ⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝfld ∈ Ring )
24 21 23 ax-mp ⊢ ℝfld ∈ Ring
25 ringgrp ⊢ ( ℝfld ∈ Ring → ℝfld ∈ Grp )
26 24 25 mp1i ⊢ ( ⊤ → ℝfld ∈ Grp )
27 11 subggrp ⊢ ( ℝ+ ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) → 𝑃 ∈ Grp )
28 4 27 mp1i ⊢ ( ⊤ → 𝑃 ∈ Grp )
29 reeff1o ⊢ ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+
30 f1of ⊢ ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ → ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ )
31 29 30 mp1i ⊢ ( ⊤ → ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ )
32 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
33 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
34 efadd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( exp ‘ ( 𝑥 + 𝑦 ) ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑦 ) ) )
35 32 33 34 syl2an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( exp ‘ ( 𝑥 + 𝑦 ) ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑦 ) ) )
36 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
37 36 fvresd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( exp ↾ ℝ ) ‘ ( 𝑥 + 𝑦 ) ) = ( exp ‘ ( 𝑥 + 𝑦 ) ) )
38 fvres ⊢ ( 𝑥 ∈ ℝ → ( ( exp ↾ ℝ ) ‘ 𝑥 ) = ( exp ‘ 𝑥 ) )
39 fvres ⊢ ( 𝑦 ∈ ℝ → ( ( exp ↾ ℝ ) ‘ 𝑦 ) = ( exp ‘ 𝑦 ) )
40 38 39 oveqan12d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( exp ↾ ℝ ) ‘ 𝑥 ) · ( ( exp ↾ ℝ ) ‘ 𝑦 ) ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ 𝑦 ) ) )
41 35 37 40 3eqtr4d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( exp ↾ ℝ ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ( exp ↾ ℝ ) ‘ 𝑥 ) · ( ( exp ↾ ℝ ) ‘ 𝑦 ) ) )
42 41 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( exp ↾ ℝ ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ( exp ↾ ℝ ) ‘ 𝑥 ) · ( ( exp ↾ ℝ ) ‘ 𝑦 ) ) )
43 2 13 14 19 26 28 31 42 isghmd ⊢ ( ⊤ → ( exp ↾ ℝ ) ∈ ( ℝfld GrpHom 𝑃 ) )
44 43 mptru ⊢ ( exp ↾ ℝ ) ∈ ( ℝfld GrpHom 𝑃 )
45 2 13 isgim ⊢ ( ( exp ↾ ℝ ) ∈ ( ℝfld GrpIso 𝑃 ) ↔ ( ( exp ↾ ℝ ) ∈ ( ℝfld GrpHom 𝑃 ) ∧ ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ ) )
46 44 29 45 mpbir2an ⊢ ( exp ↾ ℝ ) ∈ ( ℝfld GrpIso 𝑃 )