Theorem dchrresb

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	dchrresb	$$⊢\phi \to \left({X\upharpoonright }_U={Y\upharpoonright }_U\leftrightarrow X=Y\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		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
8	1 2 3 7 5	dchrf	$$⊢\phi \to X:{\mathrm{Base}}_Z⟶ℂ$$
9	8	ffnd	$$⊢\phi \to XFn{\mathrm{Base}}_Z$$
10	1 2 3 7 6	dchrf	$$⊢\phi \to Y:{\mathrm{Base}}_Z⟶ℂ$$
11	10	ffnd	$$⊢\phi \to YFn{\mathrm{Base}}_Z$$
12	7 4	unitss	$$⊢U\subseteq {\mathrm{Base}}_Z$$
13		fvreseq	$$⊢\left(\left(XFn{\mathrm{Base}}_Z\wedge YFn{\mathrm{Base}}_Z\right)\wedge U\subseteq {\mathrm{Base}}_Z\right)\to \left({X\upharpoonright }_U={Y\upharpoonright }_U\leftrightarrow \forall k\in UX\left(k\right)=Y\left(k\right)\right)$$
14	12 13	mpan2	$$⊢\left(XFn{\mathrm{Base}}_Z\wedge YFn{\mathrm{Base}}_Z\right)\to \left({X\upharpoonright }_U={Y\upharpoonright }_U\leftrightarrow \forall k\in UX\left(k\right)=Y\left(k\right)\right)$$
15	9 11 14	syl2anc	$$⊢\phi \to \left({X\upharpoonright }_U={Y\upharpoonright }_U\leftrightarrow \forall k\in UX\left(k\right)=Y\left(k\right)\right)$$
16	1 2 3 4 5 6	dchreq	$$⊢\phi \to \left(X=Y\leftrightarrow \forall k\in UX\left(k\right)=Y\left(k\right)\right)$$
17	15 16	bitr4d	$$⊢\phi \to \left({X\upharpoonright }_U={Y\upharpoonright }_U\leftrightarrow X=Y\right)$$