Theorem dchrelbas

Description: A Dirichlet character is a monoid homomorphism from the multiplicative monoid on Z/nZ to the multiplicative monoid of CC , which is zero off the group of units of Z/nZ . (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	dchrval.g	|- G = ( DChr ` N )
	dchrval.z	|- Z = ( Z/nZ ` N )
	dchrval.b	|- B = ( Base ` Z )
	dchrval.u	|- U = ( Unit ` Z )
	dchrval.n	|- ( ph -> N e. NN )
	dchrbas.b	|- D = ( Base ` G )
Assertion	dchrelbas	|- ( ph -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) ) )

Proof

Step	Hyp	Ref	Expression
1		dchrval.g	|- G = ( DChr ` N )
2		dchrval.z	|- Z = ( Z/nZ ` N )
3		dchrval.b	|- B = ( Base ` Z )
4		dchrval.u	|- U = ( Unit ` Z )
5		dchrval.n	|- ( ph -> N e. NN )
6		dchrbas.b	|- D = ( Base ` G )
7	1 2 3 4 5 6	dchrbas	|- ( ph -> D = { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } )
8	7	eleq2d	|- ( ph -> ( X e. D <-> X e. { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } ) )
9		sseq2	|- ( x = X -> ( ( ( B \ U ) X. { 0 } ) C_ x <-> ( ( B \ U ) X. { 0 } ) C_ X ) )
10	9	elrab	|- ( X e. { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) )
11	8 10	bitrdi	|- ( ph -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) ) )