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