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 )