Theorem dchrinvcl

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

	Ref	Expression
Hypotheses	dchrmhm.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchrmhm.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchrmhm.b	$$⊢D={\mathrm{Base}}_G$$
	dchrn0.b	$$⊢B={\mathrm{Base}}_Z$$
	dchrn0.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
	dchr1cl.o	$$⊢\underset{\dot{}}{1}=\left(k\in B⟼if\left(k\in U,1,0\right)\right)$$
	dchrmullid.t	$$⊢\underset{\dot{}}{·}={+}_G$$
	dchrmullid.x	$$⊢\phi \to X\in D$$
	dchrinvcl.n	$$⊢K=\left(k\in B⟼if\left(k\in U,\frac{1}{X\left(k\right)},0\right)\right)$$
Assertion	dchrinvcl	$$⊢\phi \to \left(K\in D\wedge K\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)$$

Proof

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