Metamath Proof Explorer

Theorem dchrabl

Description: The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis dchrabl.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
Assertion dchrabl ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )

Proof

Step Hyp Ref Expression
1 dchrabl.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 eqidd ⊢ ( 𝑁 ∈ ℕ → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
3 eqidd ⊢ ( 𝑁 ∈ ℕ → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) )
4 eqid ⊢ ( ℤ/nℤ ‘ 𝑁 ) = ( ℤ/nℤ ‘ 𝑁 )
5 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7 simp2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
8 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
9 1 4 5 6 7 8 dchrmulcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
10 fvexd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ V )
11 eqid ⊢ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) )
12 1 4 5 11 7 dchrf ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
13 12 3adant3r3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑥 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
14 1 4 5 11 8 dchrf ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → 𝑦 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
15 14 3adant3r3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑦 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
16 simpr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐺 ) )
17 1 4 5 11 16 dchrf ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑧 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
18 mulass ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑎 · 𝑏 ) · 𝑐 ) = ( 𝑎 · ( 𝑏 · 𝑐 ) ) )
19 18 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) ∧ ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) → ( ( 𝑎 · 𝑏 ) · 𝑐 ) = ( 𝑎 · ( 𝑏 · 𝑐 ) ) )
20 10 13 15 17 19 caofass ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ∘f · 𝑦 ) ∘f · 𝑧 ) = ( 𝑥 ∘f · ( 𝑦 ∘f · 𝑧 ) ) )
21 simpr1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
22 simpr2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
23 1 4 5 6 21 22 dchrmul ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ∘f · 𝑦 ) )
24 23 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∘f · 𝑧 ) = ( ( 𝑥 ∘f · 𝑦 ) ∘f · 𝑧 ) )
25 1 4 5 6 22 16 dchrmul ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ∘f · 𝑧 ) )
26 25 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ∘f · ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑥 ∘f · ( 𝑦 ∘f · 𝑧 ) ) )
27 20 24 26 3eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∘f · 𝑧 ) = ( 𝑥 ∘f · ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
28 9 3adant3r3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
29 1 4 5 6 28 16 dchrmul ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∘f · 𝑧 ) )
30 1 4 5 6 22 16 dchrmulcl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( Base ‘ 𝐺 ) )
31 1 4 5 6 21 30 dchrmul ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑥 ∘f · ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
32 27 29 31 3eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
33 eqid ⊢ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) )
34 eqid ⊢ ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , 1 , 0 ) ) = ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , 1 , 0 ) )
35 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
36 1 4 5 11 33 34 35 dchr1cl ⊢ ( 𝑁 ∈ ℕ → ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , 1 , 0 ) ) ∈ ( Base ‘ 𝐺 ) )
37 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
38 1 4 5 11 33 34 6 37 dchrmullid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , 1 , 0 ) ) ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
39 eqid ⊢ ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , ( 1 / ( 𝑥 ‘ 𝑘 ) ) , 0 ) ) = ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , ( 1 / ( 𝑥 ‘ 𝑘 ) ) , 0 ) )
40 1 4 5 11 33 34 6 37 39 dchrinvcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , ( 1 / ( 𝑥 ‘ 𝑘 ) ) , 0 ) ) ∈ ( Base ‘ 𝐺 ) ∧ ( ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , ( 1 / ( 𝑥 ‘ 𝑘 ) ) , 0 ) ) ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , 1 , 0 ) ) ) )
41 40 simpld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , ( 1 / ( 𝑥 ‘ 𝑘 ) ) , 0 ) ) ∈ ( Base ‘ 𝐺 ) )
42 40 simprd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , ( 1 / ( 𝑥 ‘ 𝑘 ) ) , 0 ) ) ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑘 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ if ( 𝑘 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) , 1 , 0 ) ) )
43 2 3 9 32 36 38 41 42 isgrpd ⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Grp )
44 fvexd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ V )
45 mulcom ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝑎 · 𝑏 ) = ( 𝑏 · 𝑎 ) )
46 45 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) ) → ( 𝑎 · 𝑏 ) = ( 𝑏 · 𝑎 ) )
47 44 12 14 46 caofcom ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ∘f · 𝑦 ) = ( 𝑦 ∘f · 𝑥 ) )
48 1 4 5 6 7 8 dchrmul ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ∘f · 𝑦 ) )
49 1 4 5 6 8 7 dchrmul ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑦 ∘f · 𝑥 ) )
50 47 48 49 3eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
51 2 3 43 50 isabld ⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )