sumdchr2

	Ref	Expression
Hypotheses	sumdchr.g	$⊢ G = DChr (N)$
	sumdchr.d	$⊢ D = {Base}_{G}$
	sumdchr2.z	$⊢ Z = ℤ / N ℤ$
	sumdchr2.1	$⊢ \underset{˙}{1} = 1_{Z}$
	sumdchr2.b	$⊢ B = {Base}_{Z}$
	sumdchr2.n	$⊢ φ \to N \in ℕ$
	sumdchr2.x	$⊢ φ \to A \in B$
Assertion	sumdchr2	$⊢ φ \to \sum_{x \in D} x (A) = if (A = \underset{˙}{1}, \|D\|, 0)$

Proof

Step	Hyp	Ref	Expression
1		sumdchr.g	$⊢ G = DChr (N)$
2		sumdchr.d	$⊢ D = {Base}_{G}$
3		sumdchr2.z	$⊢ Z = ℤ / N ℤ$
4		sumdchr2.1	$⊢ \underset{˙}{1} = 1_{Z}$
5		sumdchr2.b	$⊢ B = {Base}_{Z}$
6		sumdchr2.n	$⊢ φ \to N \in ℕ$
7		sumdchr2.x	$⊢ φ \to A \in B$
8		eqeq2	$⊢ \|D\| = if (A = \underset{˙}{1}, \|D\|, 0) \to (\sum_{x \in D} x (A) = \|D\| \leftrightarrow \sum_{x \in D} x (A) = if (A = \underset{˙}{1}, \|D\|, 0))$
9		eqeq2	$⊢ 0 = if (A = \underset{˙}{1}, \|D\|, 0) \to (\sum_{x \in D} x (A) = 0 \leftrightarrow \sum_{x \in D} x (A) = if (A = \underset{˙}{1}, \|D\|, 0))$
10		fveq2	$⊢ A = \underset{˙}{1} \to x (A) = x (\underset{˙}{1})$
11	1 3 2	dchrmhm	$⊢ D \subseteq {mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}$
12		simpr	$⊢ (φ \land x \in D) \to x \in D$
13	11 12	sselid	$⊢ (φ \land x \in D) \to x \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})$
14		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
15	14 4	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{Z}}$
16		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
17		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
18	16 17	ringidval	$⊢ 1 = 0_{{mulGrp}_{ℂ_{fld}}}$
19	15 18	mhm0	$⊢ x \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \to x (\underset{˙}{1}) = 1$
20	13 19	syl	$⊢ (φ \land x \in D) \to x (\underset{˙}{1}) = 1$
21	10 20	sylan9eqr	$⊢ ((φ \land x \in D) \land A = \underset{˙}{1}) \to x (A) = 1$
22	21	an32s	$⊢ ((φ \land A = \underset{˙}{1}) \land x \in D) \to x (A) = 1$
23	22	sumeq2dv	$⊢ (φ \land A = \underset{˙}{1}) \to \sum_{x \in D} x (A) = \sum_{x \in D} 1$
24	1 2	dchrfi	$⊢ N \in ℕ \to D \in Fin$
25	6 24	syl	$⊢ φ \to D \in Fin$
26		ax-1cn	$⊢ 1 \in ℂ$
27		fsumconst	$⊢ (D \in Fin \land 1 \in ℂ) \to \sum_{x \in D} 1 = \|D\| \cdot 1$
28	25 26 27	sylancl	$⊢ φ \to \sum_{x \in D} 1 = \|D\| \cdot 1$
29		hashcl	$⊢ D \in Fin \to \|D\| \in ℕ_{0}$
30	6 24 29	3syl	$⊢ φ \to \|D\| \in ℕ_{0}$
31	30	nn0cnd	$⊢ φ \to \|D\| \in ℂ$
32	31	mulid1d	$⊢ φ \to \|D\| \cdot 1 = \|D\|$
33	28 32	eqtrd	$⊢ φ \to \sum_{x \in D} 1 = \|D\|$
34	33	adantr	$⊢ (φ \land A = \underset{˙}{1}) \to \sum_{x \in D} 1 = \|D\|$
35	23 34	eqtrd	$⊢ (φ \land A = \underset{˙}{1}) \to \sum_{x \in D} x (A) = \|D\|$
36		df-ne	$⊢ A \neq \underset{˙}{1} \leftrightarrow \neg A = \underset{˙}{1}$
37	6	adantr	$⊢ (φ \land A \neq \underset{˙}{1}) \to N \in ℕ$
38		simpr	$⊢ (φ \land A \neq \underset{˙}{1}) \to A \neq \underset{˙}{1}$
39	7	adantr	$⊢ (φ \land A \neq \underset{˙}{1}) \to A \in B$
40	1 3 2 5 4 37 38 39	dchrpt	$⊢ (φ \land A \neq \underset{˙}{1}) \to \exists y \in D y (A) \neq 1$
41	37	adantr	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to N \in ℕ$
42	41 24	syl	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to D \in Fin$
43		simpr	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to x \in D$
44	1 3 2 5 43	dchrf	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to x : B ⟶ ℂ$
45	39	adantr	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to A \in B$
46	45	adantr	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to A \in B$
47	44 46	ffvelrnd	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to x (A) \in ℂ$
48	42 47	fsumcl	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to \sum_{x \in D} x (A) \in ℂ$
49		0cnd	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to 0 \in ℂ$
50		simprl	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to y \in D$
51	1 3 2 5 50	dchrf	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to y : B ⟶ ℂ$
52	51 45	ffvelrnd	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to y (A) \in ℂ$
53		subcl	$⊢ (y (A) \in ℂ \land 1 \in ℂ) \to y (A) - 1 \in ℂ$
54	52 26 53	sylancl	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to y (A) - 1 \in ℂ$
55		simprr	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to y (A) \neq 1$
56		subeq0	$⊢ (y (A) \in ℂ \land 1 \in ℂ) \to (y (A) - 1 = 0 \leftrightarrow y (A) = 1)$
57	52 26 56	sylancl	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to (y (A) - 1 = 0 \leftrightarrow y (A) = 1)$
58	57	necon3bid	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to (y (A) - 1 \neq 0 \leftrightarrow y (A) \neq 1)$
59	55 58	mpbird	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to y (A) - 1 \neq 0$
60		oveq2	$⊢ z = x \to y +_{G} z = y +_{G} x$
61	60	fveq1d	$⊢ z = x \to (y +_{G} z) (A) = (y +_{G} x) (A)$
62	61	cbvsumv	$⊢ \sum_{z \in D} (y +_{G} z) (A) = \sum_{x \in D} (y +_{G} x) (A)$
63		eqid	$⊢ +_{G} = +_{G}$
64	50	adantr	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to y \in D$
65	1 3 2 63 64 43	dchrmul	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to y +_{G} x = y \times_{f} x$
66	65	fveq1d	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to (y +_{G} x) (A) = (y \times_{f} x) (A)$
67	51	adantr	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to y : B ⟶ ℂ$
68	67	ffnd	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to y Fn B$
69	44	ffnd	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to x Fn B$
70	5	fvexi	$⊢ B \in V$
71	70	a1i	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to B \in V$
72		fnfvof	$⊢ ((y Fn B \land x Fn B) \land (B \in V \land A \in B)) \to (y \times_{f} x) (A) = y (A) x (A)$
73	68 69 71 46 72	syl22anc	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to (y \times_{f} x) (A) = y (A) x (A)$
74	66 73	eqtrd	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land x \in D) \to (y +_{G} x) (A) = y (A) x (A)$
75	74	sumeq2dv	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to \sum_{x \in D} (y +_{G} x) (A) = \sum_{x \in D} y (A) x (A)$
76	62 75	syl5eq	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to \sum_{z \in D} (y +_{G} z) (A) = \sum_{x \in D} y (A) x (A)$
77		fveq1	$⊢ x = y +_{G} z \to x (A) = (y +_{G} z) (A)$
78	1	dchrabl	$⊢ N \in ℕ \to G \in Abel$
79		ablgrp	$⊢ G \in Abel \to G \in Grp$
80	41 78 79	3syl	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to G \in Grp$
81		eqid	$⊢ (a \in D ⟼ (b \in D ⟼ a +_{G} b)) = (a \in D ⟼ (b \in D ⟼ a +_{G} b))$
82	81 2 63	grplactf1o	$⊢ (G \in Grp \land y \in D) \to (a \in D ⟼ (b \in D ⟼ a +_{G} b)) (y) : D \underset{1-1 onto}{⟶} D$
83	80 50 82	syl2anc	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to (a \in D ⟼ (b \in D ⟼ a +_{G} b)) (y) : D \underset{1-1 onto}{⟶} D$
84	81 2	grplactval	$⊢ (y \in D \land z \in D) \to (a \in D ⟼ (b \in D ⟼ a +_{G} b)) (y) (z) = y +_{G} z$
85	50 84	sylan	$⊢ (((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \land z \in D) \to (a \in D ⟼ (b \in D ⟼ a +_{G} b)) (y) (z) = y +_{G} z$
86	77 42 83 85 47	fsumf1o	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to \sum_{x \in D} x (A) = \sum_{z \in D} (y +_{G} z) (A)$
87	42 52 47	fsummulc2	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to y (A) \sum_{x \in D} x (A) = \sum_{x \in D} y (A) x (A)$
88	76 86 87	3eqtr4rd	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to y (A) \sum_{x \in D} x (A) = \sum_{x \in D} x (A)$
89	48	mulid2d	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to 1 \sum_{x \in D} x (A) = \sum_{x \in D} x (A)$
90	88 89	oveq12d	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to y (A) \sum_{x \in D} x (A) - 1 \sum_{x \in D} x (A) = \sum_{x \in D} x (A) - \sum_{x \in D} x (A)$
91	48	subidd	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to \sum_{x \in D} x (A) - \sum_{x \in D} x (A) = 0$
92	90 91	eqtrd	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to y (A) \sum_{x \in D} x (A) - 1 \sum_{x \in D} x (A) = 0$
93	26	a1i	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to 1 \in ℂ$
94	52 93 48	subdird	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to (y (A) - 1) \sum_{x \in D} x (A) = y (A) \sum_{x \in D} x (A) - 1 \sum_{x \in D} x (A)$
95	54	mul01d	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to (y (A) - 1) \cdot 0 = 0$
96	92 94 95	3eqtr4d	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to (y (A) - 1) \sum_{x \in D} x (A) = (y (A) - 1) \cdot 0$
97	48 49 54 59 96	mulcanad	$⊢ ((φ \land A \neq \underset{˙}{1}) \land (y \in D \land y (A) \neq 1)) \to \sum_{x \in D} x (A) = 0$
98	40 97	rexlimddv	$⊢ (φ \land A \neq \underset{˙}{1}) \to \sum_{x \in D} x (A) = 0$
99	36 98	sylan2br	$⊢ (φ \land \neg A = \underset{˙}{1}) \to \sum_{x \in D} x (A) = 0$
100	8 9 35 99	ifbothda	$⊢ φ \to \sum_{x \in D} x (A) = if (A = \underset{˙}{1}, \|D\|, 0)$

Metamath Proof Explorer

Theorem sumdchr2

Proof