Theorem dchrbas

Description: Base set of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	dchrval.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchrval.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchrval.b	$$⊢B={\mathrm{Base}}_Z$$
	dchrval.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
	dchrval.n	$$⊢\phi \to N\in \mathbb{N}$$
	dchrbas.b	$$⊢D={\mathrm{Base}}_G$$
Assertion	dchrbas	$$⊢\phi \to D=\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dchrval.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchrval.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
3		dchrval.b	$$⊢B={\mathrm{Base}}_Z$$
4		dchrval.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
5		dchrval.n	$$⊢\phi \to N\in \mathbb{N}$$
6		dchrbas.b	$$⊢D={\mathrm{Base}}_G$$
7		eqidd	$$⊢\phi \to \left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}=\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}$$
8	1 2 3 4 5 7	dchrval	$$⊢\phi \to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\times \left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\right)}⟩\right\}$$
9	8	fveq2d	$$⊢\phi \to {\mathrm{Base}}_G={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\times \left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\right)}⟩\right\}}$$
10		ovex	$$⊢{\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{V}$$
11	10	rabex	$$⊢\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\in \mathrm{V}$$
12		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\times \left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\right)}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\times \left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\right)}⟩\right\}$$
13	12	grpbase	$$⊢\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\in \mathrm{V}\to \left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\times \left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\right)}⟩\right\}}$$
14	11 13	ax-mp	$$⊢\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\times \left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\right)}⟩\right\}}$$
15	9 6 14	3eqtr4g	$$⊢\phi \to D=\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}$$