dchrelbas4

Description: A Dirichlet character is a monoid homomorphism from the multiplicative monoid on Z/nZ to the multiplicative monoid of CC , which is zero off the group of units of Z/nZ . (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	dchrmhm.g	$⊢ G = DChr (N)$
	dchrmhm.z	$⊢ Z = ℤ / N ℤ$
	dchrmhm.b	$⊢ D = {Base}_{G}$
	dchrelbas4.l	$⊢ L = ℤRHom (Z)$
Assertion	dchrelbas4	$⊢ X \in D \leftrightarrow (N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in ℤ (1 < x \gcd N \to X (L (x)) = 0))$

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	$⊢ G = DChr (N)$
2		dchrmhm.z	$⊢ Z = ℤ / N ℤ$
3		dchrmhm.b	$⊢ D = {Base}_{G}$
4		dchrelbas4.l	$⊢ L = ℤRHom (Z)$
5	1 3	dchrrcl	$⊢ X \in D \to N \in ℕ$
6		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
7		eqid	$⊢ Unit (Z) = Unit (Z)$
8		id	$⊢ N \in ℕ \to N \in ℕ$
9	1 2 6 7 8 3	dchrelbas2	$⊢ N \in ℕ \to (X \in D \leftrightarrow (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall y \in {Base}_{Z} (X (y) \neq 0 \to y \in Unit (Z))))$
10		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
11	10	adantr	$⊢ (N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to N \in ℕ_{0}$
12	2 6 4	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} {Base}_{Z}$
13		fveq2	$⊢ L (x) = y \to X (L (x)) = X (y)$
14	13	neeq1d	$⊢ L (x) = y \to (X (L (x)) \neq 0 \leftrightarrow X (y) \neq 0)$
15		eleq1	$⊢ L (x) = y \to (L (x) \in Unit (Z) \leftrightarrow y \in Unit (Z))$
16	14 15	imbi12d	$⊢ L (x) = y \to ((X (L (x)) \neq 0 \to L (x) \in Unit (Z)) \leftrightarrow (X (y) \neq 0 \to y \in Unit (Z)))$
17	16	cbvfo	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Z} \to (\forall x \in ℤ (X (L (x)) \neq 0 \to L (x) \in Unit (Z)) \leftrightarrow \forall y \in {Base}_{Z} (X (y) \neq 0 \to y \in Unit (Z)))$
18	11 12 17	3syl	$⊢ (N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to (\forall x \in ℤ (X (L (x)) \neq 0 \to L (x) \in Unit (Z)) \leftrightarrow \forall y \in {Base}_{Z} (X (y) \neq 0 \to y \in Unit (Z)))$
19		df-ne	$⊢ X (L (x)) \neq 0 \leftrightarrow \neg X (L (x)) = 0$
20	19	a1i	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to (X (L (x)) \neq 0 \leftrightarrow \neg X (L (x)) = 0)$
21	2 7 4	znunit	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to (L (x) \in Unit (Z) \leftrightarrow x \gcd N = 1)$
22	11 21	sylan	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to (L (x) \in Unit (Z) \leftrightarrow x \gcd N = 1)$
23		1red	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to 1 \in ℝ$
24		simpr	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to x \in ℤ$
25		simpll	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to N \in ℕ$
26	25	nnzd	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to N \in ℤ$
27		nnne0	$⊢ N \in ℕ \to N \neq 0$
28		simpr	$⊢ (x = 0 \land N = 0) \to N = 0$
29	28	necon3ai	$⊢ N \neq 0 \to \neg (x = 0 \land N = 0)$
30	25 27 29	3syl	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to \neg (x = 0 \land N = 0)$
31		gcdn0cl	$⊢ ((x \in ℤ \land N \in ℤ) \land \neg (x = 0 \land N = 0)) \to x \gcd N \in ℕ$
32	24 26 30 31	syl21anc	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to x \gcd N \in ℕ$
33	32	nnred	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to x \gcd N \in ℝ$
34	32	nnge1d	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to 1 \leq x \gcd N$
35	23 33 34	leltned	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to (1 < x \gcd N \leftrightarrow x \gcd N \neq 1)$
36	35	necon2bbid	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to (x \gcd N = 1 \leftrightarrow \neg 1 < x \gcd N)$
37	22 36	bitrd	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to (L (x) \in Unit (Z) \leftrightarrow \neg 1 < x \gcd N)$
38	20 37	imbi12d	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to ((X (L (x)) \neq 0 \to L (x) \in Unit (Z)) \leftrightarrow (\neg X (L (x)) = 0 \to \neg 1 < x \gcd N))$
39		con34b	$⊢ (1 < x \gcd N \to X (L (x)) = 0) \leftrightarrow (\neg X (L (x)) = 0 \to \neg 1 < x \gcd N)$
40	38 39	bitr4di	$⊢ ((N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land x \in ℤ) \to ((X (L (x)) \neq 0 \to L (x) \in Unit (Z)) \leftrightarrow (1 < x \gcd N \to X (L (x)) = 0))$
41	40	ralbidva	$⊢ (N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to (\forall x \in ℤ (X (L (x)) \neq 0 \to L (x) \in Unit (Z)) \leftrightarrow \forall x \in ℤ (1 < x \gcd N \to X (L (x)) = 0))$
42	18 41	bitr3d	$⊢ (N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to (\forall y \in {Base}_{Z} (X (y) \neq 0 \to y \in Unit (Z)) \leftrightarrow \forall x \in ℤ (1 < x \gcd N \to X (L (x)) = 0))$
43	42	pm5.32da	$⊢ N \in ℕ \to ((X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall y \in {Base}_{Z} (X (y) \neq 0 \to y \in Unit (Z))) \leftrightarrow (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in ℤ (1 < x \gcd N \to X (L (x)) = 0)))$
44	9 43	bitrd	$⊢ N \in ℕ \to (X \in D \leftrightarrow (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in ℤ (1 < x \gcd N \to X (L (x)) = 0)))$
45	5 44	biadanii	$⊢ X \in D \leftrightarrow (N \in ℕ \land (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in ℤ (1 < x \gcd N \to X (L (x)) = 0)))$
46		3anass	$⊢ (N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in ℤ (1 < x \gcd N \to X (L (x)) = 0)) \leftrightarrow (N \in ℕ \land (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in ℤ (1 < x \gcd N \to X (L (x)) = 0)))$
47	45 46	bitr4i	$⊢ X \in D \leftrightarrow (N \in ℕ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in ℤ (1 < x \gcd N \to X (L (x)) = 0))$

Metamath Proof Explorer

Theorem dchrelbas4

Proof