Metamath Proof Explorer

Theorem dchrelbas4

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 dchrmhm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrmhm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrmhm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrelbas4.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
Assertion dchrelbas4 ( 𝑋 ∈ 𝐷 ↔ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ ℤ ( 1 < ( 𝑥 gcd 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 dchrmhm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrmhm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrmhm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 dchrelbas4.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
5 1 3 dchrrcl ⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
6 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
7 eqid ⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
8 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
9 1 2 6 7 8 3 dchrelbas2 ⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑍 ) ( ( 𝑋 ‘ 𝑦 ) ≠ 0 → 𝑦 ∈ ( Unit ‘ 𝑍 ) ) ) ) )
10 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
11 10 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → 𝑁 ∈ ℕ0 )
12 2 6 4 znzrhfo ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
13 fveq2 ⊢ ( ( 𝐿 ‘ 𝑥 ) = 𝑦 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = ( 𝑋 ‘ 𝑦 ) )
14 13 neeq1d ⊢ ( ( 𝐿 ‘ 𝑥 ) = 𝑦 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) ≠ 0 ↔ ( 𝑋 ‘ 𝑦 ) ≠ 0 ) )
15 eleq1 ⊢ ( ( 𝐿 ‘ 𝑥 ) = 𝑦 → ( ( 𝐿 ‘ 𝑥 ) ∈ ( Unit ‘ 𝑍 ) ↔ 𝑦 ∈ ( Unit ‘ 𝑍 ) ) )
16 14 15 imbi12d ⊢ ( ( 𝐿 ‘ 𝑥 ) = 𝑦 → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) ≠ 0 → ( 𝐿 ‘ 𝑥 ) ∈ ( Unit ‘ 𝑍 ) ) ↔ ( ( 𝑋 ‘ 𝑦 ) ≠ 0 → 𝑦 ∈ ( Unit ‘ 𝑍 ) ) ) )
17 16 cbvfo ⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → ( ∀ 𝑥 ∈ ℤ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) ≠ 0 → ( 𝐿 ‘ 𝑥 ) ∈ ( Unit ‘ 𝑍 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑍 ) ( ( 𝑋 ‘ 𝑦 ) ≠ 0 → 𝑦 ∈ ( Unit ‘ 𝑍 ) ) ) )
18 11 12 17 3syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( ∀ 𝑥 ∈ ℤ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) ≠ 0 → ( 𝐿 ‘ 𝑥 ) ∈ ( Unit ‘ 𝑍 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑍 ) ( ( 𝑋 ‘ 𝑦 ) ≠ 0 → 𝑦 ∈ ( Unit ‘ 𝑍 ) ) ) )
19 df-ne ⊢ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) ≠ 0 ↔ ¬ ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 )
20 19 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) ≠ 0 ↔ ¬ ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) )
21 2 7 4 znunit ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑥 ) ∈ ( Unit ‘ 𝑍 ) ↔ ( 𝑥 gcd 𝑁 ) = 1 ) )
22 11 21 sylan ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑥 ) ∈ ( Unit ‘ 𝑍 ) ↔ ( 𝑥 gcd 𝑁 ) = 1 ) )
23 1red ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → 1 ∈ ℝ )
24 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
25 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → 𝑁 ∈ ℕ )
26 25 nnzd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → 𝑁 ∈ ℤ )
27 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
28 simpr ⊢ ( ( 𝑥 = 0 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
29 28 necon3ai ⊢ ( 𝑁 ≠ 0 → ¬ ( 𝑥 = 0 ∧ 𝑁 = 0 ) )
30 25 27 29 3syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → ¬ ( 𝑥 = 0 ∧ 𝑁 = 0 ) )
31 gcdn0cl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑥 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑥 gcd 𝑁 ) ∈ ℕ )
32 24 26 30 31 syl21anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 gcd 𝑁 ) ∈ ℕ )
33 32 nnred ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 gcd 𝑁 ) ∈ ℝ )
34 32 nnge1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → 1 ≤ ( 𝑥 gcd 𝑁 ) )
35 23 33 34 leltned ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → ( 1 < ( 𝑥 gcd 𝑁 ) ↔ ( 𝑥 gcd 𝑁 ) ≠ 1 ) )
36 35 necon2bbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 gcd 𝑁 ) = 1 ↔ ¬ 1 < ( 𝑥 gcd 𝑁 ) ) )
37 22 36 bitrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑥 ) ∈ ( Unit ‘ 𝑍 ) ↔ ¬ 1 < ( 𝑥 gcd 𝑁 ) ) )
38 20 37 imbi12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) ≠ 0 → ( 𝐿 ‘ 𝑥 ) ∈ ( Unit ‘ 𝑍 ) ) ↔ ( ¬ ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 → ¬ 1 < ( 𝑥 gcd 𝑁 ) ) ) )
39 con34b ⊢ ( ( 1 < ( 𝑥 gcd 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) ↔ ( ¬ ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 → ¬ 1 < ( 𝑥 gcd 𝑁 ) ) )
40 38 39 bitr4di ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) ≠ 0 → ( 𝐿 ‘ 𝑥 ) ∈ ( Unit ‘ 𝑍 ) ) ↔ ( 1 < ( 𝑥 gcd 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) ) )
41 40 ralbidva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( ∀ 𝑥 ∈ ℤ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) ≠ 0 → ( 𝐿 ‘ 𝑥 ) ∈ ( Unit ‘ 𝑍 ) ) ↔ ∀ 𝑥 ∈ ℤ ( 1 < ( 𝑥 gcd 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) ) )
42 18 41 bitr3d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝑍 ) ( ( 𝑋 ‘ 𝑦 ) ≠ 0 → 𝑦 ∈ ( Unit ‘ 𝑍 ) ) ↔ ∀ 𝑥 ∈ ℤ ( 1 < ( 𝑥 gcd 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) ) )
43 42 pm5.32da ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑍 ) ( ( 𝑋 ‘ 𝑦 ) ≠ 0 → 𝑦 ∈ ( Unit ‘ 𝑍 ) ) ) ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ ℤ ( 1 < ( 𝑥 gcd 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) ) ) )
44 9 43 bitrd ⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ ℤ ( 1 < ( 𝑥 gcd 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) ) ) )
45 5 44 biadanii ⊢ ( 𝑋 ∈ 𝐷 ↔ ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ ℤ ( 1 < ( 𝑥 gcd 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) ) ) )
46 3anass ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ ℤ ( 1 < ( 𝑥 gcd 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) ) ↔ ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ ℤ ( 1 < ( 𝑥 gcd 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) ) ) )
47 45 46 bitr4i ⊢ ( 𝑋 ∈ 𝐷 ↔ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ ℤ ( 1 < ( 𝑥 gcd 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑥 ) ) = 0 ) ) )