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

Theorem dchrval 23352
 Description: Value of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
Hypotheses
Ref Expression
dchrval.g DChr
dchrval.z ℤ/n
dchrval.b
dchrval.u Unit
dchrval.n
dchrval.d mulGrp MndHom mulGrpfld
Assertion
Ref Expression
dchrval
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem dchrval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dchrval.g . 2 DChr
2 df-dchr 23351 . . . 4 DChr ℤ/n mulGrp MndHom mulGrpfld Unit
32a1i 11 . . 3 DChr ℤ/n mulGrp MndHom mulGrpfld Unit
4 fvex 5881 . . . . 5 ℤ/n
54a1i 11 . . . 4 ℤ/n
6 ovex 6319 . . . . . . 7 mulGrp MndHom mulGrpfld
76rabex 4603 . . . . . 6 mulGrp MndHom mulGrpfld Unit
87a1i 11 . . . . 5 ℤ/n mulGrp MndHom mulGrpfld Unit
9 dchrval.d . . . . . . . . . . 11 mulGrp MndHom mulGrpfld
109ad2antrr 725 . . . . . . . . . 10 ℤ/n mulGrp MndHom mulGrpfld
11 simpr 461 . . . . . . . . . . . . . . . . 17
1211fveq2d 5875 . . . . . . . . . . . . . . . 16 ℤ/n ℤ/n
13 dchrval.z . . . . . . . . . . . . . . . 16 ℤ/n
1412, 13syl6reqr 2527 . . . . . . . . . . . . . . 15 ℤ/n
1514eqeq2d 2481 . . . . . . . . . . . . . 14 ℤ/n
1615biimpar 485 . . . . . . . . . . . . 13 ℤ/n
1716fveq2d 5875 . . . . . . . . . . . 12 ℤ/n mulGrp mulGrp
1817oveq1d 6309 . . . . . . . . . . 11 ℤ/n mulGrp MndHom mulGrpfld mulGrp MndHom mulGrpfld
1916fveq2d 5875 . . . . . . . . . . . . . . 15 ℤ/n
20 dchrval.b . . . . . . . . . . . . . . 15
2119, 20syl6eqr 2526 . . . . . . . . . . . . . 14 ℤ/n
2216fveq2d 5875 . . . . . . . . . . . . . . 15 ℤ/n Unit Unit
23 dchrval.u . . . . . . . . . . . . . . 15 Unit
2422, 23syl6eqr 2526 . . . . . . . . . . . . . 14 ℤ/n Unit
2521, 24difeq12d 3628 . . . . . . . . . . . . 13 ℤ/n Unit
2625xpeq1d 5027 . . . . . . . . . . . 12 ℤ/n Unit
2726sseq1d 3536 . . . . . . . . . . 11 ℤ/n Unit
2818, 27rabeqbidv 3113 . . . . . . . . . 10 ℤ/n mulGrp MndHom mulGrpfld Unit mulGrp MndHom mulGrpfld
2910, 28eqtr4d 2511 . . . . . . . . 9 ℤ/n mulGrp MndHom mulGrpfld Unit
3029eqeq2d 2481 . . . . . . . 8 ℤ/n mulGrp MndHom mulGrpfld Unit
3130biimpar 485 . . . . . . 7 ℤ/n mulGrp MndHom mulGrpfld Unit
3231opeq2d 4225 . . . . . 6 ℤ/n mulGrp MndHom mulGrpfld Unit
3331, 31xpeq12d 5029 . . . . . . . 8 ℤ/n mulGrp MndHom mulGrpfld Unit
3433reseq2d 5278 . . . . . . 7 ℤ/n mulGrp MndHom mulGrpfld Unit
3534opeq2d 4225 . . . . . 6 ℤ/n mulGrp MndHom mulGrpfld Unit
3632, 35preq12d 4119 . . . . 5 ℤ/n mulGrp MndHom mulGrpfld Unit
378, 36csbied 3467 . . . 4 ℤ/n mulGrp MndHom mulGrpfld Unit
385, 37csbied 3467 . . 3 ℤ/n mulGrp MndHom mulGrpfld Unit
39 dchrval.n . . 3
40 prex 4694 . . . 4
4140a1i 11 . . 3
423, 38, 39, 41fvmptd 5961 . 2 DChr
431, 42syl5eq 2520 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1379   wcel 1767  crab 2821  cvv 3118  csb 3440   cdif 3478   wss 3481  csn 4032  cpr 4034  cop 4038   cmpt 4510   cxp 5002   cres 5006  cfv 5593  (class class class)co 6294   cof 6532  cc0 9502   cmul 9507  cn 10546  cnx 14499  cbs 14502   cplusg 14567   MndHom cmhm 15817  mulGrpcmgp 16990  Unitcui 17137  ℂfldccnfld 18267  ℤ/nℤczn 18386  DChrcdchr 23350 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4573  ax-nul 4581  ax-pr 4691 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4251  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-res 5016  df-iota 5556  df-fun 5595  df-fv 5601  df-ov 6297  df-dchr 23351 This theorem is referenced by:  dchrbas  23353  dchrplusg  23365
 Copyright terms: Public domain W3C validator