Description: Reverse closure for a Dirichlet character. (Contributed by Mario Carneiro, 12-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dchrrcl.g | |- G = ( DChr ` N ) |
|
| dchrrcl.b | |- D = ( Base ` G ) |
||
| Assertion | dchrrcl | |- ( X e. D -> N e. NN ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dchrrcl.g | |- G = ( DChr ` N ) |
|
| 2 | dchrrcl.b | |- D = ( Base ` G ) |
|
| 3 | df-dchr | |- DChr = ( n e. NN |-> [_ ( Z/nZ ` n ) / z ]_ [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } ) |
|
| 4 | 3 | dmmptss | |- dom DChr C_ NN |
| 5 | n0i | |- ( X e. D -> -. D = (/) ) |
|
| 6 | ndmfv | |- ( -. N e. dom DChr -> ( DChr ` N ) = (/) ) |
|
| 7 | 1 6 | syl5eq | |- ( -. N e. dom DChr -> G = (/) ) |
| 8 | fveq2 | |- ( G = (/) -> ( Base ` G ) = ( Base ` (/) ) ) |
|
| 9 | base0 | |- (/) = ( Base ` (/) ) |
|
| 10 | 8 2 9 | 3eqtr4g | |- ( G = (/) -> D = (/) ) |
| 11 | 7 10 | syl | |- ( -. N e. dom DChr -> D = (/) ) |
| 12 | 5 11 | nsyl2 | |- ( X e. D -> N e. dom DChr ) |
| 13 | 4 12 | sseldi | |- ( X e. D -> N e. NN ) |