Metamath Proof Explorer

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 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
31 cnfldmul ⊢ · = ( .r ‘ ℂfld )
32 30 31 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
33 2 32 ressplusg ⊢ ( ran 𝐹 ∈ V → · = ( +g ‘ 𝐺 ) )
34 4 28 29 33 4syl ⊢ ( 𝜑 → · = ( +g ‘ 𝐺 ) )
35 34 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → · = ( +g ‘ 𝐺 ) )
36 35 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑦 ) ) )
37 20 26 36 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( ℂfld ↾s 𝑋 ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑦 ) ) )
38 9 15 17 37 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ∧ 𝑦 ∈ ( Base ‘ ( ℂfld ↾s 𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ ( ℂfld ↾s 𝑋 ) ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐹 ‘ 𝑦 ) ) )
39 fvex ⊢ ( exp ‘ ( 𝐴 · 𝑥 ) ) ∈ V
40 39 1 fnmpti ⊢ 𝐹 Fn 𝑋
41 dffn4 ⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 –onto→ ran 𝐹 )
42 40 41 mpbi ⊢ 𝐹 : 𝑋 –onto→ ran 𝐹
43 eqidd ⊢ ( 𝜑 → 𝐹 = 𝐹 )
44 eff ⊢ exp : ℂ ⟶ ℂ
45 44 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → exp : ℂ ⟶ ℂ )
46 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
47 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
48 47 subgss ⊢ ( 𝑋 ∈ ( SubGrp ‘ ℂfld ) → 𝑋 ⊆ ℂ )
49 4 48 syl ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
50 49 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ℂ )
51 46 50 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
52 45 51 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( exp ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ )
53 52 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( exp ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ )
54 1 rnmptss ⊢ ( ∀ 𝑥 ∈ 𝑋 ( exp ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ → ran 𝐹 ⊆ ℂ )
55 30 47 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
56 2 55 ressbas2 ⊢ ( ran 𝐹 ⊆ ℂ → ran 𝐹 = ( Base ‘ 𝐺 ) )
57 53 54 56 3syl ⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐺 ) )
58 43 13 57 foeq123d ⊢ ( 𝜑 → ( 𝐹 : 𝑋 –onto→ ran 𝐹 ↔ 𝐹 : ( Base ‘ ( ℂfld ↾s 𝑋 ) ) –onto→ ( Base ‘ 𝐺 ) ) )
59 42 58 mpbii ⊢ ( 𝜑 → 𝐹 : ( Base ‘ ( ℂfld ↾s 𝑋 ) ) –onto→ ( Base ‘ 𝐺 ) )
60 cnring ⊢ ℂfld ∈ Ring
61 ringabl ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Abel )
62 60 61 ax-mp ⊢ ℂfld ∈ Abel
63 11 subgabl ⊢ ( ( ℂfld ∈ Abel ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) → ( ℂfld ↾s 𝑋 ) ∈ Abel )
64 62 4 63 sylancr ⊢ ( 𝜑 → ( ℂfld ↾s 𝑋 ) ∈ Abel )
65 5 6 7 8 38 59 64 ghmabl ⊢ ( 𝜑 → 𝐺 ∈ Abel )