dchrplusg

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}$
	dchrplusg.n	$⊢ φ \to N \in ℕ$
Assertion	dchrplusg	$⊢ φ \to \underset{˙}{\cdot} = {\circ_{f} \times ↾}_{(D \times D)}$

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		dchrplusg.n	$⊢ φ \to N \in ℕ$
6		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
7		eqid	$⊢ Unit (Z) = Unit (Z)$
8	1 2 6 7 5 3	dchrbas	$⊢ φ \to D = \{x \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{Z} ∖ Unit (Z)) \times \{0\} \subseteq x\}$
9	1 2 6 7 5 8	dchrval	$⊢ φ \to G = \{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\}$
10	9	fveq2d	$⊢ φ \to +_{G} = +_{\{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\}}$
11	3	fvexi	$⊢ D \in V$
12	11 11	xpex	$⊢ D \times D \in V$
13		ofexg	$⊢ D \times D \in V \to {\circ_{f} \times ↾}_{(D \times D)} \in V$
14		eqid	$⊢ \{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\} = \{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\}$
15	14	grpplusg	$⊢ {\circ_{f} \times ↾}_{(D \times D)} \in V \to {\circ_{f} \times ↾}_{(D \times D)} = +_{\{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\}}$
16	12 13 15	mp2b	$⊢ {\circ_{f} \times ↾}_{(D \times D)} = +_{\{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\}}$
17	10 4 16	3eqtr4g	$⊢ φ \to \underset{˙}{\cdot} = {\circ_{f} \times ↾}_{(D \times D)}$

Metamath Proof Explorer