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	$$⊢F=\left(x\in X⟼{\mathrm{e}}^{Ax}\right)$$
	efabl.2	$$⊢G={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathrm{ran}F$$
	efabl.3	$$⊢\phi \to A\in ℂ$$
	efabl.4	$$⊢\phi \to X\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	efabl	$$⊢\phi \to G\in \mathrm{Abel}$$

Proof

Step	Hyp	Ref	Expression
1		efabl.1	$$⊢F=\left(x\in X⟼{\mathrm{e}}^{Ax}\right)$$
2		efabl.2	$$⊢G={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathrm{ran}F$$
3		efabl.3	$$⊢\phi \to A\in ℂ$$
4		efabl.4	$$⊢\phi \to X\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
5		eqid	$$⊢{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}$$
6		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
7		eqid	$$⊢{+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}$$
8		eqid	$$⊢{+}_G={+}_G$$
9		simp1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\wedge y\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\right)\to \phi$$
10		simp2	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\wedge y\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\right)\to x\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}$$
11		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X$$
12	11	subgbas	$$⊢X\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to X={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}$$
13	4 12	syl	$$⊢\phi \to X={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}$$
14	13	3ad2ant1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\wedge y\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\right)\to X={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}$$
15	10 14	eleqtrrd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\wedge y\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\right)\to x\in X$$
16		simp3	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\wedge y\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\right)\to y\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}$$
17	16 14	eleqtrrd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\wedge y\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\right)\to y\in X$$
18	3 4	jca	$$⊢\phi \to \left(A\in ℂ\wedge X\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
19	1	efgh	$$⊢\left(\left(A\in ℂ\wedge X\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge x\in X\wedge y\in X\right)\to F\left(x+y\right)=F\left(x\right)F\left(y\right)$$
20	18 19	syl3an1	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to F\left(x+y\right)=F\left(x\right)F\left(y\right)$$
21		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
22	11 21	ressplusg	$$⊢X\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to +={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}$$
23	4 22	syl	$$⊢\phi \to +={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}$$
24	23	3ad2ant1	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to +={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}$$
25	24	oveqd	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to x+y=x{+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}y$$
26	25	fveq2d	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to F\left(x+y\right)=F\left(x{+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}y\right)$$
27		mptexg	$$⊢X\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to \left(x\in X⟼{\mathrm{e}}^{Ax}\right)\in \mathrm{V}$$
28	1 27	eqeltrid	$$⊢X\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to F\in \mathrm{V}$$
29		rnexg	$$⊢F\in \mathrm{V}\to \mathrm{ran}F\in \mathrm{V}$$
30		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
31		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
32	30 31	mgpplusg	$$⊢\times ={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
33	2 32	ressplusg	$$⊢\mathrm{ran}F\in \mathrm{V}\to \times ={+}_G$$
34	4 28 29 33	4syl	$$⊢\phi \to \times ={+}_G$$
35	34	3ad2ant1	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to \times ={+}_G$$
36	35	oveqd	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to F\left(x\right)F\left(y\right)=F\left(x\right){+}_{G}F\left(y\right)$$
37	20 26 36	3eqtr3d	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to F\left(x{+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}y\right)=F\left(x\right){+}_{G}F\left(y\right)$$
38	9 15 17 37	syl3anc	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\wedge y\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\right)\to F\left(x{+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}y\right)=F\left(x\right){+}_{G}F\left(y\right)$$
39		fvex	$$⊢{\mathrm{e}}^{Ax}\in \mathrm{V}$$
40	39 1	fnmpti	$$⊢FFnX$$
41		dffn4	$$⊢FFnX\leftrightarrow F:X\underset{onto}{⟶}\mathrm{ran}F$$
42	40 41	mpbi	$$⊢F:X\underset{onto}{⟶}\mathrm{ran}F$$
43		eqidd	$$⊢\phi \to F=F$$
44		eff	$$⊢\exp :ℂ⟶ℂ$$
45	44	a1i	$$⊢\left(\phi \wedge x\in X\right)\to \exp :ℂ⟶ℂ$$
46	3	adantr	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
47		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
48	47	subgss	$$⊢X\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to X\subseteq ℂ$$
49	4 48	syl	$$⊢\phi \to X\subseteq ℂ$$
50	49	sselda	$$⊢\left(\phi \wedge x\in X\right)\to x\in ℂ$$
51	46 50	mulcld	$$⊢\left(\phi \wedge x\in X\right)\to Ax\in ℂ$$
52	45 51	ffvelcdmd	$$⊢\left(\phi \wedge x\in X\right)\to {\mathrm{e}}^{Ax}\in ℂ$$
53	52	ralrimiva	$$⊢\phi \to \forall x\in X{\mathrm{e}}^{Ax}\in ℂ$$
54	1	rnmptss	$$⊢\forall x\in X{\mathrm{e}}^{Ax}\in ℂ\to \mathrm{ran}F\subseteq ℂ$$
55	30 47	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
56	2 55	ressbas2	$$⊢\mathrm{ran}F\subseteq ℂ\to \mathrm{ran}F={\mathrm{Base}}_G$$
57	53 54 56	3syl	$$⊢\phi \to \mathrm{ran}F={\mathrm{Base}}_G$$
58	43 13 57	foeq123d	$$⊢\phi \to \left(F:X\underset{onto}{⟶}\mathrm{ran}F\leftrightarrow F:{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\underset{onto}{⟶}{\mathrm{Base}}_G\right)$$
59	42 58	mpbii	$$⊢\phi \to F:{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\underset{onto}{⟶}{\mathrm{Base}}_G$$
60		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
61		ringabl	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Abel}$$
62	60 61	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Abel}$$
63	11	subgabl	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Abel}\wedge X\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\in \mathrm{Abel}$$
64	62 4 63	sylancr	$$⊢\phi \to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\in \mathrm{Abel}$$
65	5 6 7 8 38 59 64	ghmabl	$$⊢\phi \to G\in \mathrm{Abel}$$