dchrelbas2

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	dchrval.g	$⊢ G = DChr (N)$
	dchrval.z	$⊢ Z = ℤ / N ℤ$
	dchrval.b	$⊢ B = {Base}_{Z}$
	dchrval.u	$⊢ U = Unit (Z)$
	dchrval.n	$⊢ φ \to N \in ℕ$
	dchrbas.b	$⊢ D = {Base}_{G}$
Assertion	dchrelbas2	$⊢ φ \to (X \in D \leftrightarrow (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in B (X (x) \neq 0 \to x \in U)))$

Proof

Step	Hyp	Ref	Expression
1		dchrval.g	$⊢ G = DChr (N)$
2		dchrval.z	$⊢ Z = ℤ / N ℤ$
3		dchrval.b	$⊢ B = {Base}_{Z}$
4		dchrval.u	$⊢ U = Unit (Z)$
5		dchrval.n	$⊢ φ \to N \in ℕ$
6		dchrbas.b	$⊢ D = {Base}_{G}$
7	1 2 3 4 5 6	dchrelbas	$⊢ φ \to (X \in D \leftrightarrow (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land (B ∖ U) \times \{0\} \subseteq X))$
8		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
9	8 3	mgpbas	$⊢ B = {Base}_{{mulGrp}_{Z}}$
10		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
11		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
12	10 11	mgpbas	$⊢ ℂ = {Base}_{{mulGrp}_{ℂ_{fld}}}$
13	9 12	mhmf	$⊢ X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \to X : B ⟶ ℂ$
14	13	adantl	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to X : B ⟶ ℂ$
15	14	ffund	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to Fun X$
16		funssres	$⊢ (Fun X \land (B ∖ U) \times \{0\} \subseteq X) \to {X ↾}_{dom ((B ∖ U) \times \{0\})} = (B ∖ U) \times \{0\}$
17	15 16	sylan	$⊢ ((φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land (B ∖ U) \times \{0\} \subseteq X) \to {X ↾}_{dom ((B ∖ U) \times \{0\})} = (B ∖ U) \times \{0\}$
18		simpr	$⊢ ((φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land {X ↾}_{dom ((B ∖ U) \times \{0\})} = (B ∖ U) \times \{0\}) \to {X ↾}_{dom ((B ∖ U) \times \{0\})} = (B ∖ U) \times \{0\}$
19		resss	$⊢ {X ↾}_{dom ((B ∖ U) \times \{0\})} \subseteq X$
20	18 19	eqsstrrdi	$⊢ ((φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \land {X ↾}_{dom ((B ∖ U) \times \{0\})} = (B ∖ U) \times \{0\}) \to (B ∖ U) \times \{0\} \subseteq X$
21	17 20	impbida	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to ((B ∖ U) \times \{0\} \subseteq X \leftrightarrow {X ↾}_{dom ((B ∖ U) \times \{0\})} = (B ∖ U) \times \{0\})$
22		0cn	$⊢ 0 \in ℂ$
23		fconst6g	$⊢ 0 \in ℂ \to ((B ∖ U) \times \{0\}) : B ∖ U ⟶ ℂ$
24	22 23	mp1i	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to ((B ∖ U) \times \{0\}) : B ∖ U ⟶ ℂ$
25	24	fdmd	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to dom ((B ∖ U) \times \{0\}) = B ∖ U$
26	25	reseq2d	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to {X ↾}_{dom ((B ∖ U) \times \{0\})} = {X ↾}_{(B ∖ U)}$
27	26	eqeq1d	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to ({X ↾}_{dom ((B ∖ U) \times \{0\})} = (B ∖ U) \times \{0\} \leftrightarrow {X ↾}_{(B ∖ U)} = (B ∖ U) \times \{0\})$
28		difss	$⊢ B ∖ U \subseteq B$
29		fssres	$⊢ (X : B ⟶ ℂ \land B ∖ U \subseteq B) \to ({X ↾}_{(B ∖ U)}) : B ∖ U ⟶ ℂ$
30	14 28 29	sylancl	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to ({X ↾}_{(B ∖ U)}) : B ∖ U ⟶ ℂ$
31	30	ffnd	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to ({X ↾}_{(B ∖ U)}) Fn (B ∖ U)$
32	24	ffnd	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to ((B ∖ U) \times \{0\}) Fn (B ∖ U)$
33		eqfnfv	$⊢ (({X ↾}_{(B ∖ U)}) Fn (B ∖ U) \land ((B ∖ U) \times \{0\}) Fn (B ∖ U)) \to ({X ↾}_{(B ∖ U)} = (B ∖ U) \times \{0\} \leftrightarrow \forall x \in (B ∖ U) ({X ↾}_{(B ∖ U)}) (x) = ((B ∖ U) \times \{0\}) (x))$
34	31 32 33	syl2anc	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to ({X ↾}_{(B ∖ U)} = (B ∖ U) \times \{0\} \leftrightarrow \forall x \in (B ∖ U) ({X ↾}_{(B ∖ U)}) (x) = ((B ∖ U) \times \{0\}) (x))$
35		fvres	$⊢ x \in (B ∖ U) \to ({X ↾}_{(B ∖ U)}) (x) = X (x)$
36		c0ex	$⊢ 0 \in V$
37	36	fvconst2	$⊢ x \in (B ∖ U) \to ((B ∖ U) \times \{0\}) (x) = 0$
38	35 37	eqeq12d	$⊢ x \in (B ∖ U) \to (({X ↾}_{(B ∖ U)}) (x) = ((B ∖ U) \times \{0\}) (x) \leftrightarrow X (x) = 0)$
39	38	ralbiia	$⊢ \forall x \in (B ∖ U) ({X ↾}_{(B ∖ U)}) (x) = ((B ∖ U) \times \{0\}) (x) \leftrightarrow \forall x \in (B ∖ U) X (x) = 0$
40		eldif	$⊢ x \in (B ∖ U) \leftrightarrow (x \in B \land \neg x \in U)$
41	40	imbi1i	$⊢ (x \in (B ∖ U) \to X (x) = 0) \leftrightarrow ((x \in B \land \neg x \in U) \to X (x) = 0)$
42		impexp	$⊢ ((x \in B \land \neg x \in U) \to X (x) = 0) \leftrightarrow (x \in B \to (\neg x \in U \to X (x) = 0))$
43		con1b	$⊢ (\neg x \in U \to X (x) = 0) \leftrightarrow (\neg X (x) = 0 \to x \in U)$
44		df-ne	$⊢ X (x) \neq 0 \leftrightarrow \neg X (x) = 0$
45	44	imbi1i	$⊢ (X (x) \neq 0 \to x \in U) \leftrightarrow (\neg X (x) = 0 \to x \in U)$
46	43 45	bitr4i	$⊢ (\neg x \in U \to X (x) = 0) \leftrightarrow (X (x) \neq 0 \to x \in U)$
47	46	imbi2i	$⊢ (x \in B \to (\neg x \in U \to X (x) = 0)) \leftrightarrow (x \in B \to (X (x) \neq 0 \to x \in U))$
48	41 42 47	3bitri	$⊢ (x \in (B ∖ U) \to X (x) = 0) \leftrightarrow (x \in B \to (X (x) \neq 0 \to x \in U))$
49	48	ralbii2	$⊢ \forall x \in (B ∖ U) X (x) = 0 \leftrightarrow \forall x \in B (X (x) \neq 0 \to x \in U)$
50	39 49	bitri	$⊢ \forall x \in (B ∖ U) ({X ↾}_{(B ∖ U)}) (x) = ((B ∖ U) \times \{0\}) (x) \leftrightarrow \forall x \in B (X (x) \neq 0 \to x \in U)$
51	34 50	bitrdi	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to ({X ↾}_{(B ∖ U)} = (B ∖ U) \times \{0\} \leftrightarrow \forall x \in B (X (x) \neq 0 \to x \in U))$
52	21 27 51	3bitrd	$⊢ (φ \land X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})) \to ((B ∖ U) \times \{0\} \subseteq X \leftrightarrow \forall x \in B (X (x) \neq 0 \to x \in U))$
53	52	pm5.32da	$⊢ φ \to ((X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land (B ∖ U) \times \{0\} \subseteq X) \leftrightarrow (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in B (X (x) \neq 0 \to x \in U)))$
54	7 53	bitrd	$⊢ φ \to (X \in D \leftrightarrow (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in B (X (x) \neq 0 \to x \in U)))$

Metamath Proof Explorer

Theorem dchrelbas2

Proof