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 𝑃 )