dchrinv

Description: The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of X are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dchrabs.g	$⊢ G = DChr (N)$
	dchrabs.d	$⊢ D = {Base}_{G}$
	dchrabs.x	$⊢ φ \to X \in D$
	dchrinv.i	$⊢ I = {inv}_{g} (G)$
Assertion	dchrinv	$⊢ φ \to I (X) = * \circ X$

Proof

Step	Hyp	Ref	Expression
1		dchrabs.g	$⊢ G = DChr (N)$
2		dchrabs.d	$⊢ D = {Base}_{G}$
3		dchrabs.x	$⊢ φ \to X \in D$
4		dchrinv.i	$⊢ I = {inv}_{g} (G)$
5		eqid	$⊢ ℤ / N ℤ = ℤ / N ℤ$
6		eqid	$⊢ +_{G} = +_{G}$
7		cjf	$⊢ * : ℂ ⟶ ℂ$
8		eqid	$⊢ {Base}_{ℤ / N ℤ} = {Base}_{ℤ / N ℤ}$
9	1 5 2 8 3	dchrf	$⊢ φ \to X : {Base}_{ℤ / N ℤ} ⟶ ℂ$
10		fco	$⊢ (* : ℂ ⟶ ℂ \land X : {Base}_{ℤ / N ℤ} ⟶ ℂ) \to (* \circ X) : {Base}_{ℤ / N ℤ} ⟶ ℂ$
11	7 9 10	sylancr	$⊢ φ \to (* \circ X) : {Base}_{ℤ / N ℤ} ⟶ ℂ$
12		eqid	$⊢ Unit (ℤ / N ℤ) = Unit (ℤ / N ℤ)$
13	1 2	dchrrcl	$⊢ X \in D \to N \in ℕ$
14	3 13	syl	$⊢ φ \to N \in ℕ$
15	1 5 8 12 14 2	dchrelbas3	$⊢ φ \to (X \in D \leftrightarrow (X : {Base}_{ℤ / N ℤ} ⟶ ℂ \land (\forall x \in Unit (ℤ / N ℤ) \forall y \in Unit (ℤ / N ℤ) X (x \cdot_{ℤ / N ℤ} y) = X (x) X (y) \land X (1_{ℤ / N ℤ}) = 1 \land \forall x \in {Base}_{ℤ / N ℤ} (X (x) \neq 0 \to x \in Unit (ℤ / N ℤ)))))$
16	3 15	mpbid	$⊢ φ \to (X : {Base}_{ℤ / N ℤ} ⟶ ℂ \land (\forall x \in Unit (ℤ / N ℤ) \forall y \in Unit (ℤ / N ℤ) X (x \cdot_{ℤ / N ℤ} y) = X (x) X (y) \land X (1_{ℤ / N ℤ}) = 1 \land \forall x \in {Base}_{ℤ / N ℤ} (X (x) \neq 0 \to x \in Unit (ℤ / N ℤ))))$
17	16	simprd	$⊢ φ \to (\forall x \in Unit (ℤ / N ℤ) \forall y \in Unit (ℤ / N ℤ) X (x \cdot_{ℤ / N ℤ} y) = X (x) X (y) \land X (1_{ℤ / N ℤ}) = 1 \land \forall x \in {Base}_{ℤ / N ℤ} (X (x) \neq 0 \to x \in Unit (ℤ / N ℤ)))$
18	17	simp1d	$⊢ φ \to \forall x \in Unit (ℤ / N ℤ) \forall y \in Unit (ℤ / N ℤ) X (x \cdot_{ℤ / N ℤ} y) = X (x) X (y)$
19	18	r19.21bi	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to \forall y \in Unit (ℤ / N ℤ) X (x \cdot_{ℤ / N ℤ} y) = X (x) X (y)$
20	19	r19.21bi	$⊢ ((φ \land x \in Unit (ℤ / N ℤ)) \land y \in Unit (ℤ / N ℤ)) \to X (x \cdot_{ℤ / N ℤ} y) = X (x) X (y)$
21	20	anasss	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to X (x \cdot_{ℤ / N ℤ} y) = X (x) X (y)$
22	21	fveq2d	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to \overline{X (x \cdot_{ℤ / N ℤ} y)} = \overline{X (x) X (y)}$
23	9	adantr	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to X : {Base}_{ℤ / N ℤ} ⟶ ℂ$
24	8 12	unitss	$⊢ Unit (ℤ / N ℤ) \subseteq {Base}_{ℤ / N ℤ}$
25		simprl	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to x \in Unit (ℤ / N ℤ)$
26	24 25	sselid	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to x \in {Base}_{ℤ / N ℤ}$
27	23 26	ffvelrnd	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to X (x) \in ℂ$
28		simprr	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to y \in Unit (ℤ / N ℤ)$
29	24 28	sselid	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to y \in {Base}_{ℤ / N ℤ}$
30	23 29	ffvelrnd	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to X (y) \in ℂ$
31	27 30	cjmuld	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to \overline{X (x) X (y)} = \overline{X (x)} \overline{X (y)}$
32	22 31	eqtrd	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to \overline{X (x \cdot_{ℤ / N ℤ} y)} = \overline{X (x)} \overline{X (y)}$
33	14	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
34	5	zncrng	$⊢ N \in ℕ_{0} \to ℤ / N ℤ \in CRing$
35		crngring	$⊢ ℤ / N ℤ \in CRing \to ℤ / N ℤ \in Ring$
36	33 34 35	3syl	$⊢ φ \to ℤ / N ℤ \in Ring$
37	36	adantr	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to ℤ / N ℤ \in Ring$
38		eqid	$⊢ \cdot_{ℤ / N ℤ} = \cdot_{ℤ / N ℤ}$
39	8 38	ringcl	$⊢ (ℤ / N ℤ \in Ring \land x \in {Base}_{ℤ / N ℤ} \land y \in {Base}_{ℤ / N ℤ}) \to x \cdot_{ℤ / N ℤ} y \in {Base}_{ℤ / N ℤ}$
40	37 26 29 39	syl3anc	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to x \cdot_{ℤ / N ℤ} y \in {Base}_{ℤ / N ℤ}$
41		fvco3	$⊢ (X : {Base}_{ℤ / N ℤ} ⟶ ℂ \land x \cdot_{ℤ / N ℤ} y \in {Base}_{ℤ / N ℤ}) \to (* \circ X) (x \cdot_{ℤ / N ℤ} y) = \overline{X (x \cdot_{ℤ / N ℤ} y)}$
42	23 40 41	syl2anc	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to (* \circ X) (x \cdot_{ℤ / N ℤ} y) = \overline{X (x \cdot_{ℤ / N ℤ} y)}$
43		fvco3	$⊢ (X : {Base}_{ℤ / N ℤ} ⟶ ℂ \land x \in {Base}_{ℤ / N ℤ}) \to (* \circ X) (x) = \overline{X (x)}$
44	23 26 43	syl2anc	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to (* \circ X) (x) = \overline{X (x)}$
45		fvco3	$⊢ (X : {Base}_{ℤ / N ℤ} ⟶ ℂ \land y \in {Base}_{ℤ / N ℤ}) \to (* \circ X) (y) = \overline{X (y)}$
46	23 29 45	syl2anc	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to (* \circ X) (y) = \overline{X (y)}$
47	44 46	oveq12d	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to (* \circ X) (x) (* \circ X) (y) = \overline{X (x)} \overline{X (y)}$
48	32 42 47	3eqtr4d	$⊢ (φ \land (x \in Unit (ℤ / N ℤ) \land y \in Unit (ℤ / N ℤ))) \to (* \circ X) (x \cdot_{ℤ / N ℤ} y) = (* \circ X) (x) (* \circ X) (y)$
49	48	ralrimivva	$⊢ φ \to \forall x \in Unit (ℤ / N ℤ) \forall y \in Unit (ℤ / N ℤ) (* \circ X) (x \cdot_{ℤ / N ℤ} y) = (* \circ X) (x) (* \circ X) (y)$
50		eqid	$⊢ 1_{ℤ / N ℤ} = 1_{ℤ / N ℤ}$
51	8 50	ringidcl	$⊢ ℤ / N ℤ \in Ring \to 1_{ℤ / N ℤ} \in {Base}_{ℤ / N ℤ}$
52	36 51	syl	$⊢ φ \to 1_{ℤ / N ℤ} \in {Base}_{ℤ / N ℤ}$
53		fvco3	$⊢ (X : {Base}_{ℤ / N ℤ} ⟶ ℂ \land 1_{ℤ / N ℤ} \in {Base}_{ℤ / N ℤ}) \to (* \circ X) (1_{ℤ / N ℤ}) = \overline{X (1_{ℤ / N ℤ})}$
54	9 52 53	syl2anc	$⊢ φ \to (* \circ X) (1_{ℤ / N ℤ}) = \overline{X (1_{ℤ / N ℤ})}$
55	17	simp2d	$⊢ φ \to X (1_{ℤ / N ℤ}) = 1$
56	55	fveq2d	$⊢ φ \to \overline{X (1_{ℤ / N ℤ})} = \overline{1}$
57		1re	$⊢ 1 \in ℝ$
58		cjre	$⊢ 1 \in ℝ \to \overline{1} = 1$
59	57 58	ax-mp	$⊢ \overline{1} = 1$
60	56 59	eqtrdi	$⊢ φ \to \overline{X (1_{ℤ / N ℤ})} = 1$
61	54 60	eqtrd	$⊢ φ \to (* \circ X) (1_{ℤ / N ℤ}) = 1$
62	17	simp3d	$⊢ φ \to \forall x \in {Base}_{ℤ / N ℤ} (X (x) \neq 0 \to x \in Unit (ℤ / N ℤ))$
63	9 43	sylan	$⊢ (φ \land x \in {Base}_{ℤ / N ℤ}) \to (* \circ X) (x) = \overline{X (x)}$
64		cj0	$⊢ \overline{0} = 0$
65	64	eqcomi	$⊢ 0 = \overline{0}$
66	65	a1i	$⊢ (φ \land x \in {Base}_{ℤ / N ℤ}) \to 0 = \overline{0}$
67	63 66	eqeq12d	$⊢ (φ \land x \in {Base}_{ℤ / N ℤ}) \to ((* \circ X) (x) = 0 \leftrightarrow \overline{X (x)} = \overline{0})$
68	9	ffvelrnda	$⊢ (φ \land x \in {Base}_{ℤ / N ℤ}) \to X (x) \in ℂ$
69		0cn	$⊢ 0 \in ℂ$
70		cj11	$⊢ (X (x) \in ℂ \land 0 \in ℂ) \to (\overline{X (x)} = \overline{0} \leftrightarrow X (x) = 0)$
71	68 69 70	sylancl	$⊢ (φ \land x \in {Base}_{ℤ / N ℤ}) \to (\overline{X (x)} = \overline{0} \leftrightarrow X (x) = 0)$
72	67 71	bitrd	$⊢ (φ \land x \in {Base}_{ℤ / N ℤ}) \to ((* \circ X) (x) = 0 \leftrightarrow X (x) = 0)$
73	72	necon3bid	$⊢ (φ \land x \in {Base}_{ℤ / N ℤ}) \to ((* \circ X) (x) \neq 0 \leftrightarrow X (x) \neq 0)$
74	73	imbi1d	$⊢ (φ \land x \in {Base}_{ℤ / N ℤ}) \to (((* \circ X) (x) \neq 0 \to x \in Unit (ℤ / N ℤ)) \leftrightarrow (X (x) \neq 0 \to x \in Unit (ℤ / N ℤ)))$
75	74	ralbidva	$⊢ φ \to (\forall x \in {Base}_{ℤ / N ℤ} ((* \circ X) (x) \neq 0 \to x \in Unit (ℤ / N ℤ)) \leftrightarrow \forall x \in {Base}_{ℤ / N ℤ} (X (x) \neq 0 \to x \in Unit (ℤ / N ℤ)))$
76	62 75	mpbird	$⊢ φ \to \forall x \in {Base}_{ℤ / N ℤ} ((* \circ X) (x) \neq 0 \to x \in Unit (ℤ / N ℤ))$
77	49 61 76	3jca	$⊢ φ \to (\forall x \in Unit (ℤ / N ℤ) \forall y \in Unit (ℤ / N ℤ) (* \circ X) (x \cdot_{ℤ / N ℤ} y) = (* \circ X) (x) (* \circ X) (y) \land (* \circ X) (1_{ℤ / N ℤ}) = 1 \land \forall x \in {Base}_{ℤ / N ℤ} ((* \circ X) (x) \neq 0 \to x \in Unit (ℤ / N ℤ)))$
78	1 5 8 12 14 2	dchrelbas3	$⊢ φ \to (* \circ X \in D \leftrightarrow ((* \circ X) : {Base}_{ℤ / N ℤ} ⟶ ℂ \land (\forall x \in Unit (ℤ / N ℤ) \forall y \in Unit (ℤ / N ℤ) (* \circ X) (x \cdot_{ℤ / N ℤ} y) = (* \circ X) (x) (* \circ X) (y) \land (* \circ X) (1_{ℤ / N ℤ}) = 1 \land \forall x \in {Base}_{ℤ / N ℤ} ((* \circ X) (x) \neq 0 \to x \in Unit (ℤ / N ℤ)))))$
79	11 77 78	mpbir2and	$⊢ φ \to * \circ X \in D$
80	1 5 2 6 3 79	dchrmul	$⊢ φ \to X +_{G} (* \circ X) = X \times_{f} (* \circ X)$
81	80	adantr	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to X +_{G} (* \circ X) = X \times_{f} (* \circ X)$
82	81	fveq1d	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to (X +_{G} (* \circ X)) (x) = (X \times_{f} (* \circ X)) (x)$
83	24	sseli	$⊢ x \in Unit (ℤ / N ℤ) \to x \in {Base}_{ℤ / N ℤ}$
84	83 63	sylan2	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to (* \circ X) (x) = \overline{X (x)}$
85	84	oveq2d	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to X (x) (* \circ X) (x) = X (x) \overline{X (x)}$
86	83 68	sylan2	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to X (x) \in ℂ$
87	86	absvalsqd	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to {\|X (x)\|}^{2} = X (x) \overline{X (x)}$
88	3	adantr	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to X \in D$
89		simpr	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to x \in Unit (ℤ / N ℤ)$
90	1 2 88 5 12 89	dchrabs	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to \|X (x)\| = 1$
91	90	oveq1d	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to {\|X (x)\|}^{2} = 1^{2}$
92		sq1	$⊢ 1^{2} = 1$
93	91 92	eqtrdi	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to {\|X (x)\|}^{2} = 1$
94	85 87 93	3eqtr2d	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to X (x) (* \circ X) (x) = 1$
95	9	adantr	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to X : {Base}_{ℤ / N ℤ} ⟶ ℂ$
96	95	ffnd	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to X Fn {Base}_{ℤ / N ℤ}$
97	11	ffnd	$⊢ φ \to (* \circ X) Fn {Base}_{ℤ / N ℤ}$
98	97	adantr	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to (* \circ X) Fn {Base}_{ℤ / N ℤ}$
99		fvexd	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to {Base}_{ℤ / N ℤ} \in V$
100	83	adantl	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to x \in {Base}_{ℤ / N ℤ}$
101		fnfvof	$⊢ ((X Fn {Base}_{ℤ / N ℤ} \land (* \circ X) Fn {Base}_{ℤ / N ℤ}) \land ({Base}_{ℤ / N ℤ} \in V \land x \in {Base}_{ℤ / N ℤ})) \to (X \times_{f} (* \circ X)) (x) = X (x) (* \circ X) (x)$
102	96 98 99 100 101	syl22anc	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to (X \times_{f} (* \circ X)) (x) = X (x) (* \circ X) (x)$
103		eqid	$⊢ 0_{G} = 0_{G}$
104	14	adantr	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to N \in ℕ$
105	1 5 103 12 104 89	dchr1	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to 0_{G} (x) = 1$
106	94 102 105	3eqtr4d	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to (X \times_{f} (* \circ X)) (x) = 0_{G} (x)$
107	82 106	eqtrd	$⊢ (φ \land x \in Unit (ℤ / N ℤ)) \to (X +_{G} (* \circ X)) (x) = 0_{G} (x)$
108	107	ralrimiva	$⊢ φ \to \forall x \in Unit (ℤ / N ℤ) (X +_{G} (* \circ X)) (x) = 0_{G} (x)$
109	1 5 2 6 3 79	dchrmulcl	$⊢ φ \to X +_{G} (* \circ X) \in D$
110	1	dchrabl	$⊢ N \in ℕ \to G \in Abel$
111		ablgrp	$⊢ G \in Abel \to G \in Grp$
112	14 110 111	3syl	$⊢ φ \to G \in Grp$
113	2 103	grpidcl	$⊢ G \in Grp \to 0_{G} \in D$
114	112 113	syl	$⊢ φ \to 0_{G} \in D$
115	1 5 2 12 109 114	dchreq	$⊢ φ \to (X +_{G} (* \circ X) = 0_{G} \leftrightarrow \forall x \in Unit (ℤ / N ℤ) (X +_{G} (* \circ X)) (x) = 0_{G} (x))$
116	108 115	mpbird	$⊢ φ \to X +_{G} (* \circ X) = 0_{G}$
117	2 6 103 4	grpinvid1	$⊢ (G \in Grp \land X \in D \land * \circ X \in D) \to (I (X) = * \circ X \leftrightarrow X +_{G} (* \circ X) = 0_{G})$
118	112 3 79 117	syl3anc	$⊢ φ \to (I (X) = * \circ X \leftrightarrow X +_{G} (* \circ X) = 0_{G})$
119	116 118	mpbird	$⊢ φ \to I (X) = * \circ X$

Metamath Proof Explorer

Theorem dchrinv

Proof