Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  efabl Structured version   Unicode version

Theorem efabl 23495
 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.)
Hypotheses
Ref Expression
efabl.1
efabl.2 mulGrpflds
efabl.3
efabl.4 SubGrpfld
Assertion
Ref Expression
efabl
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem efabl
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2423 . 2 flds flds
2 eqid 2423 . 2
3 eqid 2423 . 2 flds flds
4 eqid 2423 . 2
5 simp1 1006 . . 3 flds flds
6 simp2 1007 . . . 4 flds flds flds
7 efabl.4 . . . . . 6 SubGrpfld
8 eqid 2423 . . . . . . 7 flds flds
98subgbas 16818 . . . . . 6 SubGrpfld flds
107, 9syl 17 . . . . 5 flds
11103ad2ant1 1027 . . . 4 flds flds flds
126, 11eleqtrrd 2514 . . 3 flds flds
13 simp3 1008 . . . 4 flds flds flds
1413, 11eleqtrrd 2514 . . 3 flds flds
15 efabl.3 . . . . . 6
1615, 7jca 535 . . . . 5 SubGrpfld
17 efabl.1 . . . . . 6
1817efgh 23486 . . . . 5 SubGrpfld
1916, 18syl3an1 1298 . . . 4
20 cnfldadd 18972 . . . . . . . . 9 fld
218, 20ressplusg 15236 . . . . . . . 8 SubGrpfld flds
227, 21syl 17 . . . . . . 7 flds
23223ad2ant1 1027 . . . . . 6 flds
2423oveqd 6321 . . . . 5 flds
2524fveq2d 5884 . . . 4 flds
26 mptexg 6149 . . . . . . . . 9 SubGrpfld
2717, 26syl5eqel 2515 . . . . . . . 8 SubGrpfld
28 rnexg 6738 . . . . . . . 8
297, 27, 283syl 18 . . . . . . 7
30 efabl.2 . . . . . . . 8 mulGrpflds
31 eqid 2423 . . . . . . . . 9 mulGrpfld mulGrpfld
32 cnfldmul 18973 . . . . . . . . 9 fld
3331, 32mgpplusg 17724 . . . . . . . 8 mulGrpfld
3430, 33ressplusg 15236 . . . . . . 7
3529, 34syl 17 . . . . . 6
36353ad2ant1 1027 . . . . 5
3736oveqd 6321 . . . 4
3819, 25, 373eqtr3d 2472 . . 3 flds
395, 12, 14, 38syl3anc 1265 . 2 flds flds flds
40 fvex 5890 . . . . 5
4140, 17fnmpti 5723 . . . 4
42 dffn4 5815 . . . 4
4341, 42mpbi 212 . . 3
44 eqidd 2424 . . . 4
45 eff 14133 . . . . . . . 8
4645a1i 11 . . . . . . 7
4715adantr 467 . . . . . . . 8
48 cnfldbas 18971 . . . . . . . . . . 11 fld
4948subgss 16815 . . . . . . . . . 10 SubGrpfld
507, 49syl 17 . . . . . . . . 9
5150sselda 3466 . . . . . . . 8
5247, 51mulcld 9669 . . . . . . 7
5346, 52ffvelrnd 6037 . . . . . 6
5453ralrimiva 2840 . . . . 5
5517rnmptss 6066 . . . . 5
5631, 48mgpbas 17726 . . . . . 6 mulGrpfld
5730, 56ressbas2 15177 . . . . 5
5854, 55, 573syl 18 . . . 4
5944, 10, 58foeq123d 5826 . . 3 flds
6043, 59mpbii 215 . 2 flds
61 cnring 18987 . . . 4 fld
62 ringabl 17807 . . . 4 fld fld
6361, 62ax-mp 5 . . 3 fld
648subgabl 17473 . . 3 fld SubGrpfld flds
6563, 7, 64sylancr 668 . 2 flds
661, 2, 3, 4, 39, 60, 65ghmabl 17470 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371   w3a 983   wceq 1438   wcel 1869  wral 2776  cvv 3082   wss 3438   cmpt 4481   crn 4853   wfn 5595  wf 5596  wfo 5598  cfv 5600  (class class class)co 6304  cc 9543   caddc 9548   cmul 9550  ce 14111  cbs 15118   ↾s cress 15119   cplusg 15187  SubGrpcsubg 16808  cabl 17428  mulGrpcmgp 17720  crg 17777  ℂfldccnfld 18967 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4535  ax-sep 4545  ax-nul 4554  ax-pow 4601  ax-pr 4659  ax-un 6596  ax-inf2 8154  ax-cnex 9601  ax-resscn 9602  ax-1cn 9603  ax-icn 9604  ax-addcl 9605  ax-addrcl 9606  ax-mulcl 9607  ax-mulrcl 9608  ax-mulcom 9609  ax-addass 9610  ax-mulass 9611  ax-distr 9612  ax-i2m1 9613  ax-1ne0 9614  ax-1rid 9615  ax-rnegex 9616  ax-rrecex 9617  ax-cnre 9618  ax-pre-lttri 9619  ax-pre-lttrn 9620  ax-pre-ltadd 9621  ax-pre-mulgt0 9622  ax-pre-sup 9623  ax-addf 9624  ax-mulf 9625 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3302  df-csb 3398  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-pss 3454  df-nul 3764  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4219  df-int 4255  df-iun 4300  df-br 4423  df-opab 4482  df-mpt 4483  df-tr 4518  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-se 4812  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-isom 5609  df-riota 6266  df-ov 6307  df-oprab 6308  df-mpt2 6309  df-om 6706  df-1st 6806  df-2nd 6807  df-wrecs 7038  df-recs 7100  df-rdg 7138  df-1o 7192  df-oadd 7196  df-er 7373  df-pm 7485  df-en 7580  df-dom 7581  df-sdom 7582  df-fin 7583  df-sup 7964  df-inf 7965  df-oi 8033  df-card 8380  df-pnf 9683  df-mnf 9684  df-xr 9685  df-ltxr 9686  df-le 9687  df-sub 9868  df-neg 9869  df-div 10276  df-nn 10616  df-2 10674  df-3 10675  df-4 10676  df-5 10677  df-6 10678  df-7 10679  df-8 10680  df-9 10681  df-10 10682  df-n0 10876  df-z 10944  df-dec 11058  df-uz 11166  df-rp 11309  df-ico 11647  df-fz 11791  df-fzo 11922  df-fl 12033  df-seq 12219  df-exp 12278  df-fac 12465  df-bc 12493  df-hash 12521  df-shft 13128  df-cj 13160  df-re 13161  df-im 13162  df-sqrt 13296  df-abs 13297  df-limsup 13523  df-clim 13549  df-rlim 13550  df-sum 13750  df-ef 14118  df-struct 15120  df-ndx 15121  df-slot 15122  df-base 15123  df-sets 15124  df-ress 15125  df-plusg 15200  df-mulr 15201  df-starv 15202  df-tset 15206  df-ple 15207  df-ds 15209  df-unif 15210  df-0g 15337  df-mgm 16485  df-sgrp 16524  df-mnd 16534  df-grp 16670  df-minusg 16671  df-subg 16811  df-cmn 17429  df-abl 17430  df-mgp 17721  df-ur 17733  df-ring 17779  df-cring 17780  df-cnfld 18968 This theorem is referenced by:  efsubm  23496  circgrp  23497
 Copyright terms: Public domain W3C validator