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	4 28 29	3syl	$$⊢\phi \to \mathrm{ran}F\in \mathrm{V}$$
31		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
32		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
33	31 32	mgpplusg	$$⊢\times ={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
34	2 33	ressplusg	$$⊢\mathrm{ran}F\in \mathrm{V}\to \times ={+}_G$$
35	30 34	syl	$$⊢\phi \to \times ={+}_G$$
36	35	3ad2ant1	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to \times ={+}_G$$
37	36	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)$$
38	20 26 37	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)$$
39	9 15 17 38	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)$$
40		fvex	$$⊢{\mathrm{e}}^{Ax}\in \mathrm{V}$$
41	40 1	fnmpti	$$⊢FFnX$$
42		dffn4	$$⊢FFnX\leftrightarrow F:X\underset{onto}{⟶}\mathrm{ran}F$$
43	41 42	mpbi	$$⊢F:X\underset{onto}{⟶}\mathrm{ran}F$$
44		eqidd	$$⊢\phi \to F=F$$
45		eff	$$⊢\exp :ℂ⟶ℂ$$
46	45	a1i	$$⊢\left(\phi \wedge x\in X\right)\to \exp :ℂ⟶ℂ$$
47	3	adantr	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
48		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
49	48	subgss	$$⊢X\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to X\subseteq ℂ$$
50	4 49	syl	$$⊢\phi \to X\subseteq ℂ$$
51	50	sselda	$$⊢\left(\phi \wedge x\in X\right)\to x\in ℂ$$
52	47 51	mulcld	$$⊢\left(\phi \wedge x\in X\right)\to Ax\in ℂ$$
53	46 52	ffvelrnd	$$⊢\left(\phi \wedge x\in X\right)\to {\mathrm{e}}^{Ax}\in ℂ$$
54	53	ralrimiva	$$⊢\phi \to \forall x\in X{\mathrm{e}}^{Ax}\in ℂ$$
55	1	rnmptss	$$⊢\forall x\in X{\mathrm{e}}^{Ax}\in ℂ\to \mathrm{ran}F\subseteq ℂ$$
56	31 48	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
57	2 56	ressbas2	$$⊢\mathrm{ran}F\subseteq ℂ\to \mathrm{ran}F={\mathrm{Base}}_G$$
58	54 55 57	3syl	$$⊢\phi \to \mathrm{ran}F={\mathrm{Base}}_G$$
59	44 13 58	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)$$
60	43 59	mpbii	$$⊢\phi \to F:{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\right)}\underset{onto}{⟶}{\mathrm{Base}}_G$$
61		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
62		ringabl	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Abel}$$
63	61 62	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Abel}$$
64	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}$$
65	63 4 64	sylancr	$$⊢\phi \to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}X\in \mathrm{Abel}$$
66	5 6 7 8 39 60 65	ghmabl	$$⊢\phi \to G\in \mathrm{Abel}$$