This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) ⊆ 𝑋 ) ) )