dchrmulcl

Description: Closure of the group operation on 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	dchrmulcl	$⊢ φ \to X \underset{˙}{\cdot} Y \in D$

Proof

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 2 3 4 5 6	dchrmul	$⊢ φ \to X \underset{˙}{\cdot} Y = X \times_{f} Y$
8		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
9	8	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ)) \to x y \in ℂ$
10		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
11	1 2 3 10 5	dchrf	$⊢ φ \to X : {Base}_{Z} ⟶ ℂ$
12	1 2 3 10 6	dchrf	$⊢ φ \to Y : {Base}_{Z} ⟶ ℂ$
13		fvexd	$⊢ φ \to {Base}_{Z} \in V$
14		inidm	$⊢ {Base}_{Z} \cap {Base}_{Z} = {Base}_{Z}$
15	9 11 12 13 13 14	off	$⊢ φ \to (X \times_{f} Y) : {Base}_{Z} ⟶ ℂ$
16		eqid	$⊢ Unit (Z) = Unit (Z)$
17	10 16	unitcl	$⊢ x \in Unit (Z) \to x \in {Base}_{Z}$
18	10 16	unitcl	$⊢ y \in Unit (Z) \to y \in {Base}_{Z}$
19	17 18	anim12i	$⊢ (x \in Unit (Z) \land y \in Unit (Z)) \to (x \in {Base}_{Z} \land y \in {Base}_{Z})$
20	1 3	dchrrcl	$⊢ X \in D \to N \in ℕ$
21	5 20	syl	$⊢ φ \to N \in ℕ$
22	1 2 10 16 21 3	dchrelbas2	$⊢ φ \to (X \in D \leftrightarrow (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in {Base}_{Z} (X (x) \neq 0 \to x \in Unit (Z))))$
23	5 22	mpbid	$⊢ φ \to (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in {Base}_{Z} (X (x) \neq 0 \to x \in Unit (Z)))$
24	23	simpld	$⊢ φ \to X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})$
25		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
26	25 10	mgpbas	$⊢ {Base}_{Z} = {Base}_{{mulGrp}_{Z}}$
27		eqid	$⊢ \cdot_{Z} = \cdot_{Z}$
28	25 27	mgpplusg	$⊢ \cdot_{Z} = +_{{mulGrp}_{Z}}$
29		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
30		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
31	29 30	mgpplusg	$⊢ \times = +_{{mulGrp}_{ℂ_{fld}}}$
32	26 28 31	mhmlin	$⊢ (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land x \in {Base}_{Z} \land y \in {Base}_{Z}) \to X (x \cdot_{Z} y) = X (x) X (y)$
33	32	3expb	$⊢ (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to X (x \cdot_{Z} y) = X (x) X (y)$
34	24 33	sylan	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to X (x \cdot_{Z} y) = X (x) X (y)$
35	1 2 10 16 21 3	dchrelbas2	$⊢ φ \to (Y \in D \leftrightarrow (Y \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in {Base}_{Z} (Y (x) \neq 0 \to x \in Unit (Z))))$
36	6 35	mpbid	$⊢ φ \to (Y \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land \forall x \in {Base}_{Z} (Y (x) \neq 0 \to x \in Unit (Z)))$
37	36	simpld	$⊢ φ \to Y \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})$
38	26 28 31	mhmlin	$⊢ (Y \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land x \in {Base}_{Z} \land y \in {Base}_{Z}) \to Y (x \cdot_{Z} y) = Y (x) Y (y)$
39	38	3expb	$⊢ (Y \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to Y (x \cdot_{Z} y) = Y (x) Y (y)$
40	37 39	sylan	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to Y (x \cdot_{Z} y) = Y (x) Y (y)$
41	34 40	oveq12d	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to X (x \cdot_{Z} y) Y (x \cdot_{Z} y) = X (x) X (y) Y (x) Y (y)$
42	11	ffvelcdmda	$⊢ (φ \land x \in {Base}_{Z}) \to X (x) \in ℂ$
43	42	adantrr	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to X (x) \in ℂ$
44		simpr	$⊢ (x \in {Base}_{Z} \land y \in {Base}_{Z}) \to y \in {Base}_{Z}$
45		ffvelcdm	$⊢ (X : {Base}_{Z} ⟶ ℂ \land y \in {Base}_{Z}) \to X (y) \in ℂ$
46	11 44 45	syl2an	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to X (y) \in ℂ$
47	12	ffvelcdmda	$⊢ (φ \land x \in {Base}_{Z}) \to Y (x) \in ℂ$
48	47	adantrr	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to Y (x) \in ℂ$
49		ffvelcdm	$⊢ (Y : {Base}_{Z} ⟶ ℂ \land y \in {Base}_{Z}) \to Y (y) \in ℂ$
50	12 44 49	syl2an	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to Y (y) \in ℂ$
51	43 46 48 50	mul4d	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to X (x) X (y) Y (x) Y (y) = X (x) Y (x) X (y) Y (y)$
52	41 51	eqtrd	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to X (x \cdot_{Z} y) Y (x \cdot_{Z} y) = X (x) Y (x) X (y) Y (y)$
53	11	ffnd	$⊢ φ \to X Fn {Base}_{Z}$
54	53	adantr	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to X Fn {Base}_{Z}$
55	12	ffnd	$⊢ φ \to Y Fn {Base}_{Z}$
56	55	adantr	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to Y Fn {Base}_{Z}$
57		fvexd	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to {Base}_{Z} \in V$
58	21	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
59	2	zncrng	$⊢ N \in ℕ_{0} \to Z \in CRing$
60		crngring	$⊢ Z \in CRing \to Z \in Ring$
61	58 59 60	3syl	$⊢ φ \to Z \in Ring$
62	10 27	ringcl	$⊢ (Z \in Ring \land x \in {Base}_{Z} \land y \in {Base}_{Z}) \to x \cdot_{Z} y \in {Base}_{Z}$
63	62	3expb	$⊢ (Z \in Ring \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to x \cdot_{Z} y \in {Base}_{Z}$
64	61 63	sylan	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to x \cdot_{Z} y \in {Base}_{Z}$
65		fnfvof	$⊢ ((X Fn {Base}_{Z} \land Y Fn {Base}_{Z}) \land ({Base}_{Z} \in V \land x \cdot_{Z} y \in {Base}_{Z})) \to (X \times_{f} Y) (x \cdot_{Z} y) = X (x \cdot_{Z} y) Y (x \cdot_{Z} y)$
66	54 56 57 64 65	syl22anc	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to (X \times_{f} Y) (x \cdot_{Z} y) = X (x \cdot_{Z} y) Y (x \cdot_{Z} y)$
67	53	adantr	$⊢ (φ \land x \in {Base}_{Z}) \to X Fn {Base}_{Z}$
68	55	adantr	$⊢ (φ \land x \in {Base}_{Z}) \to Y Fn {Base}_{Z}$
69		fvexd	$⊢ (φ \land x \in {Base}_{Z}) \to {Base}_{Z} \in V$
70		simpr	$⊢ (φ \land x \in {Base}_{Z}) \to x \in {Base}_{Z}$
71		fnfvof	$⊢ ((X Fn {Base}_{Z} \land Y Fn {Base}_{Z}) \land ({Base}_{Z} \in V \land x \in {Base}_{Z})) \to (X \times_{f} Y) (x) = X (x) Y (x)$
72	67 68 69 70 71	syl22anc	$⊢ (φ \land x \in {Base}_{Z}) \to (X \times_{f} Y) (x) = X (x) Y (x)$
73	72	adantrr	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to (X \times_{f} Y) (x) = X (x) Y (x)$
74		simprr	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to y \in {Base}_{Z}$
75		fnfvof	$⊢ ((X Fn {Base}_{Z} \land Y Fn {Base}_{Z}) \land ({Base}_{Z} \in V \land y \in {Base}_{Z})) \to (X \times_{f} Y) (y) = X (y) Y (y)$
76	54 56 57 74 75	syl22anc	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to (X \times_{f} Y) (y) = X (y) Y (y)$
77	73 76	oveq12d	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to (X \times_{f} Y) (x) (X \times_{f} Y) (y) = X (x) Y (x) X (y) Y (y)$
78	52 66 77	3eqtr4d	$⊢ (φ \land (x \in {Base}_{Z} \land y \in {Base}_{Z})) \to (X \times_{f} Y) (x \cdot_{Z} y) = (X \times_{f} Y) (x) (X \times_{f} Y) (y)$
79	19 78	sylan2	$⊢ (φ \land (x \in Unit (Z) \land y \in Unit (Z))) \to (X \times_{f} Y) (x \cdot_{Z} y) = (X \times_{f} Y) (x) (X \times_{f} Y) (y)$
80	79	ralrimivva	$⊢ φ \to \forall x \in Unit (Z) \forall y \in Unit (Z) (X \times_{f} Y) (x \cdot_{Z} y) = (X \times_{f} Y) (x) (X \times_{f} Y) (y)$
81		eqid	$⊢ 1_{Z} = 1_{Z}$
82	10 81	ringidcl	$⊢ Z \in Ring \to 1_{Z} \in {Base}_{Z}$
83	61 82	syl	$⊢ φ \to 1_{Z} \in {Base}_{Z}$
84		fnfvof	$⊢ ((X Fn {Base}_{Z} \land Y Fn {Base}_{Z}) \land ({Base}_{Z} \in V \land 1_{Z} \in {Base}_{Z})) \to (X \times_{f} Y) (1_{Z}) = X (1_{Z}) Y (1_{Z})$
85	53 55 13 83 84	syl22anc	$⊢ φ \to (X \times_{f} Y) (1_{Z}) = X (1_{Z}) Y (1_{Z})$
86	25 81	ringidval	$⊢ 1_{Z} = 0_{{mulGrp}_{Z}}$
87		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
88	29 87	ringidval	$⊢ 1 = 0_{{mulGrp}_{ℂ_{fld}}}$
89	86 88	mhm0	$⊢ X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \to X (1_{Z}) = 1$
90	24 89	syl	$⊢ φ \to X (1_{Z}) = 1$
91	86 88	mhm0	$⊢ Y \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \to Y (1_{Z}) = 1$
92	37 91	syl	$⊢ φ \to Y (1_{Z}) = 1$
93	90 92	oveq12d	$⊢ φ \to X (1_{Z}) Y (1_{Z}) = 1 \cdot 1$
94		1t1e1	$⊢ 1 \cdot 1 = 1$
95	93 94	eqtrdi	$⊢ φ \to X (1_{Z}) Y (1_{Z}) = 1$
96	85 95	eqtrd	$⊢ φ \to (X \times_{f} Y) (1_{Z}) = 1$
97	72	neeq1d	$⊢ (φ \land x \in {Base}_{Z}) \to ((X \times_{f} Y) (x) \neq 0 \leftrightarrow X (x) Y (x) \neq 0)$
98	42 47	mulne0bd	$⊢ (φ \land x \in {Base}_{Z}) \to ((X (x) \neq 0 \land Y (x) \neq 0) \leftrightarrow X (x) Y (x) \neq 0)$
99	97 98	bitr4d	$⊢ (φ \land x \in {Base}_{Z}) \to ((X \times_{f} Y) (x) \neq 0 \leftrightarrow (X (x) \neq 0 \land Y (x) \neq 0))$
100	23	simprd	$⊢ φ \to \forall x \in {Base}_{Z} (X (x) \neq 0 \to x \in Unit (Z))$
101	100	r19.21bi	$⊢ (φ \land x \in {Base}_{Z}) \to (X (x) \neq 0 \to x \in Unit (Z))$
102	101	adantrd	$⊢ (φ \land x \in {Base}_{Z}) \to ((X (x) \neq 0 \land Y (x) \neq 0) \to x \in Unit (Z))$
103	99 102	sylbid	$⊢ (φ \land x \in {Base}_{Z}) \to ((X \times_{f} Y) (x) \neq 0 \to x \in Unit (Z))$
104	103	ralrimiva	$⊢ φ \to \forall x \in {Base}_{Z} ((X \times_{f} Y) (x) \neq 0 \to x \in Unit (Z))$
105	80 96 104	3jca	$⊢ φ \to (\forall x \in Unit (Z) \forall y \in Unit (Z) (X \times_{f} Y) (x \cdot_{Z} y) = (X \times_{f} Y) (x) (X \times_{f} Y) (y) \land (X \times_{f} Y) (1_{Z}) = 1 \land \forall x \in {Base}_{Z} ((X \times_{f} Y) (x) \neq 0 \to x \in Unit (Z)))$
106	1 2 10 16 21 3	dchrelbas3	$⊢ φ \to (X \times_{f} Y \in D \leftrightarrow ((X \times_{f} Y) : {Base}_{Z} ⟶ ℂ \land (\forall x \in Unit (Z) \forall y \in Unit (Z) (X \times_{f} Y) (x \cdot_{Z} y) = (X \times_{f} Y) (x) (X \times_{f} Y) (y) \land (X \times_{f} Y) (1_{Z}) = 1 \land \forall x \in {Base}_{Z} ((X \times_{f} Y) (x) \neq 0 \to x \in Unit (Z)))))$
107	15 105 106	mpbir2and	$⊢ φ \to X \times_{f} Y \in D$
108	7 107	eqeltrd	$⊢ φ \to X \underset{˙}{\cdot} Y \in D$

Metamath Proof Explorer

Theorem dchrmulcl

Proof