dchrelbasd

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, 28-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}$
	dchrelbasd.1	$⊢ k = x \to X = A$
	dchrelbasd.2	$⊢ k = y \to X = C$
	dchrelbasd.3	$⊢ k = x \cdot_{Z} y \to X = E$
	dchrelbasd.4	$⊢ k = 1_{Z} \to X = Y$
	dchrelbasd.5	$⊢ (φ \land k \in U) \to X \in ℂ$
	dchrelbasd.6	$⊢ (φ \land (x \in U \land y \in U)) \to E = A C$
	dchrelbasd.7	$⊢ φ \to Y = 1$
Assertion	dchrelbasd	$⊢ φ \to (k \in B ⟼ if (k \in U, X, 0)) \in D$

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		dchrelbasd.1	$⊢ k = x \to X = A$
8		dchrelbasd.2	$⊢ k = y \to X = C$
9		dchrelbasd.3	$⊢ k = x \cdot_{Z} y \to X = E$
10		dchrelbasd.4	$⊢ k = 1_{Z} \to X = Y$
11		dchrelbasd.5	$⊢ (φ \land k \in U) \to X \in ℂ$
12		dchrelbasd.6	$⊢ (φ \land (x \in U \land y \in U)) \to E = A C$
13		dchrelbasd.7	$⊢ φ \to Y = 1$
14	11	adantlr	$⊢ ((φ \land k \in B) \land k \in U) \to X \in ℂ$
15		0cnd	$⊢ ((φ \land k \in B) \land \neg k \in U) \to 0 \in ℂ$
16	14 15	ifclda	$⊢ (φ \land k \in B) \to if (k \in U, X, 0) \in ℂ$
17	16	fmpttd	$⊢ φ \to (k \in B ⟼ if (k \in U, X, 0)) : B ⟶ ℂ$
18	5	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
19	2	zncrng	$⊢ N \in ℕ_{0} \to Z \in CRing$
20		crngring	$⊢ Z \in CRing \to Z \in Ring$
21	18 19 20	3syl	$⊢ φ \to Z \in Ring$
22		eqid	$⊢ \cdot_{Z} = \cdot_{Z}$
23	4 22	unitmulcl	$⊢ (Z \in Ring \land x \in U \land y \in U) \to x \cdot_{Z} y \in U$
24	23	3expb	$⊢ (Z \in Ring \land (x \in U \land y \in U)) \to x \cdot_{Z} y \in U$
25	21 24	sylan	$⊢ (φ \land (x \in U \land y \in U)) \to x \cdot_{Z} y \in U$
26	25	iftrued	$⊢ (φ \land (x \in U \land y \in U)) \to if (x \cdot_{Z} y \in U, E, 0) = E$
27	26 12	eqtrd	$⊢ (φ \land (x \in U \land y \in U)) \to if (x \cdot_{Z} y \in U, E, 0) = A C$
28		eqid	$⊢ (k \in B ⟼ if (k \in U, X, 0)) = (k \in B ⟼ if (k \in U, X, 0))$
29		eleq1	$⊢ k = x \cdot_{Z} y \to (k \in U \leftrightarrow x \cdot_{Z} y \in U)$
30	29 9	ifbieq1d	$⊢ k = x \cdot_{Z} y \to if (k \in U, X, 0) = if (x \cdot_{Z} y \in U, E, 0)$
31	3 4	unitss	$⊢ U \subseteq B$
32	31 25	sseldi	$⊢ (φ \land (x \in U \land y \in U)) \to x \cdot_{Z} y \in B$
33	9	eleq1d	$⊢ k = x \cdot_{Z} y \to (X \in ℂ \leftrightarrow E \in ℂ)$
34	11	ralrimiva	$⊢ φ \to \forall k \in U X \in ℂ$
35	34	adantr	$⊢ (φ \land (x \in U \land y \in U)) \to \forall k \in U X \in ℂ$
36	33 35 25	rspcdva	$⊢ (φ \land (x \in U \land y \in U)) \to E \in ℂ$
37	26 36	eqeltrd	$⊢ (φ \land (x \in U \land y \in U)) \to if (x \cdot_{Z} y \in U, E, 0) \in ℂ$
38	28 30 32 37	fvmptd3	$⊢ (φ \land (x \in U \land y \in U)) \to (k \in B ⟼ if (k \in U, X, 0)) (x \cdot_{Z} y) = if (x \cdot_{Z} y \in U, E, 0)$
39		eleq1	$⊢ k = x \to (k \in U \leftrightarrow x \in U)$
40	39 7	ifbieq1d	$⊢ k = x \to if (k \in U, X, 0) = if (x \in U, A, 0)$
41		simprl	$⊢ (φ \land (x \in U \land y \in U)) \to x \in U$
42	31 41	sseldi	$⊢ (φ \land (x \in U \land y \in U)) \to x \in B$
43		iftrue	$⊢ x \in U \to if (x \in U, A, 0) = A$
44	43	ad2antrl	$⊢ (φ \land (x \in U \land y \in U)) \to if (x \in U, A, 0) = A$
45	7	eleq1d	$⊢ k = x \to (X \in ℂ \leftrightarrow A \in ℂ)$
46	45 35 41	rspcdva	$⊢ (φ \land (x \in U \land y \in U)) \to A \in ℂ$
47	44 46	eqeltrd	$⊢ (φ \land (x \in U \land y \in U)) \to if (x \in U, A, 0) \in ℂ$
48	28 40 42 47	fvmptd3	$⊢ (φ \land (x \in U \land y \in U)) \to (k \in B ⟼ if (k \in U, X, 0)) (x) = if (x \in U, A, 0)$
49	48 44	eqtrd	$⊢ (φ \land (x \in U \land y \in U)) \to (k \in B ⟼ if (k \in U, X, 0)) (x) = A$
50		eleq1	$⊢ k = y \to (k \in U \leftrightarrow y \in U)$
51	50 8	ifbieq1d	$⊢ k = y \to if (k \in U, X, 0) = if (y \in U, C, 0)$
52		simprr	$⊢ (φ \land (x \in U \land y \in U)) \to y \in U$
53	31 52	sseldi	$⊢ (φ \land (x \in U \land y \in U)) \to y \in B$
54		iftrue	$⊢ y \in U \to if (y \in U, C, 0) = C$
55	54	ad2antll	$⊢ (φ \land (x \in U \land y \in U)) \to if (y \in U, C, 0) = C$
56	8	eleq1d	$⊢ k = y \to (X \in ℂ \leftrightarrow C \in ℂ)$
57	56 35 52	rspcdva	$⊢ (φ \land (x \in U \land y \in U)) \to C \in ℂ$
58	55 57	eqeltrd	$⊢ (φ \land (x \in U \land y \in U)) \to if (y \in U, C, 0) \in ℂ$
59	28 51 53 58	fvmptd3	$⊢ (φ \land (x \in U \land y \in U)) \to (k \in B ⟼ if (k \in U, X, 0)) (y) = if (y \in U, C, 0)$
60	59 55	eqtrd	$⊢ (φ \land (x \in U \land y \in U)) \to (k \in B ⟼ if (k \in U, X, 0)) (y) = C$
61	49 60	oveq12d	$⊢ (φ \land (x \in U \land y \in U)) \to (k \in B ⟼ if (k \in U, X, 0)) (x) (k \in B ⟼ if (k \in U, X, 0)) (y) = A C$
62	27 38 61	3eqtr4d	$⊢ (φ \land (x \in U \land y \in U)) \to (k \in B ⟼ if (k \in U, X, 0)) (x \cdot_{Z} y) = (k \in B ⟼ if (k \in U, X, 0)) (x) (k \in B ⟼ if (k \in U, X, 0)) (y)$
63	62	ralrimivva	$⊢ φ \to \forall x \in U \forall y \in U (k \in B ⟼ if (k \in U, X, 0)) (x \cdot_{Z} y) = (k \in B ⟼ if (k \in U, X, 0)) (x) (k \in B ⟼ if (k \in U, X, 0)) (y)$
64		eleq1	$⊢ k = 1_{Z} \to (k \in U \leftrightarrow 1_{Z} \in U)$
65	64 10	ifbieq1d	$⊢ k = 1_{Z} \to if (k \in U, X, 0) = if (1_{Z} \in U, Y, 0)$
66		eqid	$⊢ 1_{Z} = 1_{Z}$
67	4 66	1unit	$⊢ Z \in Ring \to 1_{Z} \in U$
68	21 67	syl	$⊢ φ \to 1_{Z} \in U$
69	31 68	sseldi	$⊢ φ \to 1_{Z} \in B$
70	68	iftrued	$⊢ φ \to if (1_{Z} \in U, Y, 0) = Y$
71	70 13	eqtrd	$⊢ φ \to if (1_{Z} \in U, Y, 0) = 1$
72		ax-1cn	$⊢ 1 \in ℂ$
73	71 72	eqeltrdi	$⊢ φ \to if (1_{Z} \in U, Y, 0) \in ℂ$
74	28 65 69 73	fvmptd3	$⊢ φ \to (k \in B ⟼ if (k \in U, X, 0)) (1_{Z}) = if (1_{Z} \in U, Y, 0)$
75	74 71	eqtrd	$⊢ φ \to (k \in B ⟼ if (k \in U, X, 0)) (1_{Z}) = 1$
76		simpr	$⊢ (φ \land x \in B) \to x \in B$
77	45	rspcv	$⊢ x \in U \to (\forall k \in U X \in ℂ \to A \in ℂ)$
78	34 77	mpan9	$⊢ (φ \land x \in U) \to A \in ℂ$
79	78	adantlr	$⊢ ((φ \land x \in B) \land x \in U) \to A \in ℂ$
80		0cnd	$⊢ ((φ \land x \in B) \land \neg x \in U) \to 0 \in ℂ$
81	79 80	ifclda	$⊢ (φ \land x \in B) \to if (x \in U, A, 0) \in ℂ$
82	28 40 76 81	fvmptd3	$⊢ (φ \land x \in B) \to (k \in B ⟼ if (k \in U, X, 0)) (x) = if (x \in U, A, 0)$
83	82	neeq1d	$⊢ (φ \land x \in B) \to ((k \in B ⟼ if (k \in U, X, 0)) (x) \neq 0 \leftrightarrow if (x \in U, A, 0) \neq 0)$
84		iffalse	$⊢ \neg x \in U \to if (x \in U, A, 0) = 0$
85	84	necon1ai	$⊢ if (x \in U, A, 0) \neq 0 \to x \in U$
86	83 85	syl6bi	$⊢ (φ \land x \in B) \to ((k \in B ⟼ if (k \in U, X, 0)) (x) \neq 0 \to x \in U)$
87	86	ralrimiva	$⊢ φ \to \forall x \in B ((k \in B ⟼ if (k \in U, X, 0)) (x) \neq 0 \to x \in U)$
88	63 75 87	3jca	$⊢ φ \to (\forall x \in U \forall y \in U (k \in B ⟼ if (k \in U, X, 0)) (x \cdot_{Z} y) = (k \in B ⟼ if (k \in U, X, 0)) (x) (k \in B ⟼ if (k \in U, X, 0)) (y) \land (k \in B ⟼ if (k \in U, X, 0)) (1_{Z}) = 1 \land \forall x \in B ((k \in B ⟼ if (k \in U, X, 0)) (x) \neq 0 \to x \in U))$
89	1 2 3 4 5 6	dchrelbas3	$⊢ φ \to ((k \in B ⟼ if (k \in U, X, 0)) \in D \leftrightarrow ((k \in B ⟼ if (k \in U, X, 0)) : B ⟶ ℂ \land (\forall x \in U \forall y \in U (k \in B ⟼ if (k \in U, X, 0)) (x \cdot_{Z} y) = (k \in B ⟼ if (k \in U, X, 0)) (x) (k \in B ⟼ if (k \in U, X, 0)) (y) \land (k \in B ⟼ if (k \in U, X, 0)) (1_{Z}) = 1 \land \forall x \in B ((k \in B ⟼ if (k \in U, X, 0)) (x) \neq 0 \to x \in U))))$
90	17 88 89	mpbir2and	$⊢ φ \to (k \in B ⟼ if (k \in U, X, 0)) \in D$

Metamath Proof Explorer

Theorem dchrelbasd

Proof