dchrmul

Description: Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	dchrmhm.g	$⊢ G = DChr (N)$
	dchrmhm.z	$⊢ Z = ℤ / N ℤ$
	dchrmhm.b	$⊢ D = {Base}_{G}$
	dchrmul.t	$⊢ \underset{˙}{\cdot} = +_{G}$
	dchrmul.x	$⊢ φ \to X \in D$
	dchrmul.y	$⊢ φ \to Y \in D$
Assertion	dchrmul	$⊢ φ \to X \underset{˙}{\cdot} Y = X \times_{f} Y$

Step	Hyp	Ref	Expression
1		dchrmhm.g	$⊢ G = DChr (N)$
2		dchrmhm.z	$⊢ Z = ℤ / N ℤ$
3		dchrmhm.b	$⊢ D = {Base}_{G}$
4		dchrmul.t	$⊢ \underset{˙}{\cdot} = +_{G}$
5		dchrmul.x	$⊢ φ \to X \in D$
6		dchrmul.y	$⊢ φ \to Y \in D$
7	1 3	dchrrcl	$⊢ X \in D \to N \in ℕ$
8	5 7	syl	$⊢ φ \to N \in ℕ$
9	1 2 3 4 8	dchrplusg	$⊢ φ \to \underset{˙}{\cdot} = {\circ_{f} \times ↾}_{(D \times D)}$
10	9	oveqd	$⊢ φ \to X \underset{˙}{\cdot} Y = X ({\circ_{f} \times ↾}_{(D \times D)}) Y$
11	5 6	ofmresval	$⊢ φ \to X ({\circ_{f} \times ↾}_{(D \times D)}) Y = X \times_{f} Y$
12	10 11	eqtrd	$⊢ φ \to X \underset{˙}{\cdot} Y = X \times_{f} Y$

Metamath Proof Explorer