Theorem dchrinvcl

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

	Ref	Expression
Hypotheses	dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
	dchrn0.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
	dchrn0.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
	dchr1cl.o	⊢ 1 = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) )
	dchrmullid.t	⊢ · = ( +g ‘ 𝐺 )
	dchrmullid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrinvcl.n	⊢ 𝐾 = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , ( 1 / ( 𝑋 ‘ 𝑘 ) ) , 0 ) )
Assertion	dchrinvcl	⊢ ( 𝜑 → ( 𝐾 ∈ 𝐷 ∧ ( 𝐾 · 𝑋 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
4		dchrn0.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
5		dchrn0.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
6		dchr1cl.o	⊢ 1 = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) )
7		dchrmullid.t	⊢ · = ( +g ‘ 𝐺 )
8		dchrmullid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9		dchrinvcl.n	⊢ 𝐾 = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , ( 1 / ( 𝑋 ‘ 𝑘 ) ) , 0 ) )
10	1 3	dchrrcl	⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
11	8 10	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
12		fveq2	⊢ ( 𝑘 = 𝑥 → ( 𝑋 ‘ 𝑘 ) = ( 𝑋 ‘ 𝑥 ) )
13	12	oveq2d	⊢ ( 𝑘 = 𝑥 → ( 1 / ( 𝑋 ‘ 𝑘 ) ) = ( 1 / ( 𝑋 ‘ 𝑥 ) ) )
14		fveq2	⊢ ( 𝑘 = 𝑦 → ( 𝑋 ‘ 𝑘 ) = ( 𝑋 ‘ 𝑦 ) )
15	14	oveq2d	⊢ ( 𝑘 = 𝑦 → ( 1 / ( 𝑋 ‘ 𝑘 ) ) = ( 1 / ( 𝑋 ‘ 𝑦 ) ) )
16		fveq2	⊢ ( 𝑘 = ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) → ( 𝑋 ‘ 𝑘 ) = ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) )
17	16	oveq2d	⊢ ( 𝑘 = ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) → ( 1 / ( 𝑋 ‘ 𝑘 ) ) = ( 1 / ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) ) )
18		fveq2	⊢ ( 𝑘 = ( 1r ‘ 𝑍 ) → ( 𝑋 ‘ 𝑘 ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
19	18	oveq2d	⊢ ( 𝑘 = ( 1r ‘ 𝑍 ) → ( 1 / ( 𝑋 ‘ 𝑘 ) ) = ( 1 / ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) ) )
20	1 2 3 4 8	dchrf	⊢ ( 𝜑 → 𝑋 : 𝐵 ⟶ ℂ )
21	4 5	unitss	⊢ 𝑈 ⊆ 𝐵
22	21	sseli	⊢ ( 𝑘 ∈ 𝑈 → 𝑘 ∈ 𝐵 )
23		ffvelcdm	⊢ ( ( 𝑋 : 𝐵 ⟶ ℂ ∧ 𝑘 ∈ 𝐵 ) → ( 𝑋 ‘ 𝑘 ) ∈ ℂ )
24	20 22 23	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑘 ) ∈ ℂ )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ∈ 𝑈 )
26	8	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝑋 ∈ 𝐷 )
27	22	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ∈ 𝐵 )
28	1 2 3 4 5 26 27	dchrn0	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( ( 𝑋 ‘ 𝑘 ) ≠ 0 ↔ 𝑘 ∈ 𝑈 ) )
29	25 28	mpbird	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑘 ) ≠ 0 )
30	24 29	reccld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( 1 / ( 𝑋 ‘ 𝑘 ) ) ∈ ℂ )
31		1t1e1	⊢ ( 1 · 1 ) = 1
32	31	eqcomi	⊢ 1 = ( 1 · 1 )
33	32	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 1 = ( 1 · 1 ) )
34	1 2 3	dchrmhm	⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
35	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑋 ∈ 𝐷 )
36	34 35	sselid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
37		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝑈 )
38	21 37	sselid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝐵 )
39		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
40	21 39	sselid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝐵 )
41		eqid	⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
42	41 4	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑍 ) )
43		eqid	⊢ ( .r ‘ 𝑍 ) = ( .r ‘ 𝑍 )
44	41 43	mgpplusg	⊢ ( .r ‘ 𝑍 ) = ( +g ‘ ( mulGrp ‘ 𝑍 ) )
45		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
46		cnfldmul	⊢ · = ( .r ‘ ℂfld )
47	45 46	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
48	42 44 47	mhmlin	⊢ ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
49	36 38 40 48	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
50	33 49	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 1 / ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) ) = ( ( 1 · 1 ) / ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
51		1cnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 1 ∈ ℂ )
52	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑋 : 𝐵 ⟶ ℂ )
53	52 38	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
54	52 40	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑋 ‘ 𝑦 ) ∈ ℂ )
55	1 2 3 4 5 35 38	dchrn0	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 ↔ 𝑥 ∈ 𝑈 ) )
56	37 55	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑋 ‘ 𝑥 ) ≠ 0 )
57	1 2 3 4 5 35 40	dchrn0	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑋 ‘ 𝑦 ) ≠ 0 ↔ 𝑦 ∈ 𝑈 ) )
58	39 57	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑋 ‘ 𝑦 ) ≠ 0 )
59	51 53 51 54 56 58	divmuldivd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 1 / ( 𝑋 ‘ 𝑥 ) ) · ( 1 / ( 𝑋 ‘ 𝑦 ) ) ) = ( ( 1 · 1 ) / ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
60	50 59	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 1 / ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) ) = ( ( 1 / ( 𝑋 ‘ 𝑥 ) ) · ( 1 / ( 𝑋 ‘ 𝑦 ) ) ) )
61	34 8	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
62		eqid	⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
63	41 62	ringidval	⊢ ( 1r ‘ 𝑍 ) = ( 0g ‘ ( mulGrp ‘ 𝑍 ) )
64		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
65	45 64	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
66	63 65	mhm0	⊢ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
67	61 66	syl	⊢ ( 𝜑 → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
68	67	oveq2d	⊢ ( 𝜑 → ( 1 / ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) ) = ( 1 / 1 ) )
69		1div1e1	⊢ ( 1 / 1 ) = 1
70	68 69	eqtrdi	⊢ ( 𝜑 → ( 1 / ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) ) = 1 )
71	1 2 4 5 11 3 13 15 17 19 30 60 70	dchrelbasd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , ( 1 / ( 𝑋 ‘ 𝑘 ) ) , 0 ) ) ∈ 𝐷 )
72	9 71	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
73	1 2 3 7 72 8	dchrmul	⊢ ( 𝜑 → ( 𝐾 · 𝑋 ) = ( 𝐾 ∘f · 𝑋 ) )
74	4	fvexi	⊢ 𝐵 ∈ V
75	74	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
76		ovex	⊢ ( 1 / ( 𝑋 ‘ 𝑘 ) ) ∈ V
77		c0ex	⊢ 0 ∈ V
78	76 77	ifex	⊢ if ( 𝑘 ∈ 𝑈 , ( 1 / ( 𝑋 ‘ 𝑘 ) ) , 0 ) ∈ V
79	78	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝑈 , ( 1 / ( 𝑋 ‘ 𝑘 ) ) , 0 ) ∈ V )
80	20	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑋 ‘ 𝑘 ) ∈ ℂ )
81	9	a1i	⊢ ( 𝜑 → 𝐾 = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , ( 1 / ( 𝑋 ‘ 𝑘 ) ) , 0 ) ) )
82	20	feqmptd	⊢ ( 𝜑 → 𝑋 = ( 𝑘 ∈ 𝐵 ↦ ( 𝑋 ‘ 𝑘 ) ) )
83	75 79 80 81 82	offval2	⊢ ( 𝜑 → ( 𝐾 ∘f · 𝑋 ) = ( 𝑘 ∈ 𝐵 ↦ ( if ( 𝑘 ∈ 𝑈 , ( 1 / ( 𝑋 ‘ 𝑘 ) ) , 0 ) · ( 𝑋 ‘ 𝑘 ) ) ) )
84		ovif	⊢ ( if ( 𝑘 ∈ 𝑈 , ( 1 / ( 𝑋 ‘ 𝑘 ) ) , 0 ) · ( 𝑋 ‘ 𝑘 ) ) = if ( 𝑘 ∈ 𝑈 , ( ( 1 / ( 𝑋 ‘ 𝑘 ) ) · ( 𝑋 ‘ 𝑘 ) ) , ( 0 · ( 𝑋 ‘ 𝑘 ) ) )
85	80	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑘 ) ∈ ℂ )
86	8	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝑋 ∈ 𝐷 )
87		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
88	1 2 3 4 5 86 87	dchrn0	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑘 ) ≠ 0 ↔ 𝑘 ∈ 𝑈 ) )
89	88	biimpar	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑘 ) ≠ 0 )
90	85 89	recid2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑘 ∈ 𝑈 ) → ( ( 1 / ( 𝑋 ‘ 𝑘 ) ) · ( 𝑋 ‘ 𝑘 ) ) = 1 )
91	90	ifeq1da	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝑈 , ( ( 1 / ( 𝑋 ‘ 𝑘 ) ) · ( 𝑋 ‘ 𝑘 ) ) , ( 0 · ( 𝑋 ‘ 𝑘 ) ) ) = if ( 𝑘 ∈ 𝑈 , 1 , ( 0 · ( 𝑋 ‘ 𝑘 ) ) ) )
92	80	mul02d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 0 · ( 𝑋 ‘ 𝑘 ) ) = 0 )
93	92	ifeq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝑈 , 1 , ( 0 · ( 𝑋 ‘ 𝑘 ) ) ) = if ( 𝑘 ∈ 𝑈 , 1 , 0 ) )
94	91 93	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝑈 , ( ( 1 / ( 𝑋 ‘ 𝑘 ) ) · ( 𝑋 ‘ 𝑘 ) ) , ( 0 · ( 𝑋 ‘ 𝑘 ) ) ) = if ( 𝑘 ∈ 𝑈 , 1 , 0 ) )
95	84 94	eqtrid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( if ( 𝑘 ∈ 𝑈 , ( 1 / ( 𝑋 ‘ 𝑘 ) ) , 0 ) · ( 𝑋 ‘ 𝑘 ) ) = if ( 𝑘 ∈ 𝑈 , 1 , 0 ) )
96	95	mpteq2dva	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ ( if ( 𝑘 ∈ 𝑈 , ( 1 / ( 𝑋 ‘ 𝑘 ) ) , 0 ) · ( 𝑋 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) )
97	6 96	eqtr4id	⊢ ( 𝜑 → 1 = ( 𝑘 ∈ 𝐵 ↦ ( if ( 𝑘 ∈ 𝑈 , ( 1 / ( 𝑋 ‘ 𝑘 ) ) , 0 ) · ( 𝑋 ‘ 𝑘 ) ) ) )
98	83 97	eqtr4d	⊢ ( 𝜑 → ( 𝐾 ∘f · 𝑋 ) = 1 )
99	73 98	eqtrd	⊢ ( 𝜑 → ( 𝐾 · 𝑋 ) = 1 )
100	72 99	jca	⊢ ( 𝜑 → ( 𝐾 ∈ 𝐷 ∧ ( 𝐾 · 𝑋 ) = 1 ) )