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 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 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 )