Metamath Proof Explorer


Theorem dchrinvcl

Description: Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses dchrmhm.g 𝐺 = ( DChr ‘ 𝑁 )
dchrmhm.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrmhm.b 𝐷 = ( Base ‘ 𝐺 )
dchrn0.b 𝐵 = ( Base ‘ 𝑍 )
dchrn0.u 𝑈 = ( Unit ‘ 𝑍 )
dchr1cl.o 1 = ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 1 , 0 ) )
dchrmulid2.t · = ( +g𝐺 )
dchrmulid2.x ( 𝜑𝑋𝐷 )
dchrinvcl.n 𝐾 = ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , ( 1 / ( 𝑋𝑘 ) ) , 0 ) )
Assertion dchrinvcl ( 𝜑 → ( 𝐾𝐷 ∧ ( 𝐾 · 𝑋 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 dchrmhm.g 𝐺 = ( DChr ‘ 𝑁 )
2 dchrmhm.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrmhm.b 𝐷 = ( Base ‘ 𝐺 )
4 dchrn0.b 𝐵 = ( Base ‘ 𝑍 )
5 dchrn0.u 𝑈 = ( Unit ‘ 𝑍 )
6 dchr1cl.o 1 = ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 1 , 0 ) )
7 dchrmulid2.t · = ( +g𝐺 )
8 dchrmulid2.x ( 𝜑𝑋𝐷 )
9 dchrinvcl.n 𝐾 = ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , ( 1 / ( 𝑋𝑘 ) ) , 0 ) )
10 1 3 dchrrcl ( 𝑋𝐷𝑁 ∈ ℕ )
11 8 10 syl ( 𝜑𝑁 ∈ ℕ )
12 fveq2 ( 𝑘 = 𝑥 → ( 𝑋𝑘 ) = ( 𝑋𝑥 ) )
13 12 oveq2d ( 𝑘 = 𝑥 → ( 1 / ( 𝑋𝑘 ) ) = ( 1 / ( 𝑋𝑥 ) ) )
14 fveq2 ( 𝑘 = 𝑦 → ( 𝑋𝑘 ) = ( 𝑋𝑦 ) )
15 14 oveq2d ( 𝑘 = 𝑦 → ( 1 / ( 𝑋𝑘 ) ) = ( 1 / ( 𝑋𝑦 ) ) )
16 fveq2 ( 𝑘 = ( 𝑥 ( .r𝑍 ) 𝑦 ) → ( 𝑋𝑘 ) = ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) )
17 16 oveq2d ( 𝑘 = ( 𝑥 ( .r𝑍 ) 𝑦 ) → ( 1 / ( 𝑋𝑘 ) ) = ( 1 / ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) ) )
18 fveq2 ( 𝑘 = ( 1r𝑍 ) → ( 𝑋𝑘 ) = ( 𝑋 ‘ ( 1r𝑍 ) ) )
19 18 oveq2d ( 𝑘 = ( 1r𝑍 ) → ( 1 / ( 𝑋𝑘 ) ) = ( 1 / ( 𝑋 ‘ ( 1r𝑍 ) ) ) )
20 1 2 3 4 8 dchrf ( 𝜑𝑋 : 𝐵 ⟶ ℂ )
21 4 5 unitss 𝑈𝐵
22 21 sseli ( 𝑘𝑈𝑘𝐵 )
23 ffvelrn ( ( 𝑋 : 𝐵 ⟶ ℂ ∧ 𝑘𝐵 ) → ( 𝑋𝑘 ) ∈ ℂ )
24 20 22 23 syl2an ( ( 𝜑𝑘𝑈 ) → ( 𝑋𝑘 ) ∈ ℂ )
25 simpr ( ( 𝜑𝑘𝑈 ) → 𝑘𝑈 )
26 8 adantr ( ( 𝜑𝑘𝑈 ) → 𝑋𝐷 )
27 22 adantl ( ( 𝜑𝑘𝑈 ) → 𝑘𝐵 )
28 1 2 3 4 5 26 27 dchrn0 ( ( 𝜑𝑘𝑈 ) → ( ( 𝑋𝑘 ) ≠ 0 ↔ 𝑘𝑈 ) )
29 25 28 mpbird ( ( 𝜑𝑘𝑈 ) → ( 𝑋𝑘 ) ≠ 0 )
30 24 29 reccld ( ( 𝜑𝑘𝑈 ) → ( 1 / ( 𝑋𝑘 ) ) ∈ ℂ )
31 1t1e1 ( 1 · 1 ) = 1
32 31 eqcomi 1 = ( 1 · 1 )
33 32 a1i ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 1 = ( 1 · 1 ) )
34 1 2 3 dchrmhm 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
35 8 adantr ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝑋𝐷 )
36 34 35 sselid ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
37 simprl ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝑥𝑈 )
38 21 37 sselid ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝑥𝐵 )
39 simprr ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝑦𝑈 )
40 21 39 sselid ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝑦𝐵 )
41 eqid ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
42 41 4 mgpbas 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑍 ) )
43 eqid ( .r𝑍 ) = ( .r𝑍 )
44 41 43 mgpplusg ( .r𝑍 ) = ( +g ‘ ( mulGrp ‘ 𝑍 ) )
45 eqid ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
46 cnfldmul · = ( .r ‘ ℂfld )
47 45 46 mgpplusg · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
48 42 44 47 mhmlin ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝑥𝐵𝑦𝐵 ) → ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( 𝑋𝑥 ) · ( 𝑋𝑦 ) ) )
49 36 38 40 48 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( 𝑋𝑥 ) · ( 𝑋𝑦 ) ) )
50 33 49 oveq12d ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( 1 / ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) ) = ( ( 1 · 1 ) / ( ( 𝑋𝑥 ) · ( 𝑋𝑦 ) ) ) )
51 1cnd ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 1 ∈ ℂ )
52 20 adantr ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → 𝑋 : 𝐵 ⟶ ℂ )
53 52 38 ffvelrnd ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( 𝑋𝑥 ) ∈ ℂ )
54 52 40 ffvelrnd ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( 𝑋𝑦 ) ∈ ℂ )
55 1 2 3 4 5 35 38 dchrn0 ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( ( 𝑋𝑥 ) ≠ 0 ↔ 𝑥𝑈 ) )
56 37 55 mpbird ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( 𝑋𝑥 ) ≠ 0 )
57 1 2 3 4 5 35 40 dchrn0 ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( ( 𝑋𝑦 ) ≠ 0 ↔ 𝑦𝑈 ) )
58 39 57 mpbird ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( 𝑋𝑦 ) ≠ 0 )
59 51 53 51 54 56 58 divmuldivd ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( ( 1 / ( 𝑋𝑥 ) ) · ( 1 / ( 𝑋𝑦 ) ) ) = ( ( 1 · 1 ) / ( ( 𝑋𝑥 ) · ( 𝑋𝑦 ) ) ) )
60 50 59 eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( 1 / ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) ) = ( ( 1 / ( 𝑋𝑥 ) ) · ( 1 / ( 𝑋𝑦 ) ) ) )
61 34 8 sselid ( 𝜑𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
62 eqid ( 1r𝑍 ) = ( 1r𝑍 )
63 41 62 ringidval ( 1r𝑍 ) = ( 0g ‘ ( mulGrp ‘ 𝑍 ) )
64 cnfld1 1 = ( 1r ‘ ℂfld )
65 45 64 ringidval 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
66 63 65 mhm0 ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑋 ‘ ( 1r𝑍 ) ) = 1 )
67 61 66 syl ( 𝜑 → ( 𝑋 ‘ ( 1r𝑍 ) ) = 1 )
68 67 oveq2d ( 𝜑 → ( 1 / ( 𝑋 ‘ ( 1r𝑍 ) ) ) = ( 1 / 1 ) )
69 1div1e1 ( 1 / 1 ) = 1
70 68 69 eqtrdi ( 𝜑 → ( 1 / ( 𝑋 ‘ ( 1r𝑍 ) ) ) = 1 )
71 1 2 4 5 11 3 13 15 17 19 30 60 70 dchrelbasd ( 𝜑 → ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , ( 1 / ( 𝑋𝑘 ) ) , 0 ) ) ∈ 𝐷 )
72 9 71 eqeltrid ( 𝜑𝐾𝐷 )
73 1 2 3 7 72 8 dchrmul ( 𝜑 → ( 𝐾 · 𝑋 ) = ( 𝐾f · 𝑋 ) )
74 4 fvexi 𝐵 ∈ V
75 74 a1i ( 𝜑𝐵 ∈ V )
76 ovex ( 1 / ( 𝑋𝑘 ) ) ∈ V
77 c0ex 0 ∈ V
78 76 77 ifex if ( 𝑘𝑈 , ( 1 / ( 𝑋𝑘 ) ) , 0 ) ∈ V
79 78 a1i ( ( 𝜑𝑘𝐵 ) → if ( 𝑘𝑈 , ( 1 / ( 𝑋𝑘 ) ) , 0 ) ∈ V )
80 20 ffvelrnda ( ( 𝜑𝑘𝐵 ) → ( 𝑋𝑘 ) ∈ ℂ )
81 9 a1i ( 𝜑𝐾 = ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , ( 1 / ( 𝑋𝑘 ) ) , 0 ) ) )
82 20 feqmptd ( 𝜑𝑋 = ( 𝑘𝐵 ↦ ( 𝑋𝑘 ) ) )
83 75 79 80 81 82 offval2 ( 𝜑 → ( 𝐾f · 𝑋 ) = ( 𝑘𝐵 ↦ ( if ( 𝑘𝑈 , ( 1 / ( 𝑋𝑘 ) ) , 0 ) · ( 𝑋𝑘 ) ) ) )
84 ovif ( if ( 𝑘𝑈 , ( 1 / ( 𝑋𝑘 ) ) , 0 ) · ( 𝑋𝑘 ) ) = if ( 𝑘𝑈 , ( ( 1 / ( 𝑋𝑘 ) ) · ( 𝑋𝑘 ) ) , ( 0 · ( 𝑋𝑘 ) ) )
85 80 adantr ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑘𝑈 ) → ( 𝑋𝑘 ) ∈ ℂ )
86 8 adantr ( ( 𝜑𝑘𝐵 ) → 𝑋𝐷 )
87 simpr ( ( 𝜑𝑘𝐵 ) → 𝑘𝐵 )
88 1 2 3 4 5 86 87 dchrn0 ( ( 𝜑𝑘𝐵 ) → ( ( 𝑋𝑘 ) ≠ 0 ↔ 𝑘𝑈 ) )
89 88 biimpar ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑘𝑈 ) → ( 𝑋𝑘 ) ≠ 0 )
90 85 89 recid2d ( ( ( 𝜑𝑘𝐵 ) ∧ 𝑘𝑈 ) → ( ( 1 / ( 𝑋𝑘 ) ) · ( 𝑋𝑘 ) ) = 1 )
91 90 ifeq1da ( ( 𝜑𝑘𝐵 ) → if ( 𝑘𝑈 , ( ( 1 / ( 𝑋𝑘 ) ) · ( 𝑋𝑘 ) ) , ( 0 · ( 𝑋𝑘 ) ) ) = if ( 𝑘𝑈 , 1 , ( 0 · ( 𝑋𝑘 ) ) ) )
92 80 mul02d ( ( 𝜑𝑘𝐵 ) → ( 0 · ( 𝑋𝑘 ) ) = 0 )
93 92 ifeq2d ( ( 𝜑𝑘𝐵 ) → if ( 𝑘𝑈 , 1 , ( 0 · ( 𝑋𝑘 ) ) ) = if ( 𝑘𝑈 , 1 , 0 ) )
94 91 93 eqtrd ( ( 𝜑𝑘𝐵 ) → if ( 𝑘𝑈 , ( ( 1 / ( 𝑋𝑘 ) ) · ( 𝑋𝑘 ) ) , ( 0 · ( 𝑋𝑘 ) ) ) = if ( 𝑘𝑈 , 1 , 0 ) )
95 84 94 syl5eq ( ( 𝜑𝑘𝐵 ) → ( if ( 𝑘𝑈 , ( 1 / ( 𝑋𝑘 ) ) , 0 ) · ( 𝑋𝑘 ) ) = if ( 𝑘𝑈 , 1 , 0 ) )
96 95 mpteq2dva ( 𝜑 → ( 𝑘𝐵 ↦ ( if ( 𝑘𝑈 , ( 1 / ( 𝑋𝑘 ) ) , 0 ) · ( 𝑋𝑘 ) ) ) = ( 𝑘𝐵 ↦ if ( 𝑘𝑈 , 1 , 0 ) ) )
97 6 96 eqtr4id ( 𝜑1 = ( 𝑘𝐵 ↦ ( if ( 𝑘𝑈 , ( 1 / ( 𝑋𝑘 ) ) , 0 ) · ( 𝑋𝑘 ) ) ) )
98 83 97 eqtr4d ( 𝜑 → ( 𝐾f · 𝑋 ) = 1 )
99 73 98 eqtrd ( 𝜑 → ( 𝐾 · 𝑋 ) = 1 )
100 72 99 jca ( 𝜑 → ( 𝐾𝐷 ∧ ( 𝐾 · 𝑋 ) = 1 ) )