Theorem dchrmhm

Description: A Dirichlet character is a monoid homomorphism. (Contributed by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
Assertion	dchrmhm	⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
4		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
5		eqid	⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
6	1 3	dchrrcl	⊢ ( 𝑥 ∈ 𝐷 → 𝑁 ∈ ℕ )
7	1 2 4 5 6 3	dchrelbas	⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( ( Base ‘ 𝑍 ) ∖ ( Unit ‘ 𝑍 ) ) × { 0 } ) ⊆ 𝑥 ) ) )
8	7	ibi	⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( ( Base ‘ 𝑍 ) ∖ ( Unit ‘ 𝑍 ) ) × { 0 } ) ⊆ 𝑥 ) )
9	8	simpld	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
10	9	ssriv	⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )