Theorem dchreq

Description: A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dchrresb.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchrresb.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchrresb.b	$$⊢D={\mathrm{Base}}_G$$
	dchrresb.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
	dchrresb.x	$$⊢\phi \to X\in D$$
	dchrresb.Y	$$⊢\phi \to Y\in D$$
Assertion	dchreq	$$⊢\phi \to \left(X=Y\leftrightarrow \forall k\in UX\left(k\right)=Y\left(k\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dchrresb.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchrresb.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
3		dchrresb.b	$$⊢D={\mathrm{Base}}_G$$
4		dchrresb.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
5		dchrresb.x	$$⊢\phi \to X\in D$$
6		dchrresb.Y	$$⊢\phi \to Y\in D$$
7		eldif	$$⊢k\in \left({\mathrm{Base}}_Z\setminus U\right)\leftrightarrow \left(k\in {\mathrm{Base}}_Z\wedge \neg k\in U\right)$$
8		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
9	5	adantr	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_Z\right)\to X\in D$$
10		simpr	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_Z\right)\to k\in {\mathrm{Base}}_Z$$
11	1 2 3 8 4 9 10	dchrn0	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_Z\right)\to \left(X\left(k\right)\ne 0\leftrightarrow k\in U\right)$$
12	11	biimpd	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_Z\right)\to \left(X\left(k\right)\ne 0\to k\in U\right)$$
13	12	necon1bd	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_Z\right)\to \left(\neg k\in U\to X\left(k\right)=0\right)$$
14	13	impr	$$⊢\left(\phi \wedge \left(k\in {\mathrm{Base}}_Z\wedge \neg k\in U\right)\right)\to X\left(k\right)=0$$
15	7 14	sylan2b	$$⊢\left(\phi \wedge k\in \left({\mathrm{Base}}_Z\setminus U\right)\right)\to X\left(k\right)=0$$
16	6	adantr	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_Z\right)\to Y\in D$$
17	1 2 3 8 4 16 10	dchrn0	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_Z\right)\to \left(Y\left(k\right)\ne 0\leftrightarrow k\in U\right)$$
18	17	biimpd	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_Z\right)\to \left(Y\left(k\right)\ne 0\to k\in U\right)$$
19	18	necon1bd	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_Z\right)\to \left(\neg k\in U\to Y\left(k\right)=0\right)$$
20	19	impr	$$⊢\left(\phi \wedge \left(k\in {\mathrm{Base}}_Z\wedge \neg k\in U\right)\right)\to Y\left(k\right)=0$$
21	7 20	sylan2b	$$⊢\left(\phi \wedge k\in \left({\mathrm{Base}}_Z\setminus U\right)\right)\to Y\left(k\right)=0$$
22	15 21	eqtr4d	$$⊢\left(\phi \wedge k\in \left({\mathrm{Base}}_Z\setminus U\right)\right)\to X\left(k\right)=Y\left(k\right)$$
23	22	ralrimiva	$$⊢\phi \to \forall k\in \left({\mathrm{Base}}_Z\setminus U\right)X\left(k\right)=Y\left(k\right)$$
24	1 2 3 8 5	dchrf	$$⊢\phi \to X:{\mathrm{Base}}_Z⟶ℂ$$
25	24	ffnd	$$⊢\phi \to XFn{\mathrm{Base}}_Z$$
26	1 2 3 8 6	dchrf	$$⊢\phi \to Y:{\mathrm{Base}}_Z⟶ℂ$$
27	26	ffnd	$$⊢\phi \to YFn{\mathrm{Base}}_Z$$
28		eqfnfv	$$⊢\left(XFn{\mathrm{Base}}_Z\wedge YFn{\mathrm{Base}}_Z\right)\to \left(X=Y\leftrightarrow \forall k\in {\mathrm{Base}}_{Z}X\left(k\right)=Y\left(k\right)\right)$$
29	25 27 28	syl2anc	$$⊢\phi \to \left(X=Y\leftrightarrow \forall k\in {\mathrm{Base}}_{Z}X\left(k\right)=Y\left(k\right)\right)$$
30	8 4	unitss	$$⊢U\subseteq {\mathrm{Base}}_Z$$
31		undif	$$⊢U\subseteq {\mathrm{Base}}_Z\leftrightarrow U\cup \left({\mathrm{Base}}_Z\setminus U\right)={\mathrm{Base}}_Z$$
32	30 31	mpbi	$$⊢U\cup \left({\mathrm{Base}}_Z\setminus U\right)={\mathrm{Base}}_Z$$
33	32	raleqi	$$⊢\forall k\in \left(U\cup \left({\mathrm{Base}}_Z\setminus U\right)\right)X\left(k\right)=Y\left(k\right)\leftrightarrow \forall k\in {\mathrm{Base}}_{Z}X\left(k\right)=Y\left(k\right)$$
34		ralunb	$$⊢\forall k\in \left(U\cup \left({\mathrm{Base}}_Z\setminus U\right)\right)X\left(k\right)=Y\left(k\right)\leftrightarrow \left(\forall k\in UX\left(k\right)=Y\left(k\right)\wedge \forall k\in \left({\mathrm{Base}}_Z\setminus U\right)X\left(k\right)=Y\left(k\right)\right)$$
35	33 34	bitr3i	$$⊢\forall k\in {\mathrm{Base}}_{Z}X\left(k\right)=Y\left(k\right)\leftrightarrow \left(\forall k\in UX\left(k\right)=Y\left(k\right)\wedge \forall k\in \left({\mathrm{Base}}_Z\setminus U\right)X\left(k\right)=Y\left(k\right)\right)$$
36	29 35	bitrdi	$$⊢\phi \to \left(X=Y\leftrightarrow \left(\forall k\in UX\left(k\right)=Y\left(k\right)\wedge \forall k\in \left({\mathrm{Base}}_Z\setminus U\right)X\left(k\right)=Y\left(k\right)\right)\right)$$
37	23 36	mpbiran2d	$$⊢\phi \to \left(X=Y\leftrightarrow \forall k\in UX\left(k\right)=Y\left(k\right)\right)$$