Theorem efabl

Description: The image of a subgroup of the group + , under the exponential function of a scaled complex number, is an Abelian group. (Contributed by Paul Chapman, 25-Apr-2008) (Revised by Mario Carneiro, 12-May-2014) (Revised by Thierry Arnoux, 26-Jan-2020)

	Ref	Expression
Hypotheses	efabl.1	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( exp ‘ ( 𝐴 · 𝑥 ) ) )
	efabl.2	⊢ 𝐺 = ( ( mulGrp ‘ ℂfld ) ↾s ran 𝐹 )
	efabl.3	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	efabl.4	⊢ ( 𝜑 → 𝑋 ∈ ( SubGrp ‘ ℂfld ) )
Assertion	efabl	⊢ ( 𝜑 → 𝐺 ∈ Abel )

Proof

Step	Hyp	Ref	Expression
1		efabl.1	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( exp ‘ ( 𝐴 · 𝑥 ) ) )
2		efabl.2	⊢ 𝐺 = ( ( mulGrp ‘ ℂfld ) ↾s ran 𝐹 )
3		efabl.3	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4		efabl.4	⊢ ( 𝜑 → 𝑋 ∈ ( SubGrp ‘ ℂfld ) )
5		eqid	⊢ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) = ( Base ‘ ( ℂfld ↾s 𝑋 ) )
6		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7		eqid	⊢ ( +g ‘ ( ℂfld ↾s 𝑋 ) ) = ( +g ‘ ( ℂfld ↾s 𝑋 ) )
8		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
9		simp1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ) → 𝜑 )
10		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ) → 𝑥 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) )
11		eqid	⊢ ( ℂfld ↾s 𝑋 ) = ( ℂfld ↾s 𝑋 )
12	11	subgbas	⊢ ( 𝑋 ∈ ( SubGrp ‘ ℂfld ) → 𝑋 = ( Base ‘ ( ℂfld ↾s 𝑋 ) ) )
13	4 12	syl	⊢ ( 𝜑 → 𝑋 = ( Base ‘ ( ℂfld ↾s 𝑋 ) ) )
14	13	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ) → 𝑋 = ( Base ‘ ( ℂfld ↾s 𝑋 ) ) )
15	10 14	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ) → 𝑥 ∈ 𝑋 )
16		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ) → 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) )
17	16 14	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ) → 𝑦 ∈ 𝑋 )
18	3 4	jca	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) )
19	1	efgh	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) )
20	18 19	syl3an1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) )
21		cnfldadd	⊢ + = ( +g ‘ ℂfld )
22	11 21	ressplusg	⊢ ( 𝑋 ∈ ( SubGrp ‘ ℂfld ) → + = ( +g ‘ ( ℂfld ↾s 𝑋 ) ) )
23	4 22	syl	⊢ ( 𝜑 → + = ( +g ‘ ( ℂfld ↾s 𝑋 ) ) )
24	23	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → + = ( +g ‘ ( ℂfld ↾s 𝑋 ) ) )
25	24	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ ( ℂfld ↾s 𝑋 ) ) 𝑦 ) )
26	25	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( ℂfld ↾s 𝑋 ) ) 𝑦 ) ) )
27		mptexg	⊢ ( 𝑋 ∈ ( SubGrp ‘ ℂfld ) → ( 𝑥 ∈ 𝑋 ↦ ( exp ‘ ( 𝐴 · 𝑥 ) ) ) ∈ V )
28	1 27	eqeltrid	⊢ ( 𝑋 ∈ ( SubGrp ‘ ℂfld ) → 𝐹 ∈ V )
29		rnexg	⊢ ( 𝐹 ∈ V → ran 𝐹 ∈ V )
30	4 28 29	3syl	⊢ ( 𝜑 → ran 𝐹 ∈ V )
31		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
32		cnfldmul	⊢ · = ( .r ‘ ℂfld )
33	31 32	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
34	2 33	ressplusg	⊢ ( ran 𝐹 ∈ V → · = ( +g ‘ 𝐺 ) )
35	30 34	syl	⊢ ( 𝜑 → · = ( +g ‘ 𝐺 ) )
36	35	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → · = ( +g ‘ 𝐺 ) )
37	36	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑦 ) ) )
38	20 26 37	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( ℂfld ↾s 𝑋 ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑦 ) ) )
39	9 15 17 38	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( ℂfld ↾s 𝑋 ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑦 ) ) )
40		fvex	⊢ ( exp ‘ ( 𝐴 · 𝑥 ) ) ∈ V
41	40 1	fnmpti	⊢ 𝐹 Fn 𝑋
42		dffn4	⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 –onto→ ran 𝐹 )
43	41 42	mpbi	⊢ 𝐹 : 𝑋 –onto→ ran 𝐹
44		eqidd	⊢ ( 𝜑 → 𝐹 = 𝐹 )
45		eff	⊢ exp : ℂ ⟶ ℂ
46	45	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → exp : ℂ ⟶ ℂ )
47	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
48		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
49	48	subgss	⊢ ( 𝑋 ∈ ( SubGrp ‘ ℂfld ) → 𝑋 ⊆ ℂ )
50	4 49	syl	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
51	50	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ℂ )
52	47 51	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
53	46 52	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( exp ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ )
54	53	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( exp ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ )
55	1	rnmptss	⊢ ( ∀ 𝑥 ∈ 𝑋 ( exp ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ → ran 𝐹 ⊆ ℂ )
56	31 48	mgpbas	⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
57	2 56	ressbas2	⊢ ( ran 𝐹 ⊆ ℂ → ran 𝐹 = ( Base ‘ 𝐺 ) )
58	54 55 57	3syl	⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐺 ) )
59	44 13 58	foeq123d	⊢ ( 𝜑 → ( 𝐹 : 𝑋 –onto→ ran 𝐹 ↔ 𝐹 : ( Base ‘ ( ℂfld ↾s 𝑋 ) ) –onto→ ( Base ‘ 𝐺 ) ) )
60	43 59	mpbii	⊢ ( 𝜑 → 𝐹 : ( Base ‘ ( ℂfld ↾s 𝑋 ) ) –onto→ ( Base ‘ 𝐺 ) )
61		cnring	⊢ ℂfld ∈ Ring
62		ringabl	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Abel )
63	61 62	ax-mp	⊢ ℂfld ∈ Abel
64	11	subgabl	⊢ ( ( ℂfld ∈ Abel ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) → ( ℂfld ↾s 𝑋 ) ∈ Abel )
65	63 4 64	sylancr	⊢ ( 𝜑 → ( ℂfld ↾s 𝑋 ) ∈ Abel )
66	5 6 7 8 39 60 65	ghmabl	⊢ ( 𝜑 → 𝐺 ∈ Abel )