Theorem dchrmullid

Description: Left identity for the principal Dirichlet character. (Contributed by Mario Carneiro, 18-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$$
Assertion	dchrmullid	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$

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	1 3	dchrrcl	$$⊢X\in D\to N\in \mathbb{N}$$
10	8 9	syl	$$⊢\phi \to N\in \mathbb{N}$$
11	1 2 3 4 5 6 10	dchr1cl	$$⊢\phi \to \underset{\dot{}}{1}\in D$$
12	1 2 3 7 11 8	dchrmul	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}X=\underset{\dot{}}{1}{\times }_{f}X$$
13		oveq1	$$⊢1=if\left(k\in U,1,0\right)\to 1X\left(k\right)=if\left(k\in U,1,0\right)X\left(k\right)$$
14	13	eqeq1d	$$⊢1=if\left(k\in U,1,0\right)\to \left(1X\left(k\right)=X\left(k\right)\leftrightarrow if\left(k\in U,1,0\right)X\left(k\right)=X\left(k\right)\right)$$
15		oveq1	$$⊢0=if\left(k\in U,1,0\right)\to 0\cdot X\left(k\right)=if\left(k\in U,1,0\right)X\left(k\right)$$
16	15	eqeq1d	$$⊢0=if\left(k\in U,1,0\right)\to \left(0\cdot X\left(k\right)=X\left(k\right)\leftrightarrow if\left(k\in U,1,0\right)X\left(k\right)=X\left(k\right)\right)$$
17	1 2 3 4 8	dchrf	$$⊢\phi \to X:B⟶ℂ$$
18	17	ffvelcdmda	$$⊢\left(\phi \wedge k\in B\right)\to X\left(k\right)\in ℂ$$
19	18	adantr	$$⊢\left(\left(\phi \wedge k\in B\right)\wedge k\in U\right)\to X\left(k\right)\in ℂ$$
20	19	mullidd	$$⊢\left(\left(\phi \wedge k\in B\right)\wedge k\in U\right)\to 1X\left(k\right)=X\left(k\right)$$
21		0cn	$$⊢0\in ℂ$$
22	21	mul02i	$$⊢0\cdot 0=0$$
23	1 2 4 5 10 3	dchrelbas2	$$⊢\phi \to \left(X\in D\leftrightarrow \left(X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \forall k\in B\left(X\left(k\right)\ne 0\to k\in U\right)\right)\right)$$
24	8 23	mpbid	$$⊢\phi \to \left(X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \forall k\in B\left(X\left(k\right)\ne 0\to k\in U\right)\right)$$
25	24	simprd	$$⊢\phi \to \forall k\in B\left(X\left(k\right)\ne 0\to k\in U\right)$$
26	25	r19.21bi	$$⊢\left(\phi \wedge k\in B\right)\to \left(X\left(k\right)\ne 0\to k\in U\right)$$
27	26	necon1bd	$$⊢\left(\phi \wedge k\in B\right)\to \left(\neg k\in U\to X\left(k\right)=0\right)$$
28	27	imp	$$⊢\left(\left(\phi \wedge k\in B\right)\wedge \neg k\in U\right)\to X\left(k\right)=0$$
29	28	oveq2d	$$⊢\left(\left(\phi \wedge k\in B\right)\wedge \neg k\in U\right)\to 0\cdot X\left(k\right)=0\cdot 0$$
30	22 29 28	3eqtr4a	$$⊢\left(\left(\phi \wedge k\in B\right)\wedge \neg k\in U\right)\to 0\cdot X\left(k\right)=X\left(k\right)$$
31	14 16 20 30	ifbothda	$$⊢\left(\phi \wedge k\in B\right)\to if\left(k\in U,1,0\right)X\left(k\right)=X\left(k\right)$$
32	31	mpteq2dva	$$⊢\phi \to \left(k\in B⟼if\left(k\in U,1,0\right)X\left(k\right)\right)=\left(k\in B⟼X\left(k\right)\right)$$
33	4	fvexi	$$⊢B\in \mathrm{V}$$
34	33	a1i	$$⊢\phi \to B\in \mathrm{V}$$
35		ax-1cn	$$⊢1\in ℂ$$
36	35 21	ifcli	$$⊢if\left(k\in U,1,0\right)\in ℂ$$
37	36	a1i	$$⊢\left(\phi \wedge k\in B\right)\to if\left(k\in U,1,0\right)\in ℂ$$
38	6	a1i	$$⊢\phi \to \underset{\dot{}}{1}=\left(k\in B⟼if\left(k\in U,1,0\right)\right)$$
39	17	feqmptd	$$⊢\phi \to X=\left(k\in B⟼X\left(k\right)\right)$$
40	34 37 18 38 39	offval2	$$⊢\phi \to \underset{\dot{}}{1}{\times }_{f}X=\left(k\in B⟼if\left(k\in U,1,0\right)X\left(k\right)\right)$$
41	32 40 39	3eqtr4d	$$⊢\phi \to \underset{\dot{}}{1}{\times }_{f}X=X$$
42	12 41	eqtrd	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$