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