Metamath Proof Explorer

Theorem dchrelbas2

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 dchrelbas2 ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ ( ( 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 dchrelbas ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ) ) )
8 eqid ⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
9 8 3 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑍 ) )
10 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
11 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
12 10 11 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
13 9 12 mhmf ⊢ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → 𝑋 : 𝐵 ⟶ ℂ )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → 𝑋 : 𝐵 ⟶ ℂ )
15 14 ffund ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → Fun 𝑋 )
16 funssres ⊢ ( ( Fun 𝑋 ∧ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ) → ( 𝑋 ↾ dom ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) )
17 15 16 sylan ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ) → ( 𝑋 ↾ dom ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) )
18 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ ( 𝑋 ↾ dom ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) → ( 𝑋 ↾ dom ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) )
19 resss ⊢ ( 𝑋 ↾ dom ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) ⊆ 𝑋
20 18 19 eqsstrrdi ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) ∧ ( 𝑋 ↾ dom ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) → ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 )
21 17 20 impbida ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ↔ ( 𝑋 ↾ dom ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) )
22 0cn ⊢ 0 ∈ ℂ
23 fconst6g ⊢ ( 0 ∈ ℂ → ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) : ( 𝐵 ∖ 𝑈 ) ⟶ ℂ )
24 22 23 mp1i ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) : ( 𝐵 ∖ 𝑈 ) ⟶ ℂ )
25 24 fdmd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → dom ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) = ( 𝐵 ∖ 𝑈 ) )
26 25 reseq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( 𝑋 ↾ dom ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) = ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) )
27 26 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( ( 𝑋 ↾ dom ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ↔ ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ) )
28 difss ⊢ ( 𝐵 ∖ 𝑈 ) ⊆ 𝐵
29 fssres ⊢ ( ( 𝑋 : 𝐵 ⟶ ℂ ∧ ( 𝐵 ∖ 𝑈 ) ⊆ 𝐵 ) → ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) : ( 𝐵 ∖ 𝑈 ) ⟶ ℂ )
30 14 28 29 sylancl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) : ( 𝐵 ∖ 𝑈 ) ⟶ ℂ )
31 30 ffnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) Fn ( 𝐵 ∖ 𝑈 ) )
32 24 ffnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) Fn ( 𝐵 ∖ 𝑈 ) )
33 eqfnfv ⊢ ( ( ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) Fn ( 𝐵 ∖ 𝑈 ) ∧ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) Fn ( 𝐵 ∖ 𝑈 ) ) → ( ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ( ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) ‘ 𝑥 ) = ( ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ‘ 𝑥 ) ) )
34 31 32 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ( ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) ‘ 𝑥 ) = ( ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ‘ 𝑥 ) ) )
35 fvres ⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) → ( ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) ‘ 𝑥 ) = ( 𝑋 ‘ 𝑥 ) )
36 c0ex ⊢ 0 ∈ V
37 36 fvconst2 ⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) → ( ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ‘ 𝑥 ) = 0 )
38 35 37 eqeq12d ⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) → ( ( ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) ‘ 𝑥 ) = ( ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ‘ 𝑥 ) ↔ ( 𝑋 ‘ 𝑥 ) = 0 ) )
39 38 ralbiia ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ( ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) ‘ 𝑥 ) = ( ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ( 𝑋 ‘ 𝑥 ) = 0 )
40 eldif ⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈 ) )
41 40 imbi1i ⊢ ( ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) → ( 𝑋 ‘ 𝑥 ) = 0 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑥 ) = 0 ) )
42 impexp ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑥 ) = 0 ) ↔ ( 𝑥 ∈ 𝐵 → ( ¬ 𝑥 ∈ 𝑈 → ( 𝑋 ‘ 𝑥 ) = 0 ) ) )
43 con1b ⊢ ( ( ¬ 𝑥 ∈ 𝑈 → ( 𝑋 ‘ 𝑥 ) = 0 ) ↔ ( ¬ ( 𝑋 ‘ 𝑥 ) = 0 → 𝑥 ∈ 𝑈 ) )
44 df-ne ⊢ ( ( 𝑋 ‘ 𝑥 ) ≠ 0 ↔ ¬ ( 𝑋 ‘ 𝑥 ) = 0 )
45 44 imbi1i ⊢ ( ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ↔ ( ¬ ( 𝑋 ‘ 𝑥 ) = 0 → 𝑥 ∈ 𝑈 ) )
46 43 45 bitr4i ⊢ ( ( ¬ 𝑥 ∈ 𝑈 → ( 𝑋 ‘ 𝑥 ) = 0 ) ↔ ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) )
47 46 imbi2i ⊢ ( ( 𝑥 ∈ 𝐵 → ( ¬ 𝑥 ∈ 𝑈 → ( 𝑋 ‘ 𝑥 ) = 0 ) ) ↔ ( 𝑥 ∈ 𝐵 → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ) )
48 41 42 47 3bitri ⊢ ( ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) → ( 𝑋 ‘ 𝑥 ) = 0 ) ↔ ( 𝑥 ∈ 𝐵 → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ) )
49 48 ralbii2 ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ( 𝑋 ‘ 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) )
50 39 49 bitri ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ( ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) ‘ 𝑥 ) = ( ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) )
51 34 50 bitrdi ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( ( 𝑋 ↾ ( 𝐵 ∖ 𝑈 ) ) = ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ) )
52 21 27 51 3bitrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) → ( ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ) )
53 52 pm5.32da ⊢ ( 𝜑 → ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( 𝐵 ∖ 𝑈 ) × { 0 } ) ⊆ 𝑋 ) ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ) ) )
54 7 53 bitrd ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ) ) )