Theorem dchrf

Description: A Dirichlet character is a function. (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$$
	dchrf.b	$$⊢B={\mathrm{Base}}_Z$$
	dchrf.x	$$⊢\phi \to X\in D$$
Assertion	dchrf	$$⊢\phi \to X:B⟶ℂ$$

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		dchrf.b	$$⊢B={\mathrm{Base}}_Z$$
5		dchrf.x	$$⊢\phi \to X\in D$$
6		eqid	$$⊢\mathrm{Unit}\left(Z\right)=\mathrm{Unit}\left(Z\right)$$
7	1 3	dchrrcl	$$⊢X\in D\to N\in \mathbb{N}$$
8	5 7	syl	$$⊢\phi \to N\in \mathbb{N}$$
9	1 2 4 6 8 3	dchrelbas3	$$⊢\phi \to \left(X\in D\leftrightarrow \left(X:B⟶ℂ\wedge \left(\forall x\in \mathrm{Unit}\left(Z\right)\forall y\in \mathrm{Unit}\left(Z\right)X\left(x{\cdot }_{Z}y\right)=X\left(x\right)X\left(y\right)\wedge X\left(1_Z\right)=1\wedge \forall x\in B\left(X\left(x\right)\ne 0\to x\in \mathrm{Unit}\left(Z\right)\right)\right)\right)\right)$$
10	5 9	mpbid	$$⊢\phi \to \left(X:B⟶ℂ\wedge \left(\forall x\in \mathrm{Unit}\left(Z\right)\forall y\in \mathrm{Unit}\left(Z\right)X\left(x{\cdot }_{Z}y\right)=X\left(x\right)X\left(y\right)\wedge X\left(1_Z\right)=1\wedge \forall x\in B\left(X\left(x\right)\ne 0\to x\in \mathrm{Unit}\left(Z\right)\right)\right)\right)$$
11	10	simpld	$$⊢\phi \to X:B⟶ℂ$$