Theorem dchr1

Description: Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dchr1.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchr1.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchr1.o	$$⊢\underset{\dot{}}{1}=0_G$$
	dchr1.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
	dchr1.n	$$⊢\phi \to N\in \mathbb{N}$$
	dchr1.a	$$⊢\phi \to A\in U$$
Assertion	dchr1	$$⊢\phi \to \underset{\dot{}}{1}\left(A\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		dchr1.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchr1.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
3		dchr1.o	$$⊢\underset{\dot{}}{1}=0_G$$
4		dchr1.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
5		dchr1.n	$$⊢\phi \to N\in \mathbb{N}$$
6		dchr1.a	$$⊢\phi \to A\in U$$
7		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
8		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
9		eqid	$$⊢\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)=\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)$$
10	1 2 7 8 4 9 5	dchr1cl	$$⊢\phi \to \left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)\in {\mathrm{Base}}_G$$
11		eleq1w	$$⊢k=x\to \left(k\in U\leftrightarrow x\in U\right)$$
12	11	ifbid	$$⊢k=x\to if\left(k\in U,1,0\right)=if\left(x\in U,1,0\right)$$
13	12	cbvmptv	$$⊢\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)=\left(x\in {\mathrm{Base}}_Z⟼if\left(x\in U,1,0\right)\right)$$
14		eqid	$$⊢{+}_G={+}_G$$
15	1 2 7 8 4 13 14 10	dchrmulid2	$$⊢\phi \to \left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right){+}_G\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)=\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)$$
16	1	dchrabl	$$⊢N\in \mathbb{N}\to G\in \mathrm{Abel}$$
17		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
18	7 14 3	isgrpid2	$$⊢G\in \mathrm{Grp}\to \left(\left(\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)\in {\mathrm{Base}}_G\wedge \left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right){+}_G\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)=\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)\right)\leftrightarrow \underset{\dot{}}{1}=\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)\right)$$
19	5 16 17 18	4syl	$$⊢\phi \to \left(\left(\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)\in {\mathrm{Base}}_G\wedge \left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right){+}_G\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)=\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)\right)\leftrightarrow \underset{\dot{}}{1}=\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)\right)$$
20	10 15 19	mpbi2and	$$⊢\phi \to \underset{\dot{}}{1}=\left(k\in {\mathrm{Base}}_Z⟼if\left(k\in U,1,0\right)\right)$$
21		simpr	$$⊢\left(\phi \wedge k=A\right)\to k=A$$
22	6	adantr	$$⊢\left(\phi \wedge k=A\right)\to A\in U$$
23	21 22	eqeltrd	$$⊢\left(\phi \wedge k=A\right)\to k\in U$$
24	23	iftrued	$$⊢\left(\phi \wedge k=A\right)\to if\left(k\in U,1,0\right)=1$$
25	8 4	unitss	$$⊢U\subseteq {\mathrm{Base}}_Z$$
26	25 6	sselid	$$⊢\phi \to A\in {\mathrm{Base}}_Z$$
27		1cnd	$$⊢\phi \to 1\in ℂ$$
28	20 24 26 27	fvmptd	$$⊢\phi \to \underset{\dot{}}{1}\left(A\right)=1$$