dchrabl

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

		Ref	Expression
	Hypothesis	dchrabl.g	$⊢ G = DChr (N)$
	Assertion	dchrabl	$⊢ N \in ℕ \to G \in Abel$

Proof

Step	Hyp	Ref	Expression
1		dchrabl.g	$⊢ G = DChr (N)$
2		eqidd	$⊢ N \in ℕ \to {Base}_{G} = {Base}_{G}$
3		eqidd	$⊢ N \in ℕ \to +_{G} = +_{G}$
4		eqid	$⊢ ℤ / N ℤ = ℤ / N ℤ$
5		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6		eqid	$⊢ +_{G} = +_{G}$
7		simp2	$⊢ (N \in ℕ \land x \in {Base}_{G} \land y \in {Base}_{G}) \to x \in {Base}_{G}$
8		simp3	$⊢ (N \in ℕ \land x \in {Base}_{G} \land y \in {Base}_{G}) \to y \in {Base}_{G}$
9	1 4 5 6 7 8	dchrmulcl	$⊢ (N \in ℕ \land x \in {Base}_{G} \land y \in {Base}_{G}) \to x +_{G} y \in {Base}_{G}$
10		fvexd	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to {Base}_{ℤ / N ℤ} \in V$
11		eqid	$⊢ {Base}_{ℤ / N ℤ} = {Base}_{ℤ / N ℤ}$
12	1 4 5 11 7	dchrf	$⊢ (N \in ℕ \land x \in {Base}_{G} \land y \in {Base}_{G}) \to x : {Base}_{ℤ / N ℤ} ⟶ ℂ$
13	12	3adant3r3	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to x : {Base}_{ℤ / N ℤ} ⟶ ℂ$
14	1 4 5 11 8	dchrf	$⊢ (N \in ℕ \land x \in {Base}_{G} \land y \in {Base}_{G}) \to y : {Base}_{ℤ / N ℤ} ⟶ ℂ$
15	14	3adant3r3	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to y : {Base}_{ℤ / N ℤ} ⟶ ℂ$
16		simpr3	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to z \in {Base}_{G}$
17	1 4 5 11 16	dchrf	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to z : {Base}_{ℤ / N ℤ} ⟶ ℂ$
18		mulass	$⊢ (a \in ℂ \land b \in ℂ \land c \in ℂ) \to a b c = a b c$
19	18	adantl	$⊢ ((N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \land (a \in ℂ \land b \in ℂ \land c \in ℂ)) \to a b c = a b c$
20	10 13 15 17 19	caofass	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to (x \times_{f} y) \times_{f} z = x \times_{f} (y \times_{f} z)$
21		simpr1	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to x \in {Base}_{G}$
22		simpr2	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to y \in {Base}_{G}$
23	1 4 5 6 21 22	dchrmul	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to x +_{G} y = x \times_{f} y$
24	23	oveq1d	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to (x +_{G} y) \times_{f} z = (x \times_{f} y) \times_{f} z$
25	1 4 5 6 22 16	dchrmul	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to y +_{G} z = y \times_{f} z$
26	25	oveq2d	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to x \times_{f} (y +_{G} z) = x \times_{f} (y \times_{f} z)$
27	20 24 26	3eqtr4d	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to (x +_{G} y) \times_{f} z = x \times_{f} (y +_{G} z)$
28	9	3adant3r3	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to x +_{G} y \in {Base}_{G}$
29	1 4 5 6 28 16	dchrmul	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to (x +_{G} y) +_{G} z = (x +_{G} y) \times_{f} z$
30	1 4 5 6 22 16	dchrmulcl	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to y +_{G} z \in {Base}_{G}$
31	1 4 5 6 21 30	dchrmul	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to x +_{G} (y +_{G} z) = x \times_{f} (y +_{G} z)$
32	27 29 31	3eqtr4d	$⊢ (N \in ℕ \land (x \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to (x +_{G} y) +_{G} z = x +_{G} (y +_{G} z)$
33		eqid	$⊢ Unit (ℤ / N ℤ) = Unit (ℤ / N ℤ)$
34		eqid	$⊢ (k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), 1, 0)) = (k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), 1, 0))$
35		id	$⊢ N \in ℕ \to N \in ℕ$
36	1 4 5 11 33 34 35	dchr1cl	$⊢ N \in ℕ \to (k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), 1, 0)) \in {Base}_{G}$
37		simpr	$⊢ (N \in ℕ \land x \in {Base}_{G}) \to x \in {Base}_{G}$
38	1 4 5 11 33 34 6 37	dchrmulid2	$⊢ (N \in ℕ \land x \in {Base}_{G}) \to (k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), 1, 0)) +_{G} x = x$
39		eqid	$⊢ (k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), \frac{1}{x (k)}, 0)) = (k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), \frac{1}{x (k)}, 0))$
40	1 4 5 11 33 34 6 37 39	dchrinvcl	$⊢ (N \in ℕ \land x \in {Base}_{G}) \to ((k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), \frac{1}{x (k)}, 0)) \in {Base}_{G} \land (k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), \frac{1}{x (k)}, 0)) +_{G} x = (k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), 1, 0)))$
41	40	simpld	$⊢ (N \in ℕ \land x \in {Base}_{G}) \to (k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), \frac{1}{x (k)}, 0)) \in {Base}_{G}$
42	40	simprd	$⊢ (N \in ℕ \land x \in {Base}_{G}) \to (k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), \frac{1}{x (k)}, 0)) +_{G} x = (k \in {Base}_{ℤ / N ℤ} ⟼ if (k \in Unit (ℤ / N ℤ), 1, 0))$
43	2 3 9 32 36 38 41 42	isgrpd	$⊢ N \in ℕ \to G \in Grp$
44		fvexd	$⊢ (N \in ℕ \land x \in {Base}_{G} \land y \in {Base}_{G}) \to {Base}_{ℤ / N ℤ} \in V$
45		mulcom	$⊢ (a \in ℂ \land b \in ℂ) \to a b = b a$
46	45	adantl	$⊢ ((N \in ℕ \land x \in {Base}_{G} \land y \in {Base}_{G}) \land (a \in ℂ \land b \in ℂ)) \to a b = b a$
47	44 12 14 46	caofcom	$⊢ (N \in ℕ \land x \in {Base}_{G} \land y \in {Base}_{G}) \to x \times_{f} y = y \times_{f} x$
48	1 4 5 6 7 8	dchrmul	$⊢ (N \in ℕ \land x \in {Base}_{G} \land y \in {Base}_{G}) \to x +_{G} y = x \times_{f} y$
49	1 4 5 6 8 7	dchrmul	$⊢ (N \in ℕ \land x \in {Base}_{G} \land y \in {Base}_{G}) \to y +_{G} x = y \times_{f} x$
50	47 48 49	3eqtr4d	$⊢ (N \in ℕ \land x \in {Base}_{G} \land y \in {Base}_{G}) \to x +_{G} y = y +_{G} x$
51	2 3 43 50	isabld	$⊢ N \in ℕ \to G \in Abel$

Metamath Proof Explorer

Theorem dchrabl

Proof