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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 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 ) )