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

Theorem dchrrcl 23898
Description: Reverse closure for a Dirichlet character. (Contributed by Mario Carneiro, 12-May-2016.)
Hypotheses
Ref Expression
dchrrcl.g  |-  G  =  (DChr `  N )
dchrrcl.b  |-  D  =  ( Base `  G
)
Assertion
Ref Expression
dchrrcl  |-  ( X  e.  D  ->  N  e.  NN )

Proof of Theorem dchrrcl
Dummy variables  n  b  x  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-dchr 23891 . . 3  |- DChr  =  ( n  e.  NN  |->  [_ (ℤ/n `  n )  /  z ]_ [_ { x  e.  ( (mulGrp `  z
) MndHom  (mulGrp ` fld ) )  |  ( ( ( Base `  z
)  \  (Unit `  z
) )  X.  {
0 } )  C_  x }  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  (  oF  x.  |`  ( b  X.  b ) )
>. } )
21dmmptss 5321 . 2  |-  dom DChr  C_  NN
3 n0i 3745 . . 3  |-  ( X  e.  D  ->  -.  D  =  (/) )
4 dchrrcl.g . . . . 5  |-  G  =  (DChr `  N )
5 ndmfv 5875 . . . . 5  |-  ( -.  N  e.  dom DChr  ->  (DChr `  N )  =  (/) )
64, 5syl5eq 2457 . . . 4  |-  ( -.  N  e.  dom DChr  ->  G  =  (/) )
7 fveq2 5851 . . . . 5  |-  ( G  =  (/)  ->  ( Base `  G )  =  (
Base `  (/) ) )
8 dchrrcl.b . . . . 5  |-  D  =  ( Base `  G
)
9 base0 14884 . . . . 5  |-  (/)  =  (
Base `  (/) )
107, 8, 93eqtr4g 2470 . . . 4  |-  ( G  =  (/)  ->  D  =  (/) )
116, 10syl 17 . . 3  |-  ( -.  N  e.  dom DChr  ->  D  =  (/) )
123, 11nsyl2 129 . 2  |-  ( X  e.  D  ->  N  e.  dom DChr )
132, 12sseldi 3442 1  |-  ( X  e.  D  ->  N  e.  NN )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1407    e. wcel 1844   {crab 2760   [_csb 3375    \ cdif 3413    C_ wss 3416   (/)c0 3740   {csn 3974   {cpr 3976   <.cop 3980    X. cxp 4823   dom cdm 4825    |` cres 4827   ` cfv 5571  (class class class)co 6280    oFcof 6521   0cc0 9524    x. cmul 9529   NNcn 10578   ndxcnx 14840   Basecbs 14843   +g cplusg 14911   MndHom cmhm 16290  mulGrpcmgp 17463  Unitcui 17610  ℂfldccnfld 18742  ℤ/nczn 18842  DChrcdchr 23890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3063  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-br 4398  df-opab 4456  df-mpt 4457  df-id 4740  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-iota 5535  df-fun 5573  df-fv 5579  df-slot 14847  df-base 14848  df-dchr 23891
This theorem is referenced by:  dchrmhm  23899  dchrf  23900  dchrelbas4  23901  dchrzrh1  23902  dchrzrhcl  23903  dchrzrhmul  23904  dchrmul  23906  dchrmulcl  23907  dchrn0  23908  dchrmulid2  23910  dchrinvcl  23911  dchrghm  23914  dchrabs  23918  dchrinv  23919  dchrsum2  23926  dchrsum  23927  dchr2sum  23931
  Copyright terms: Public domain W3C validator