Theorem dchrplusg

Description: Group operation on the group of Dirichlet characters. (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$$
	dchrmul.t	$$⊢\underset{\dot{}}{·}={+}_G$$
	dchrplusg.n	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	dchrplusg	$$⊢\phi \to \underset{\dot{}}{·}={{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}$$

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		dchrmul.t	$$⊢\underset{\dot{}}{·}={+}_G$$
5		dchrplusg.n	$$⊢\phi \to N\in \mathbb{N}$$
6		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
7		eqid	$$⊢\mathrm{Unit}\left(Z\right)=\mathrm{Unit}\left(Z\right)$$
8	1 2 6 7 5 3	dchrbas	$$⊢\phi \to D=\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left({\mathrm{Base}}_Z\setminus \mathrm{Unit}\left(Z\right)\right)\times \left\{0\right\}\subseteq x\right\}$$
9	1 2 6 7 5 8	dchrval	$$⊢\phi \to G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},D⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}⟩\right\}$$
10	9	fveq2d	$$⊢\phi \to {+}_G={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},D⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}⟩\right\}}$$
11	3	fvexi	$$⊢D\in \mathrm{V}$$
12	11 11	xpex	$$⊢D\times D\in \mathrm{V}$$
13		ofexg	$$⊢D\times D\in \mathrm{V}\to {{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}\in \mathrm{V}$$
14		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},D⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},D⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}⟩\right\}$$
15	14	grpplusg	$$⊢{{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}\in \mathrm{V}\to {{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},D⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}⟩\right\}}$$
16	12 13 15	mp2b	$$⊢{{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},D⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}⟩\right\}}$$
17	10 4 16	3eqtr4g	$$⊢\phi \to \underset{\dot{}}{·}={{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}$$