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	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrval.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrval.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
	dchrval.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
	dchrval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	dchrbas.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
Assertion	dchrelbas	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dchrval.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrval.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchrval.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
4		dchrval.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
5		dchrval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		dchrbas.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
7	1 2 3 4 5 6	dchrbas	⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } )
8	7	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ 𝑋 ∈ { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ) )
9		sseq2	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 ↔ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ) )
10	9	elrab	⊢ ( 𝑋 ∈ { 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑥 } ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ) )
11	8 10	bitrdi	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ) ) )