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	$⊢ F = (x \in X ⟼ e^{A x})$
	efabl.2	$⊢ G = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ran F$
	efabl.3	$⊢ φ \to A \in ℂ$
	efabl.4	$⊢ φ \to X \in SubGrp (ℂ_{fld})$
Assertion	efsubm	$⊢ φ \to ran F \in SubMnd ({mulGrp}_{ℂ_{fld}})$

Proof

Step	Hyp	Ref	Expression
1		efabl.1	$⊢ F = (x \in X ⟼ e^{A x})$
2		efabl.2	$⊢ G = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ran F$
3		efabl.3	$⊢ φ \to A \in ℂ$
4		efabl.4	$⊢ φ \to X \in SubGrp (ℂ_{fld})$
5		eff	$⊢ \exp : ℂ ⟶ ℂ$
6	5	a1i	$⊢ (φ \land x \in X) \to \exp : ℂ ⟶ ℂ$
7	3	adantr	$⊢ (φ \land x \in X) \to A \in ℂ$
8		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
9	8	subgss	$⊢ X \in SubGrp (ℂ_{fld}) \to X \subseteq ℂ$
10	4 9	syl	$⊢ φ \to X \subseteq ℂ$
11	10	sselda	$⊢ (φ \land x \in X) \to x \in ℂ$
12	7 11	mulcld	$⊢ (φ \land x \in X) \to A x \in ℂ$
13	6 12	ffvelrnd	$⊢ (φ \land x \in X) \to e^{A x} \in ℂ$
14	13	ralrimiva	$⊢ φ \to \forall x \in X e^{A x} \in ℂ$
15	1	rnmptss	$⊢ \forall x \in X e^{A x} \in ℂ \to ran F \subseteq ℂ$
16	14 15	syl	$⊢ φ \to ran F \subseteq ℂ$
17	3	mul01d	$⊢ φ \to A \cdot 0 = 0$
18	17	fveq2d	$⊢ φ \to e^{A \cdot 0} = e^{0}$
19		ef0	$⊢ e^{0} = 1$
20	18 19	syl6eq	$⊢ φ \to e^{A \cdot 0} = 1$
21		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
22	21	subg0cl	$⊢ X \in SubGrp (ℂ_{fld}) \to 0 \in X$
23	4 22	syl	$⊢ φ \to 0 \in X$
24		fvex	$⊢ e^{A \cdot 0} \in V$
25		oveq2	$⊢ x = 0 \to A x = A \cdot 0$
26	25	fveq2d	$⊢ x = 0 \to e^{A x} = e^{A \cdot 0}$
27	1 26	elrnmpt1s	$⊢ (0 \in X \land e^{A \cdot 0} \in V) \to e^{A \cdot 0} \in ran F$
28	23 24 27	sylancl	$⊢ φ \to e^{A \cdot 0} \in ran F$
29	20 28	eqeltrrd	$⊢ φ \to 1 \in ran F$
30	1 2 3 4	efabl	$⊢ φ \to G \in Abel$
31		ablgrp	$⊢ G \in Abel \to G \in Grp$
32	30 31	syl	$⊢ φ \to G \in Grp$
33	32	3ad2ant1	$⊢ (φ \land x \in ran F \land y \in ran F) \to G \in Grp$
34		simp2	$⊢ (φ \land x \in ran F \land y \in ran F) \to x \in ran F$
35		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
36	35 8	mgpbas	$⊢ ℂ = {Base}_{{mulGrp}_{ℂ_{fld}}}$
37	2 36	ressbas2	$⊢ ran F \subseteq ℂ \to ran F = {Base}_{G}$
38	16 37	syl	$⊢ φ \to ran F = {Base}_{G}$
39	38	3ad2ant1	$⊢ (φ \land x \in ran F \land y \in ran F) \to ran F = {Base}_{G}$
40	34 39	eleqtrd	$⊢ (φ \land x \in ran F \land y \in ran F) \to x \in {Base}_{G}$
41		simp3	$⊢ (φ \land x \in ran F \land y \in ran F) \to y \in ran F$
42	41 39	eleqtrd	$⊢ (φ \land x \in ran F \land y \in ran F) \to y \in {Base}_{G}$
43		eqid	$⊢ {Base}_{G} = {Base}_{G}$
44		eqid	$⊢ +_{G} = +_{G}$
45	43 44	grpcl	$⊢ (G \in Grp \land x \in {Base}_{G} \land y \in {Base}_{G}) \to x +_{G} y \in {Base}_{G}$
46	33 40 42 45	syl3anc	$⊢ (φ \land x \in ran F \land y \in ran F) \to x +_{G} y \in {Base}_{G}$
47	4	mptexd	$⊢ φ \to (x \in X ⟼ e^{A x}) \in V$
48	1 47	eqeltrid	$⊢ φ \to F \in V$
49		rnexg	$⊢ F \in V \to ran F \in V$
50		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
51	35 50	mgpplusg	$⊢ \times = +_{{mulGrp}_{ℂ_{fld}}}$
52	2 51	ressplusg	$⊢ ran F \in V \to \times = +_{G}$
53	48 49 52	3syl	$⊢ φ \to \times = +_{G}$
54	53	3ad2ant1	$⊢ (φ \land x \in ran F \land y \in ran F) \to \times = +_{G}$
55	54	oveqd	$⊢ (φ \land x \in ran F \land y \in ran F) \to x y = x +_{G} y$
56	46 55 39	3eltr4d	$⊢ (φ \land x \in ran F \land y \in ran F) \to x y \in ran F$
57	56	3expb	$⊢ (φ \land (x \in ran F \land y \in ran F)) \to x y \in ran F$
58	57	ralrimivva	$⊢ φ \to \forall x \in ran F \forall y \in ran F x y \in ran F$
59		cnring	$⊢ ℂ_{fld} \in Ring$
60	35	ringmgp	$⊢ ℂ_{fld} \in Ring \to {mulGrp}_{ℂ_{fld}} \in Mnd$
61		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
62	35 61	ringidval	$⊢ 1 = 0_{{mulGrp}_{ℂ_{fld}}}$
63	36 62 51	issubm	$⊢ {mulGrp}_{ℂ_{fld}} \in Mnd \to (ran F \in SubMnd ({mulGrp}_{ℂ_{fld}}) \leftrightarrow (ran F \subseteq ℂ \land 1 \in ran F \land \forall x \in ran F \forall y \in ran F x y \in ran F))$
64	59 60 63	mp2b	$⊢ ran F \in SubMnd ({mulGrp}_{ℂ_{fld}}) \leftrightarrow (ran F \subseteq ℂ \land 1 \in ran F \land \forall x \in ran F \forall y \in ran F x y \in ran F)$
65	16 29 58 64	syl3anbrc	$⊢ φ \to ran F \in SubMnd ({mulGrp}_{ℂ_{fld}})$

Metamath Proof Explorer

Theorem efsubm

Proof