dchrinvcl

Description: Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	dchrmhm.g	$⊢ G = DChr (N)$
	dchrmhm.z	$⊢ Z = ℤ / N ℤ$
	dchrmhm.b	$⊢ D = {Base}_{G}$
	dchrn0.b	$⊢ B = {Base}_{Z}$
	dchrn0.u	$⊢ U = Unit (Z)$
	dchr1cl.o	$⊢ \underset{˙}{1} = (k \in B ⟼ if (k \in U, 1, 0))$
	dchrmulid2.t	$⊢ \underset{˙}{\cdot} = +_{G}$
	dchrmulid2.x	$⊢ φ \to X \in D$
	dchrinvcl.n	$⊢ K = (k \in B ⟼ if (k \in U, \frac{1}{X (k)}, 0))$
Assertion	dchrinvcl	$⊢ φ \to (K \in D \land K \underset{˙}{\cdot} X = \underset{˙}{1})$

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	$⊢ G = DChr (N)$
2		dchrmhm.z	$⊢ Z = ℤ / N ℤ$
3		dchrmhm.b	$⊢ D = {Base}_{G}$
4		dchrn0.b	$⊢ B = {Base}_{Z}$
5		dchrn0.u	$⊢ U = Unit (Z)$
6		dchr1cl.o	$⊢ \underset{˙}{1} = (k \in B ⟼ if (k \in U, 1, 0))$
7		dchrmulid2.t	$⊢ \underset{˙}{\cdot} = +_{G}$
8		dchrmulid2.x	$⊢ φ \to X \in D$
9		dchrinvcl.n	$⊢ K = (k \in B ⟼ if (k \in U, \frac{1}{X (k)}, 0))$
10	1 3	dchrrcl	$⊢ X \in D \to N \in ℕ$
11	8 10	syl	$⊢ φ \to N \in ℕ$
12		fveq2	$⊢ k = x \to X (k) = X (x)$
13	12	oveq2d	$⊢ k = x \to \frac{1}{X (k)} = \frac{1}{X (x)}$
14		fveq2	$⊢ k = y \to X (k) = X (y)$
15	14	oveq2d	$⊢ k = y \to \frac{1}{X (k)} = \frac{1}{X (y)}$
16		fveq2	$⊢ k = x \cdot_{Z} y \to X (k) = X (x \cdot_{Z} y)$
17	16	oveq2d	$⊢ k = x \cdot_{Z} y \to \frac{1}{X (k)} = \frac{1}{X (x \cdot_{Z} y)}$
18		fveq2	$⊢ k = 1_{Z} \to X (k) = X (1_{Z})$
19	18	oveq2d	$⊢ k = 1_{Z} \to \frac{1}{X (k)} = \frac{1}{X (1_{Z})}$
20	1 2 3 4 8	dchrf	$⊢ φ \to X : B ⟶ ℂ$
21	4 5	unitss	$⊢ U \subseteq B$
22	21	sseli	$⊢ k \in U \to k \in B$
23		ffvelrn	$⊢ (X : B ⟶ ℂ \land k \in B) \to X (k) \in ℂ$
24	20 22 23	syl2an	$⊢ (φ \land k \in U) \to X (k) \in ℂ$
25		simpr	$⊢ (φ \land k \in U) \to k \in U$
26	8	adantr	$⊢ (φ \land k \in U) \to X \in D$
27	22	adantl	$⊢ (φ \land k \in U) \to k \in B$
28	1 2 3 4 5 26 27	dchrn0	$⊢ (φ \land k \in U) \to (X (k) \neq 0 \leftrightarrow k \in U)$
29	25 28	mpbird	$⊢ (φ \land k \in U) \to X (k) \neq 0$
30	24 29	reccld	$⊢ (φ \land k \in U) \to \frac{1}{X (k)} \in ℂ$
31		1t1e1	$⊢ 1 \cdot 1 = 1$
32	31	eqcomi	$⊢ 1 = 1 \cdot 1$
33	32	a1i	$⊢ (φ \land (x \in U \land y \in U)) \to 1 = 1 \cdot 1$
34	1 2 3	dchrmhm	$⊢ D \subseteq {mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}$
35	8	adantr	$⊢ (φ \land (x \in U \land y \in U)) \to X \in D$
36	34 35	sseldi	$⊢ (φ \land (x \in U \land y \in U)) \to X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})$
37		simprl	$⊢ (φ \land (x \in U \land y \in U)) \to x \in U$
38	21 37	sseldi	$⊢ (φ \land (x \in U \land y \in U)) \to x \in B$
39		simprr	$⊢ (φ \land (x \in U \land y \in U)) \to y \in U$
40	21 39	sseldi	$⊢ (φ \land (x \in U \land y \in U)) \to y \in B$
41		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
42	41 4	mgpbas	$⊢ B = {Base}_{{mulGrp}_{Z}}$
43		eqid	$⊢ \cdot_{Z} = \cdot_{Z}$
44	41 43	mgpplusg	$⊢ \cdot_{Z} = +_{{mulGrp}_{Z}}$
45		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
46		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
47	45 46	mgpplusg	$⊢ \times = +_{{mulGrp}_{ℂ_{fld}}}$
48	42 44 47	mhmlin	$⊢ (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land x \in B \land y \in B) \to X (x \cdot_{Z} y) = X (x) X (y)$
49	36 38 40 48	syl3anc	$⊢ (φ \land (x \in U \land y \in U)) \to X (x \cdot_{Z} y) = X (x) X (y)$
50	33 49	oveq12d	$⊢ (φ \land (x \in U \land y \in U)) \to \frac{1}{X (x \cdot_{Z} y)} = \frac{1 \cdot 1}{X (x) X (y)}$
51		1cnd	$⊢ (φ \land (x \in U \land y \in U)) \to 1 \in ℂ$
52	20	adantr	$⊢ (φ \land (x \in U \land y \in U)) \to X : B ⟶ ℂ$
53	52 38	ffvelrnd	$⊢ (φ \land (x \in U \land y \in U)) \to X (x) \in ℂ$
54	52 40	ffvelrnd	$⊢ (φ \land (x \in U \land y \in U)) \to X (y) \in ℂ$
55	1 2 3 4 5 35 38	dchrn0	$⊢ (φ \land (x \in U \land y \in U)) \to (X (x) \neq 0 \leftrightarrow x \in U)$
56	37 55	mpbird	$⊢ (φ \land (x \in U \land y \in U)) \to X (x) \neq 0$
57	1 2 3 4 5 35 40	dchrn0	$⊢ (φ \land (x \in U \land y \in U)) \to (X (y) \neq 0 \leftrightarrow y \in U)$
58	39 57	mpbird	$⊢ (φ \land (x \in U \land y \in U)) \to X (y) \neq 0$
59	51 53 51 54 56 58	divmuldivd	$⊢ (φ \land (x \in U \land y \in U)) \to (\frac{1}{X (x)}) (\frac{1}{X (y)}) = \frac{1 \cdot 1}{X (x) X (y)}$
60	50 59	eqtr4d	$⊢ (φ \land (x \in U \land y \in U)) \to \frac{1}{X (x \cdot_{Z} y)} = (\frac{1}{X (x)}) (\frac{1}{X (y)})$
61	34 8	sseldi	$⊢ φ \to X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})$
62		eqid	$⊢ 1_{Z} = 1_{Z}$
63	41 62	ringidval	$⊢ 1_{Z} = 0_{{mulGrp}_{Z}}$
64		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
65	45 64	ringidval	$⊢ 1 = 0_{{mulGrp}_{ℂ_{fld}}}$
66	63 65	mhm0	$⊢ X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \to X (1_{Z}) = 1$
67	61 66	syl	$⊢ φ \to X (1_{Z}) = 1$
68	67	oveq2d	$⊢ φ \to \frac{1}{X (1_{Z})} = \frac{1}{1}$
69		1div1e1	$⊢ \frac{1}{1} = 1$
70	68 69	eqtrdi	$⊢ φ \to \frac{1}{X (1_{Z})} = 1$
71	1 2 4 5 11 3 13 15 17 19 30 60 70	dchrelbasd	$⊢ φ \to (k \in B ⟼ if (k \in U, \frac{1}{X (k)}, 0)) \in D$
72	9 71	eqeltrid	$⊢ φ \to K \in D$
73	1 2 3 7 72 8	dchrmul	$⊢ φ \to K \underset{˙}{\cdot} X = K \times_{f} X$
74	4	fvexi	$⊢ B \in V$
75	74	a1i	$⊢ φ \to B \in V$
76		ovex	$⊢ \frac{1}{X (k)} \in V$
77		c0ex	$⊢ 0 \in V$
78	76 77	ifex	$⊢ if (k \in U, \frac{1}{X (k)}, 0) \in V$
79	78	a1i	$⊢ (φ \land k \in B) \to if (k \in U, \frac{1}{X (k)}, 0) \in V$
80	20	ffvelrnda	$⊢ (φ \land k \in B) \to X (k) \in ℂ$
81	9	a1i	$⊢ φ \to K = (k \in B ⟼ if (k \in U, \frac{1}{X (k)}, 0))$
82	20	feqmptd	$⊢ φ \to X = (k \in B ⟼ X (k))$
83	75 79 80 81 82	offval2	$⊢ φ \to K \times_{f} X = (k \in B ⟼ if (k \in U, \frac{1}{X (k)}, 0) X (k))$
84		ovif	$⊢ if (k \in U, \frac{1}{X (k)}, 0) X (k) = if (k \in U, (\frac{1}{X (k)}) X (k), 0 \cdot X (k))$
85	80	adantr	$⊢ ((φ \land k \in B) \land k \in U) \to X (k) \in ℂ$
86	8	adantr	$⊢ (φ \land k \in B) \to X \in D$
87		simpr	$⊢ (φ \land k \in B) \to k \in B$
88	1 2 3 4 5 86 87	dchrn0	$⊢ (φ \land k \in B) \to (X (k) \neq 0 \leftrightarrow k \in U)$
89	88	biimpar	$⊢ ((φ \land k \in B) \land k \in U) \to X (k) \neq 0$
90	85 89	recid2d	$⊢ ((φ \land k \in B) \land k \in U) \to (\frac{1}{X (k)}) X (k) = 1$
91	90	ifeq1da	$⊢ (φ \land k \in B) \to if (k \in U, (\frac{1}{X (k)}) X (k), 0 \cdot X (k)) = if (k \in U, 1, 0 \cdot X (k))$
92	80	mul02d	$⊢ (φ \land k \in B) \to 0 \cdot X (k) = 0$
93	92	ifeq2d	$⊢ (φ \land k \in B) \to if (k \in U, 1, 0 \cdot X (k)) = if (k \in U, 1, 0)$
94	91 93	eqtrd	$⊢ (φ \land k \in B) \to if (k \in U, (\frac{1}{X (k)}) X (k), 0 \cdot X (k)) = if (k \in U, 1, 0)$
95	84 94	syl5eq	$⊢ (φ \land k \in B) \to if (k \in U, \frac{1}{X (k)}, 0) X (k) = if (k \in U, 1, 0)$
96	95	mpteq2dva	$⊢ φ \to (k \in B ⟼ if (k \in U, \frac{1}{X (k)}, 0) X (k)) = (k \in B ⟼ if (k \in U, 1, 0))$
97	6 96	eqtr4id	$⊢ φ \to \underset{˙}{1} = (k \in B ⟼ if (k \in U, \frac{1}{X (k)}, 0) X (k))$
98	83 97	eqtr4d	$⊢ φ \to K \times_{f} X = \underset{˙}{1}$
99	73 98	eqtrd	$⊢ φ \to K \underset{˙}{\cdot} X = \underset{˙}{1}$
100	72 99	jca	$⊢ φ \to (K \in D \land K \underset{˙}{\cdot} X = \underset{˙}{1})$

Metamath Proof Explorer

Theorem dchrinvcl

Proof