Theorem dchrmul

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$$
	dchrmul.x	$$⊢\phi \to X\in D$$
	dchrmul.y	$$⊢\phi \to Y\in D$$
Assertion	dchrmul	$$⊢\phi \to X\underset{\dot{}}{·}Y=X{\times }_{f}Y$$

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		dchrmul.x	$$⊢\phi \to X\in D$$
6		dchrmul.y	$$⊢\phi \to Y\in D$$
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 3 4 8	dchrplusg	$$⊢\phi \to \underset{\dot{}}{·}={{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}$$
10	9	oveqd	$$⊢\phi \to X\underset{\dot{}}{·}Y=X\left({{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}\right)Y$$
11	5 6	ofmresval	$$⊢\phi \to X\left({{\circ }_f\times \upharpoonright }_{\left(D\times D\right)}\right)Y=X{\times }_{f}Y$$
12	10 11	eqtrd	$$⊢\phi \to X\underset{\dot{}}{·}Y=X{\times }_{f}Y$$