dchrval

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

	Ref	Expression
Hypotheses	dchrval.g	$⊢ G = DChr (N)$
	dchrval.z	$⊢ Z = ℤ / N ℤ$
	dchrval.b	$⊢ B = {Base}_{Z}$
	dchrval.u	$⊢ U = Unit (Z)$
	dchrval.n	$⊢ φ \to N \in ℕ$
	dchrval.d	$⊢ φ \to D = \{x \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \| (B ∖ U) \times \{0\} \subseteq x\}$
Assertion	dchrval	$⊢ φ \to G = \{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\}$

Proof

Step	Hyp	Ref	Expression
1		dchrval.g	$⊢ G = DChr (N)$
2		dchrval.z	$⊢ Z = ℤ / N ℤ$
3		dchrval.b	$⊢ B = {Base}_{Z}$
4		dchrval.u	$⊢ U = Unit (Z)$
5		dchrval.n	$⊢ φ \to N \in ℕ$
6		dchrval.d	$⊢ φ \to D = \{x \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \| (B ∖ U) \times \{0\} \subseteq x\}$
7		df-dchr	$⊢ DChr = (n \in ℕ ⟼ ⦋ ℤ / n ℤ / z ⦌ ⦋ \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\} / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(b \times b)}⟩\})$
8		fvexd	$⊢ (φ \land n = N) \to ℤ / n ℤ \in V$
9		ovex	$⊢ {mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}} \in V$
10	9	rabex	$⊢ \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\} \in V$
11	10	a1i	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\} \in V$
12	6	ad2antrr	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to D = \{x \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \| (B ∖ U) \times \{0\} \subseteq x\}$
13		simpr	$⊢ (φ \land n = N) \to n = N$
14	13	fveq2d	$⊢ (φ \land n = N) \to ℤ / n ℤ = ℤ / N ℤ$
15	2 14	eqtr4id	$⊢ (φ \land n = N) \to Z = ℤ / n ℤ$
16	15	eqeq2d	$⊢ (φ \land n = N) \to (z = Z \leftrightarrow z = ℤ / n ℤ)$
17	16	biimpar	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to z = Z$
18	17	fveq2d	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to {mulGrp}_{z} = {mulGrp}_{Z}$
19	18	oveq1d	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to {mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}} = {mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}$
20	17	fveq2d	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to {Base}_{z} = {Base}_{Z}$
21	20 3	eqtr4di	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to {Base}_{z} = B$
22	17	fveq2d	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to Unit (z) = Unit (Z)$
23	22 4	eqtr4di	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to Unit (z) = U$
24	21 23	difeq12d	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to {Base}_{z} ∖ Unit (z) = B ∖ U$
25	24	xpeq1d	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to ({Base}_{z} ∖ Unit (z)) \times \{0\} = (B ∖ U) \times \{0\}$
26	25	sseq1d	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to (({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x \leftrightarrow (B ∖ U) \times \{0\} \subseteq x)$
27	19 26	rabeqbidv	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\} = \{x \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \| (B ∖ U) \times \{0\} \subseteq x\}$
28	12 27	eqtr4d	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to D = \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\}$
29	28	eqeq2d	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to (b = D \leftrightarrow b = \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\})$
30	29	biimpar	$⊢ (((φ \land n = N) \land z = ℤ / n ℤ) \land b = \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\}) \to b = D$
31	30	opeq2d	$⊢ (((φ \land n = N) \land z = ℤ / n ℤ) \land b = \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\}) \to ⟨{Base}_{ndx}, b⟩ = ⟨{Base}_{ndx}, D⟩$
32	30	sqxpeqd	$⊢ (((φ \land n = N) \land z = ℤ / n ℤ) \land b = \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\}) \to b \times b = D \times D$
33	32	reseq2d	$⊢ (((φ \land n = N) \land z = ℤ / n ℤ) \land b = \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\}) \to {\circ_{f} \times ↾}_{(b \times b)} = {\circ_{f} \times ↾}_{(D \times D)}$
34	33	opeq2d	$⊢ (((φ \land n = N) \land z = ℤ / n ℤ) \land b = \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\}) \to ⟨+_{ndx}, {\circ_{f} \times ↾}_{(b \times b)}⟩ = ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩$
35	31 34	preq12d	$⊢ (((φ \land n = N) \land z = ℤ / n ℤ) \land b = \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\}) \to \{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(b \times b)}⟩\} = \{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\}$
36	11 35	csbied	$⊢ ((φ \land n = N) \land z = ℤ / n ℤ) \to ⦋ \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\} / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(b \times b)}⟩\} = \{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\}$
37	8 36	csbied	$⊢ (φ \land n = N) \to ⦋ ℤ / n ℤ / z ⦌ ⦋ \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\} / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(b \times b)}⟩\} = \{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\}$
38		prex	$⊢ \{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\} \in V$
39	38	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\} \in V$
40	7 37 5 39	fvmptd2	$⊢ φ \to DChr (N) = \{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\}$
41	1 40	syl5eq	$⊢ φ \to G = \{⟨{Base}_{ndx}, D⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(D \times D)}⟩\}$

Metamath Proof Explorer

Theorem dchrval

Proof