Metamath Proof Explorer


Theorem dchrelbasd

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, 28-Apr-2016)

Ref Expression
Hypotheses dchrval.g 𝐺 = ( DChr ‘ 𝑁 )
dchrval.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrval.b 𝐵 = ( Base ‘ 𝑍 )
dchrval.u 𝑈 = ( Unit ‘ 𝑍 )
dchrval.n ( 𝜑𝑁 ∈ ℕ )
dchrbas.b 𝐷 = ( Base ‘ 𝐺 )
dchrelbasd.1 ( 𝑘 = 𝑥𝑋 = 𝐴 )
dchrelbasd.2 ( 𝑘 = 𝑦𝑋 = 𝐶 )
dchrelbasd.3 ( 𝑘 = ( 𝑥 ( .r𝑍 ) 𝑦 ) → 𝑋 = 𝐸 )
dchrelbasd.4 ( 𝑘 = ( 1r𝑍 ) → 𝑋 = 𝑌 )
dchrelbasd.5 ( ( 𝜑𝑘𝑈 ) → 𝑋 ∈ ℂ )
dchrelbasd.6 ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝐸 = ( 𝐴 · 𝐶 ) )
dchrelbasd.7 ( 𝜑𝑌 = 1 )
Assertion dchrelbasd ( 𝜑 → ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 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 dchrelbasd.1 ( 𝑘 = 𝑥𝑋 = 𝐴 )
8 dchrelbasd.2 ( 𝑘 = 𝑦𝑋 = 𝐶 )
9 dchrelbasd.3 ( 𝑘 = ( 𝑥 ( .r𝑍 ) 𝑦 ) → 𝑋 = 𝐸 )
10 dchrelbasd.4 ( 𝑘 = ( 1r𝑍 ) → 𝑋 = 𝑌 )
11 dchrelbasd.5 ( ( 𝜑𝑘𝑈 ) → 𝑋 ∈ ℂ )
12 dchrelbasd.6 ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝐸 = ( 𝐴 · 𝐶 ) )
13 dchrelbasd.7 ( 𝜑𝑌 = 1 )
14 11 adantlr ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑘𝑈 ) → 𝑋 ∈ ℂ )
15 0cnd ( ( ( 𝜑𝑘𝐵 ) ∧ ¬ 𝑘𝑈 ) → 0 ∈ ℂ )
16 14 15 ifclda ( ( 𝜑𝑘𝐵 ) → if ( 𝑘𝑈 , 𝑋 , 0 ) ∈ ℂ )
17 16 fmpttd ( 𝜑 → ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) : 𝐵 ⟶ ℂ )
18 5 nnnn0d ( 𝜑𝑁 ∈ ℕ0 )
19 2 zncrng ( 𝑁 ∈ ℕ0𝑍 ∈ CRing )
20 crngring ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
21 18 19 20 3syl ( 𝜑𝑍 ∈ Ring )
22 eqid ( .r𝑍 ) = ( .r𝑍 )
23 4 22 unitmulcl ( ( 𝑍 ∈ Ring ∧ 𝑥𝑈𝑦𝑈 ) → ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ 𝑈 )
24 23 3expb ( ( 𝑍 ∈ Ring ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ 𝑈 )
25 21 24 sylan ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ 𝑈 )
26 25 iftrued ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → if ( ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ 𝑈 , 𝐸 , 0 ) = 𝐸 )
27 26 12 eqtrd ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → if ( ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ 𝑈 , 𝐸 , 0 ) = ( 𝐴 · 𝐶 ) )
28 eqid ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) = ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) )
29 eleq1 ( 𝑘 = ( 𝑥 ( .r𝑍 ) 𝑦 ) → ( 𝑘𝑈 ↔ ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ 𝑈 ) )
30 29 9 ifbieq1d ( 𝑘 = ( 𝑥 ( .r𝑍 ) 𝑦 ) → if ( 𝑘𝑈 , 𝑋 , 0 ) = if ( ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ 𝑈 , 𝐸 , 0 ) )
31 3 4 unitss 𝑈𝐵
32 31 25 sselid ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ 𝐵 )
33 9 eleq1d ( 𝑘 = ( 𝑥 ( .r𝑍 ) 𝑦 ) → ( 𝑋 ∈ ℂ ↔ 𝐸 ∈ ℂ ) )
34 11 ralrimiva ( 𝜑 → ∀ 𝑘𝑈 𝑋 ∈ ℂ )
35 34 adantr ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ∀ 𝑘𝑈 𝑋 ∈ ℂ )
36 33 35 25 rspcdva ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝐸 ∈ ℂ )
37 26 36 eqeltrd ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → if ( ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ 𝑈 , 𝐸 , 0 ) ∈ ℂ )
38 28 30 32 37 fvmptd3 ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = if ( ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ 𝑈 , 𝐸 , 0 ) )
39 eleq1 ( 𝑘 = 𝑥 → ( 𝑘𝑈𝑥𝑈 ) )
40 39 7 ifbieq1d ( 𝑘 = 𝑥 → if ( 𝑘𝑈 , 𝑋 , 0 ) = if ( 𝑥𝑈 , 𝐴 , 0 ) )
41 simprl ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝑥𝑈 )
42 31 41 sselid ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝑥𝐵 )
43 iftrue ( 𝑥𝑈 → if ( 𝑥𝑈 , 𝐴 , 0 ) = 𝐴 )
44 43 ad2antrl ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → if ( 𝑥𝑈 , 𝐴 , 0 ) = 𝐴 )
45 7 eleq1d ( 𝑘 = 𝑥 → ( 𝑋 ∈ ℂ ↔ 𝐴 ∈ ℂ ) )
46 45 35 41 rspcdva ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝐴 ∈ ℂ )
47 44 46 eqeltrd ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → if ( 𝑥𝑈 , 𝐴 , 0 ) ∈ ℂ )
48 28 40 42 47 fvmptd3 ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) = if ( 𝑥𝑈 , 𝐴 , 0 ) )
49 48 44 eqtrd ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) = 𝐴 )
50 eleq1 ( 𝑘 = 𝑦 → ( 𝑘𝑈𝑦𝑈 ) )
51 50 8 ifbieq1d ( 𝑘 = 𝑦 → if ( 𝑘𝑈 , 𝑋 , 0 ) = if ( 𝑦𝑈 , 𝐶 , 0 ) )
52 simprr ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝑦𝑈 )
53 31 52 sselid ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝑦𝐵 )
54 iftrue ( 𝑦𝑈 → if ( 𝑦𝑈 , 𝐶 , 0 ) = 𝐶 )
55 54 ad2antll ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → if ( 𝑦𝑈 , 𝐶 , 0 ) = 𝐶 )
56 8 eleq1d ( 𝑘 = 𝑦 → ( 𝑋 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
57 56 35 52 rspcdva ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝐶 ∈ ℂ )
58 55 57 eqeltrd ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → if ( 𝑦𝑈 , 𝐶 , 0 ) ∈ ℂ )
59 28 51 53 58 fvmptd3 ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) = if ( 𝑦𝑈 , 𝐶 , 0 ) )
60 59 55 eqtrd ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) = 𝐶 )
61 49 60 oveq12d ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) · ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) ) = ( 𝐴 · 𝐶 ) )
62 27 38 61 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) · ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) ) )
63 62 ralrimivva ( 𝜑 → ∀ 𝑥𝑈𝑦𝑈 ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) · ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) ) )
64 eleq1 ( 𝑘 = ( 1r𝑍 ) → ( 𝑘𝑈 ↔ ( 1r𝑍 ) ∈ 𝑈 ) )
65 64 10 ifbieq1d ( 𝑘 = ( 1r𝑍 ) → if ( 𝑘𝑈 , 𝑋 , 0 ) = if ( ( 1r𝑍 ) ∈ 𝑈 , 𝑌 , 0 ) )
66 eqid ( 1r𝑍 ) = ( 1r𝑍 )
67 4 66 1unit ( 𝑍 ∈ Ring → ( 1r𝑍 ) ∈ 𝑈 )
68 21 67 syl ( 𝜑 → ( 1r𝑍 ) ∈ 𝑈 )
69 31 68 sselid ( 𝜑 → ( 1r𝑍 ) ∈ 𝐵 )
70 68 iftrued ( 𝜑 → if ( ( 1r𝑍 ) ∈ 𝑈 , 𝑌 , 0 ) = 𝑌 )
71 70 13 eqtrd ( 𝜑 → if ( ( 1r𝑍 ) ∈ 𝑈 , 𝑌 , 0 ) = 1 )
72 ax-1cn 1 ∈ ℂ
73 71 72 eqeltrdi ( 𝜑 → if ( ( 1r𝑍 ) ∈ 𝑈 , 𝑌 , 0 ) ∈ ℂ )
74 28 65 69 73 fvmptd3 ( 𝜑 → ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ ( 1r𝑍 ) ) = if ( ( 1r𝑍 ) ∈ 𝑈 , 𝑌 , 0 ) )
75 74 71 eqtrd ( 𝜑 → ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ ( 1r𝑍 ) ) = 1 )
76 simpr ( ( 𝜑𝑥𝐵 ) → 𝑥𝐵 )
77 45 rspcv ( 𝑥𝑈 → ( ∀ 𝑘𝑈 𝑋 ∈ ℂ → 𝐴 ∈ ℂ ) )
78 34 77 mpan9 ( ( 𝜑𝑥𝑈 ) → 𝐴 ∈ ℂ )
79 78 adantlr ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑥𝑈 ) → 𝐴 ∈ ℂ )
80 0cnd ( ( ( 𝜑𝑥𝐵 ) ∧ ¬ 𝑥𝑈 ) → 0 ∈ ℂ )
81 79 80 ifclda ( ( 𝜑𝑥𝐵 ) → if ( 𝑥𝑈 , 𝐴 , 0 ) ∈ ℂ )
82 28 40 76 81 fvmptd3 ( ( 𝜑𝑥𝐵 ) → ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) = if ( 𝑥𝑈 , 𝐴 , 0 ) )
83 82 neeq1d ( ( 𝜑𝑥𝐵 ) → ( ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) ≠ 0 ↔ if ( 𝑥𝑈 , 𝐴 , 0 ) ≠ 0 ) )
84 iffalse ( ¬ 𝑥𝑈 → if ( 𝑥𝑈 , 𝐴 , 0 ) = 0 )
85 84 necon1ai ( if ( 𝑥𝑈 , 𝐴 , 0 ) ≠ 0 → 𝑥𝑈 )
86 83 85 syl6bi ( ( 𝜑𝑥𝐵 ) → ( ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) ≠ 0 → 𝑥𝑈 ) )
87 86 ralrimiva ( 𝜑 → ∀ 𝑥𝐵 ( ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) ≠ 0 → 𝑥𝑈 ) )
88 63 75 87 3jca ( 𝜑 → ( ∀ 𝑥𝑈𝑦𝑈 ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) · ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) ) ∧ ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ ( 1r𝑍 ) ) = 1 ∧ ∀ 𝑥𝐵 ( ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) ≠ 0 → 𝑥𝑈 ) ) )
89 1 2 3 4 5 6 dchrelbas3 ( 𝜑 → ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ∈ 𝐷 ↔ ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) : 𝐵 ⟶ ℂ ∧ ( ∀ 𝑥𝑈𝑦𝑈 ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) · ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑦 ) ) ∧ ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ ( 1r𝑍 ) ) = 1 ∧ ∀ 𝑥𝐵 ( ( ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ‘ 𝑥 ) ≠ 0 → 𝑥𝑈 ) ) ) ) )
90 17 88 89 mpbir2and ( 𝜑 → ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 𝑋 , 0 ) ) ∈ 𝐷 )