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

Theorem dchrmulcl 24040
 Description: Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
Hypotheses
Ref Expression
dchrmhm.g DChr
dchrmhm.z ℤ/n
dchrmhm.b
dchrmul.t
dchrmul.x
dchrmul.y
Assertion
Ref Expression
dchrmulcl

Proof of Theorem dchrmulcl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dchrmhm.g . . 3 DChr
2 dchrmhm.z . . 3 ℤ/n
3 dchrmhm.b . . 3
4 dchrmul.t . . 3
5 dchrmul.x . . 3
6 dchrmul.y . . 3
71, 2, 3, 4, 5, 6dchrmul 24039 . 2
8 mulcl 9622 . . . . 5
98adantl 467 . . . 4
10 eqid 2429 . . . . 5
111, 2, 3, 10, 5dchrf 24033 . . . 4
121, 2, 3, 10, 6dchrf 24033 . . . 4
13 fvex 5891 . . . . 5
1413a1i 11 . . . 4
15 inidm 3677 . . . 4
169, 11, 12, 14, 14, 15off 6560 . . 3
17 eqid 2429 . . . . . . . 8 Unit Unit
1810, 17unitcl 17822 . . . . . . 7 Unit
1910, 17unitcl 17822 . . . . . . 7 Unit
2018, 19anim12i 568 . . . . . 6 Unit Unit
211, 3dchrrcl 24031 . . . . . . . . . . . . . 14
225, 21syl 17 . . . . . . . . . . . . 13
231, 2, 10, 17, 22, 3dchrelbas2 24028 . . . . . . . . . . . 12 mulGrp MndHom mulGrpfld Unit
245, 23mpbid 213 . . . . . . . . . . 11 mulGrp MndHom mulGrpfld Unit
2524simpld 460 . . . . . . . . . 10 mulGrp MndHom mulGrpfld
26 eqid 2429 . . . . . . . . . . . . 13 mulGrp mulGrp
2726, 10mgpbas 17664 . . . . . . . . . . . 12 mulGrp
28 eqid 2429 . . . . . . . . . . . . 13
2926, 28mgpplusg 17662 . . . . . . . . . . . 12 mulGrp
30 eqid 2429 . . . . . . . . . . . . 13 mulGrpfld mulGrpfld
31 cnfldmul 18911 . . . . . . . . . . . . 13 fld
3230, 31mgpplusg 17662 . . . . . . . . . . . 12 mulGrpfld
3327, 29, 32mhmlin 16540 . . . . . . . . . . 11 mulGrp MndHom mulGrpfld
34333expb 1206 . . . . . . . . . 10 mulGrp MndHom mulGrpfld
3525, 34sylan 473 . . . . . . . . 9
361, 2, 10, 17, 22, 3dchrelbas2 24028 . . . . . . . . . . . 12 mulGrp MndHom mulGrpfld Unit
376, 36mpbid 213 . . . . . . . . . . 11 mulGrp MndHom mulGrpfld Unit
3837simpld 460 . . . . . . . . . 10 mulGrp MndHom mulGrpfld
3927, 29, 32mhmlin 16540 . . . . . . . . . . 11 mulGrp MndHom mulGrpfld
40393expb 1206 . . . . . . . . . 10 mulGrp MndHom mulGrpfld
4138, 40sylan 473 . . . . . . . . 9
4235, 41oveq12d 6323 . . . . . . . 8
4311ffvelrnda 6037 . . . . . . . . . 10
4443adantrr 721 . . . . . . . . 9
45 simpr 462 . . . . . . . . . 10
46 ffvelrn 6035 . . . . . . . . . 10
4711, 45, 46syl2an 479 . . . . . . . . 9
4812ffvelrnda 6037 . . . . . . . . . 10
4948adantrr 721 . . . . . . . . 9
50 ffvelrn 6035 . . . . . . . . . 10
5112, 45, 50syl2an 479 . . . . . . . . 9
5244, 47, 49, 51mul4d 9844 . . . . . . . 8
5342, 52eqtrd 2470 . . . . . . 7
54 ffn 5746 . . . . . . . . . 10
5511, 54syl 17 . . . . . . . . 9
5655adantr 466 . . . . . . . 8
57 ffn 5746 . . . . . . . . . 10
5812, 57syl 17 . . . . . . . . 9
5958adantr 466 . . . . . . . 8
6013a1i 11 . . . . . . . 8
6122nnnn0d 10925 . . . . . . . . . 10
622zncrng 19046 . . . . . . . . . 10
63 crngring 17726 . . . . . . . . . 10
6461, 62, 633syl 18 . . . . . . . . 9
6510, 28ringcl 17729 . . . . . . . . . 10
66653expb 1206 . . . . . . . . 9
6764, 66sylan 473 . . . . . . . 8
68 fnfvof 6559 . . . . . . . 8
6956, 59, 60, 67, 68syl22anc 1265 . . . . . . 7
7055adantr 466 . . . . . . . . . 10
7158adantr 466 . . . . . . . . . 10
7213a1i 11 . . . . . . . . . 10
73 simpr 462 . . . . . . . . . 10
74 fnfvof 6559 . . . . . . . . . 10
7570, 71, 72, 73, 74syl22anc 1265 . . . . . . . . 9
7675adantrr 721 . . . . . . . 8
77 simprr 764 . . . . . . . . 9
78 fnfvof 6559 . . . . . . . . 9
7956, 59, 60, 77, 78syl22anc 1265 . . . . . . . 8
8076, 79oveq12d 6323 . . . . . . 7
8153, 69, 803eqtr4d 2480 . . . . . 6
8220, 81sylan2 476 . . . . 5 Unit Unit
8382ralrimivva 2853 . . . 4 Unit Unit
84 eqid 2429 . . . . . . . 8
8510, 84ringidcl 17736 . . . . . . 7
8664, 85syl 17 . . . . . 6
87 fnfvof 6559 . . . . . 6
8855, 58, 14, 86, 87syl22anc 1265 . . . . 5
8926, 84ringidval 17672 . . . . . . . . 9 mulGrp
90 cnfld1 18928 . . . . . . . . . 10 fld
9130, 90ringidval 17672 . . . . . . . . 9 mulGrpfld
9289, 91mhm0 16541 . . . . . . . 8 mulGrp MndHom mulGrpfld
9325, 92syl 17 . . . . . . 7
9489, 91mhm0 16541 . . . . . . . 8 mulGrp MndHom mulGrpfld
9538, 94syl 17 . . . . . . 7
9693, 95oveq12d 6323 . . . . . 6
97 1t1e1 10757 . . . . . 6
9896, 97syl6eq 2486 . . . . 5
9988, 98eqtrd 2470 . . . 4
10075neeq1d 2708 . . . . . . 7
10143, 48mulne0bd 10262 . . . . . . 7
102100, 101bitr4d 259 . . . . . 6
10324simprd 464 . . . . . . . 8 Unit
104103r19.21bi 2801 . . . . . . 7 Unit
105104adantrd 469 . . . . . 6 Unit
106102, 105sylbid 218 . . . . 5 Unit
107106ralrimiva 2846 . . . 4 Unit
10883, 99, 1073jca 1185 . . 3 Unit Unit Unit
1091, 2, 10, 17, 22, 3dchrelbas3 24029 . . 3 Unit Unit Unit
11016, 108, 109mpbir2and 930 . 2
1117, 110eqeltrd 2517 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3a 982   wceq 1437   wcel 1870   wne 2625  wral 2782  cvv 3087   wfn 5596  wf 5597  cfv 5601  (class class class)co 6305   cof 6543  cc 9536  cc0 9538  c1 9539   cmul 9543  cn 10609  cn0 10869  cbs 15084   cplusg 15152  cmulr 15153   MndHom cmhm 16531  mulGrpcmgp 17658  cur 17670  crg 17715  ccrg 17716  Unitcui 17802  ℂfldccnfld 18905  ℤ/nℤczn 19005  DChrcdchr 24023 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615  ax-addf 9617  ax-mulf 9618 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-of 6545  df-om 6707  df-1st 6807  df-2nd 6808  df-tpos 6981  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-oadd 7194  df-er 7371  df-ec 7373  df-qs 7377  df-map 7482  df-en 7578  df-dom 7579  df-sdom 7580  df-fin 7581  df-sup 7962  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-fz 11783  df-struct 15086  df-ndx 15087  df-slot 15088  df-base 15089  df-sets 15090  df-ress 15091  df-plusg 15165  df-mulr 15166  df-starv 15167  df-sca 15168  df-vsca 15169  df-ip 15170  df-tset 15171  df-ple 15172  df-ds 15174  df-unif 15175  df-0g 15299  df-imas 15365  df-qus 15366  df-mgm 16439  df-sgrp 16478  df-mnd 16488  df-mhm 16533  df-grp 16624  df-minusg 16625  df-sbg 16626  df-subg 16765  df-nsg 16766  df-eqg 16767  df-cmn 17367  df-abl 17368  df-mgp 17659  df-ur 17671  df-ring 17717  df-cring 17718  df-oppr 17786  df-dvdsr 17804  df-unit 17805  df-subrg 17941  df-lmod 18028  df-lss 18091  df-lsp 18130  df-sra 18330  df-rgmod 18331  df-lidl 18332  df-rsp 18333  df-2idl 18391  df-cnfld 18906  df-zring 18974  df-zn 19009  df-dchr 24024 This theorem is referenced by:  dchrabl  24045  dchrinv  24052
 Copyright terms: Public domain W3C validator