Metamath Proof Explorer

Theorem efsubm

Description: The image of a subgroup of the group + , under the exponential function of a scaled complex number is a submonoid of the multiplicative group of CCfld . (Contributed 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 efsubm ( 𝜑 → ran 𝐹 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )

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 eff ⊢ exp : ℂ ⟶ ℂ
6 5 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → exp : ℂ ⟶ ℂ )
7 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
8 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
9 8 subgss ⊢ ( 𝑋 ∈ ( SubGrp ‘ ℂfld ) → 𝑋 ⊆ ℂ )
10 4 9 syl ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
11 10 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ℂ )
12 7 11 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
13 6 12 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( exp ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ )
14 13 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( exp ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ )
15 1 rnmptss ⊢ ( ∀ 𝑥 ∈ 𝑋 ( exp ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ → ran 𝐹 ⊆ ℂ )
16 14 15 syl ⊢ ( 𝜑 → ran 𝐹 ⊆ ℂ )
17 3 mul01d ⊢ ( 𝜑 → ( 𝐴 · 0 ) = 0 )
18 17 fveq2d ⊢ ( 𝜑 → ( exp ‘ ( 𝐴 · 0 ) ) = ( exp ‘ 0 ) )
19 ef0 ⊢ ( exp ‘ 0 ) = 1
20 18 19 eqtrdi ⊢ ( 𝜑 → ( exp ‘ ( 𝐴 · 0 ) ) = 1 )
21 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
22 21 subg0cl ⊢ ( 𝑋 ∈ ( SubGrp ‘ ℂfld ) → 0 ∈ 𝑋 )
23 4 22 syl ⊢ ( 𝜑 → 0 ∈ 𝑋 )
24 fvex ⊢ ( exp ‘ ( 𝐴 · 0 ) ) ∈ V
25 oveq2 ⊢ ( 𝑥 = 0 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 0 ) )
26 25 fveq2d ⊢ ( 𝑥 = 0 → ( exp ‘ ( 𝐴 · 𝑥 ) ) = ( exp ‘ ( 𝐴 · 0 ) ) )
27 1 26 elrnmpt1s ⊢ ( ( 0 ∈ 𝑋 ∧ ( exp ‘ ( 𝐴 · 0 ) ) ∈ V ) → ( exp ‘ ( 𝐴 · 0 ) ) ∈ ran 𝐹 )
28 23 24 27 sylancl ⊢ ( 𝜑 → ( exp ‘ ( 𝐴 · 0 ) ) ∈ ran 𝐹 )
29 20 28 eqeltrrd ⊢ ( 𝜑 → 1 ∈ ran 𝐹 )
30 1 2 3 4 efabl ⊢ ( 𝜑 → 𝐺 ∈ Abel )
31 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
32 30 31 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
33 32 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) → 𝐺 ∈ Grp )
34 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) → 𝑥 ∈ ran 𝐹 )
35 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
36 35 8 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
37 2 36 ressbas2 ⊢ ( ran 𝐹 ⊆ ℂ → ran 𝐹 = ( Base ‘ 𝐺 ) )
38 16 37 syl ⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐺 ) )
39 38 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) → ran 𝐹 = ( Base ‘ 𝐺 ) )
40 34 39 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
41 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ran 𝐹 )
42 41 39 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
43 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
44 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
45 43 44 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
46 33 40 42 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
47 4 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( exp ‘ ( 𝐴 · 𝑥 ) ) ) ∈ V )
48 1 47 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ V )
49 rnexg ⊢ ( 𝐹 ∈ V → ran 𝐹 ∈ V )
50 cnfldmul ⊢ · = ( .r ‘ ℂfld )
51 35 50 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
52 2 51 ressplusg ⊢ ( ran 𝐹 ∈ V → · = ( +g ‘ 𝐺 ) )
53 48 49 52 3syl ⊢ ( 𝜑 → · = ( +g ‘ 𝐺 ) )
54 53 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) → · = ( +g ‘ 𝐺 ) )
55 54 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑥 · 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
56 46 55 39 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑥 · 𝑦 ) ∈ ran 𝐹 )
57 56 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹 ) ) → ( 𝑥 · 𝑦 ) ∈ ran 𝐹 )
58 57 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 · 𝑦 ) ∈ ran 𝐹 )
59 cnring ⊢ ℂfld ∈ Ring
60 35 ringmgp ⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
61 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
62 35 61 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
63 36 62 51 issubm ⊢ ( ( mulGrp ‘ ℂfld ) ∈ Mnd → ( ran 𝐹 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ↔ ( ran 𝐹 ⊆ ℂ ∧ 1 ∈ ran 𝐹 ∧ ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 · 𝑦 ) ∈ ran 𝐹 ) ) )
64 59 60 63 mp2b ⊢ ( ran 𝐹 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ↔ ( ran 𝐹 ⊆ ℂ ∧ 1 ∈ ran 𝐹 ∧ ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 ( 𝑥 · 𝑦 ) ∈ ran 𝐹 ) )
65 16 29 58 64 syl3anbrc ⊢ ( 𝜑 → ran 𝐹 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )