Metamath Proof Explorer


Theorem dchrbas

Description: Base set of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrval.g G = DChr N
dchrval.z Z = /N
dchrval.b B = Base Z
dchrval.u U = Unit Z
dchrval.n φ N
dchrbas.b D = Base G
Assertion dchrbas φ D = x mulGrp Z MndHom mulGrp fld | B U × 0 x

Proof

Step Hyp Ref Expression
1 dchrval.g G = DChr N
2 dchrval.z Z = /N
3 dchrval.b B = Base Z
4 dchrval.u U = Unit Z
5 dchrval.n φ N
6 dchrbas.b D = Base G
7 eqidd φ x mulGrp Z MndHom mulGrp fld | B U × 0 x = x mulGrp Z MndHom mulGrp fld | B U × 0 x
8 1 2 3 4 5 7 dchrval φ G = Base ndx x mulGrp Z MndHom mulGrp fld | B U × 0 x + ndx f × x mulGrp Z MndHom mulGrp fld | B U × 0 x × x mulGrp Z MndHom mulGrp fld | B U × 0 x
9 8 fveq2d φ Base G = Base Base ndx x mulGrp Z MndHom mulGrp fld | B U × 0 x + ndx f × x mulGrp Z MndHom mulGrp fld | B U × 0 x × x mulGrp Z MndHom mulGrp fld | B U × 0 x
10 ovex mulGrp Z MndHom mulGrp fld V
11 10 rabex x mulGrp Z MndHom mulGrp fld | B U × 0 x V
12 eqid Base ndx x mulGrp Z MndHom mulGrp fld | B U × 0 x + ndx f × x mulGrp Z MndHom mulGrp fld | B U × 0 x × x mulGrp Z MndHom mulGrp fld | B U × 0 x = Base ndx x mulGrp Z MndHom mulGrp fld | B U × 0 x + ndx f × x mulGrp Z MndHom mulGrp fld | B U × 0 x × x mulGrp Z MndHom mulGrp fld | B U × 0 x
13 12 grpbase x mulGrp Z MndHom mulGrp fld | B U × 0 x V x mulGrp Z MndHom mulGrp fld | B U × 0 x = Base Base ndx x mulGrp Z MndHom mulGrp fld | B U × 0 x + ndx f × x mulGrp Z MndHom mulGrp fld | B U × 0 x × x mulGrp Z MndHom mulGrp fld | B U × 0 x
14 11 13 ax-mp x mulGrp Z MndHom mulGrp fld | B U × 0 x = Base Base ndx x mulGrp Z MndHom mulGrp fld | B U × 0 x + ndx f × x mulGrp Z MndHom mulGrp fld | B U × 0 x × x mulGrp Z MndHom mulGrp fld | B U × 0 x
15 9 6 14 3eqtr4g φ D = x mulGrp Z MndHom mulGrp fld | B U × 0 x