sumdchr2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > sumdchr2		Structured version Visualization version GIF version

Theorem sumdchr2 27158

Description: Lemma for sumdchr 27160. (Contributed by Mario Carneiro, 28-Apr-2016.)

**Hypotheses**
Ref	Expression
sumdchr.g	⊢ 𝐺 = (DChr‘𝑁)
sumdchr.d	⊢ 𝐷 = (Base‘𝐺)
sumdchr2.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
sumdchr2.1	⊢ 1 = (1_r‘𝑍)
sumdchr2.b	⊢ 𝐵 = (Base‘𝑍)
sumdchr2.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
sumdchr2.x	⊢ (𝜑 → 𝐴 ∈ 𝐵)

**Assertion**
Ref	Expression
sumdchr2	⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0))

Distinct variable groups: 𝑥, 1 𝑥,𝐴 𝑥,𝐷 𝑥,𝑁 𝑥,𝐺 𝜑,𝑥 Allowed substitution hints: 𝐵(𝑥) 𝑍(𝑥)

Proof of Theorem sumdchr2 Dummy variables 𝑦 𝑧 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2738	. 2 ⊢ ((♯‘𝐷) = if(𝐴 = 1 , (♯‘𝐷), 0) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = (♯‘𝐷) ↔ Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0)))
2		eqeq2 2738	. 2 ⊢ (0 = if(𝐴 = 1 , (♯‘𝐷), 0) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0 ↔ Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0)))
3		fveq2 6885	. . . . . 6 ⊢ (𝐴 = 1 → (𝑥‘𝐴) = (𝑥‘ 1 ))
4		sumdchr.g	. . . . . . . . 9 ⊢ 𝐺 = (DChr‘𝑁)
5		sumdchr2.z	. . . . . . . . 9 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
6		sumdchr.d	. . . . . . . . 9 ⊢ 𝐷 = (Base‘𝐺)
7	4, 5, 6	dchrmhm 27129	. . . . . . . 8 ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld))
8		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
9	7, 8	sselid 3975	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)))
10		eqid 2726	. . . . . . . . 9 ⊢ (mulGrp‘𝑍) = (mulGrp‘𝑍)
11		sumdchr2.1	. . . . . . . . 9 ⊢ 1 = (1_r‘𝑍)
12	10, 11	ringidval 20088	. . . . . . . 8 ⊢ 1 = (0_g‘(mulGrp‘𝑍))
13		eqid 2726	. . . . . . . . 9 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
14		cnfld1 21282	. . . . . . . . 9 ⊢ 1 = (1_r‘ℂ_fld)
15	13, 14	ringidval 20088	. . . . . . . 8 ⊢ 1 = (0_g‘(mulGrp‘ℂ_fld))
16	12, 15	mhm0 18724	. . . . . . 7 ⊢ (𝑥 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)) → (𝑥‘ 1 ) = 1)
17	9, 16	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥‘ 1 ) = 1)
18	3, 17	sylan9eqr 2788	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝐴 = 1 ) → (𝑥‘𝐴) = 1)
19	18	an32s 649	. . . 4 ⊢ (((𝜑 ∧ 𝐴 = 1 ) ∧ 𝑥 ∈ 𝐷) → (𝑥‘𝐴) = 1)
20	19	sumeq2dv 15655	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = Σ𝑥 ∈ 𝐷 1)
21		sumdchr2.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ)
22	4, 6	dchrfi 27143	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin)
23	21, 22	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ Fin)
24		ax-1cn 11170	. . . . . 6 ⊢ 1 ∈ ℂ
25		fsumconst 15742	. . . . . 6 ⊢ ((𝐷 ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑥 ∈ 𝐷 1 = ((♯‘𝐷) · 1))
26	23, 24, 25	sylancl 585	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 1 = ((♯‘𝐷) · 1))
27		hashcl 14321	. . . . . . . 8 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
28	21, 22, 27	3syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
29	28	nn0cnd 12538	. . . . . 6 ⊢ (𝜑 → (♯‘𝐷) ∈ ℂ)
30	29	mulridd 11235	. . . . 5 ⊢ (𝜑 → ((♯‘𝐷) · 1) = (♯‘𝐷))
31	26, 30	eqtrd 2766	. . . 4 ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 1 = (♯‘𝐷))
32	31	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 1 = (♯‘𝐷))
33	20, 32	eqtrd 2766	. 2 ⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = (♯‘𝐷))
34		df-ne 2935	. . 3 ⊢ (𝐴 ≠ 1 ↔ ¬ 𝐴 = 1 )
35		sumdchr2.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑍)
36	21	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ≠ 1 ) → 𝑁 ∈ ℕ)
37		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ≠ 1 ) → 𝐴 ≠ 1 )
38		sumdchr2.x	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
39	38	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ≠ 1 ) → 𝐴 ∈ 𝐵)
40	4, 5, 6, 35, 11, 36, 37, 39	dchrpt 27155	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ≠ 1 ) → ∃𝑦 ∈ 𝐷 (𝑦‘𝐴) ≠ 1)
41	36	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝑁 ∈ ℕ)
42	41, 22	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝐷 ∈ Fin)
43		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
44	4, 5, 6, 35, 43	dchrf 27130	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐵⟶ℂ)
45	39	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝐴 ∈ 𝐵)
46	45	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝐵)
47	44, 46	ffvelcdmd 7081	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → (𝑥‘𝐴) ∈ ℂ)
48	42, 47	fsumcl 15685	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) ∈ ℂ)
49		0cnd 11211	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 0 ∈ ℂ)
50		simprl 768	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝑦 ∈ 𝐷)
51	4, 5, 6, 35, 50	dchrf 27130	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝑦:𝐵⟶ℂ)
52	51, 45	ffvelcdmd 7081	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (𝑦‘𝐴) ∈ ℂ)
53		subcl 11463	. . . . . 6 ⊢ (((𝑦‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑦‘𝐴) − 1) ∈ ℂ)
54	52, 24, 53	sylancl 585	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) − 1) ∈ ℂ)
55		simprr 770	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (𝑦‘𝐴) ≠ 1)
56		subeq0 11490	. . . . . . . 8 ⊢ (((𝑦‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑦‘𝐴) − 1) = 0 ↔ (𝑦‘𝐴) = 1))
57	52, 24, 56	sylancl 585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) = 0 ↔ (𝑦‘𝐴) = 1))
58	57	necon3bid 2979	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) ≠ 0 ↔ (𝑦‘𝐴) ≠ 1))
59	55, 58	mpbird 257	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) − 1) ≠ 0)
60		oveq2 7413	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑦(+_g‘𝐺)𝑧) = (𝑦(+_g‘𝐺)𝑥))
61	60	fveq1d 6887	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → ((𝑦(+_g‘𝐺)𝑧)‘𝐴) = ((𝑦(+_g‘𝐺)𝑥)‘𝐴))
62	61	cbvsumv 15648	. . . . . . . . . 10 ⊢ Σ𝑧 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑧)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑥)‘𝐴)
63		eqid 2726	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
64	50	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦 ∈ 𝐷)
65	4, 5, 6, 63, 64, 43	dchrmul 27136	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → (𝑦(+_g‘𝐺)𝑥) = (𝑦 ∘_f · 𝑥))
66	65	fveq1d 6887	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → ((𝑦(+_g‘𝐺)𝑥)‘𝐴) = ((𝑦 ∘_f · 𝑥)‘𝐴))
67	51	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦:𝐵⟶ℂ)
68	67	ffnd 6712	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦 Fn 𝐵)
69	44	ffnd 6712	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑥 Fn 𝐵)
70	35	fvexi 6899	. . . . . . . . . . . . . 14 ⊢ 𝐵 ∈ V
71	70	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ V)
72		fnfvof 7684	. . . . . . . . . . . . 13 ⊢ (((𝑦 Fn 𝐵 ∧ 𝑥 Fn 𝐵) ∧ (𝐵 ∈ V ∧ 𝐴 ∈ 𝐵)) → ((𝑦 ∘_f · 𝑥)‘𝐴) = ((𝑦‘𝐴) · (𝑥‘𝐴)))
73	68, 69, 71, 46, 72	syl22anc 836	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → ((𝑦 ∘_f · 𝑥)‘𝐴) = ((𝑦‘𝐴) · (𝑥‘𝐴)))
74	66, 73	eqtrd 2766	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → ((𝑦(+_g‘𝐺)𝑥)‘𝐴) = ((𝑦‘𝐴) · (𝑥‘𝐴)))
75	74	sumeq2dv 15655	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑥)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴)))
76	62, 75	eqtrid 2778	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑧 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑧)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴)))
77		fveq1 6884	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦(+_g‘𝐺)𝑧) → (𝑥‘𝐴) = ((𝑦(+_g‘𝐺)𝑧)‘𝐴))
78	4	dchrabl 27142	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
79		ablgrp 19705	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
80	41, 78, 79	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝐺 ∈ Grp)
81		eqid 2726	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏))) = (𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))
82	81, 6, 63	grplactf1o 18972	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐷) → ((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦):𝐷–1-1-onto→𝐷)
83	80, 50, 82	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦):𝐷–1-1-onto→𝐷)
84	81, 6	grplactval 18970	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦)‘𝑧) = (𝑦(+_g‘𝐺)𝑧))
85	50, 84	sylan 579	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑧 ∈ 𝐷) → (((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦)‘𝑧) = (𝑦(+_g‘𝐺)𝑧))
86	77, 42, 83, 85, 47	fsumf1o 15675	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = Σ𝑧 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑧)‘𝐴))
87	42, 52, 47	fsummulc2 15736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴)))
88	76, 86, 87	3eqtr4rd 2777	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))
89	48	mullidd 11236	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))
90	88, 89	oveq12d 7423	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))) = (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) − Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)))
91	48	subidd 11563	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) − Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = 0)
92	90, 91	eqtrd 2766	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))) = 0)
93	24	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 1 ∈ ℂ)
94	52, 93, 48	subdird 11675	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))))
95	54	mul01d 11417	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · 0) = 0)
96	92, 94, 95	3eqtr4d 2776	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = (((𝑦‘𝐴) − 1) · 0))
97	48, 49, 54, 59, 96	mulcanad 11853	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0)
98	40, 97	rexlimddv 3155	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0)
99	34, 98	sylan2br 594	. 2 ⊢ ((𝜑 ∧ ¬ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0)
100	1, 2, 33, 99	ifbothda 4561	1 ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ≠ wne 2934 Vcvv 3468 ifcif 4523 ↦ cmpt 5224 Fn wfn 6532 ⟶wf 6533 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7405 ∘_f cof 7665 Fincfn 8941 ℂcc 11110 0cc0 11112 1c1 11113 · cmul 11117 − cmin 11448 ℕcn 12216 ℕ₀cn0 12476 ♯chash 14295 Σcsu 15638 Basecbs 17153 +_gcplusg 17206 MndHom cmhm 18711 Grpcgrp 18863 Abelcabl 19701 mulGrpcmgp 20039 1_rcur 20086 ℂ_fldccnfld 21240 ℤ/nℤczn 21389 DChrcdchr 27120

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7722 ax-inf2 9638 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190 ax-addf 11191 ax-mulf 11192

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4903 df-int 4944 df-iun 4992 df-iin 4993 df-disj 5107 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-se 5625 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6294 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7667 df-rpss 7710 df-om 7853 df-1st 7974 df-2nd 7975 df-supp 8147 df-tpos 8212 df-frecs 8267 df-wrecs 8298 df-recs 8372 df-rdg 8411 df-1o 8467 df-2o 8468 df-oadd 8471 df-omul 8472 df-er 8705 df-ec 8707 df-qs 8711 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-fi 9408 df-sup 9439 df-inf 9440 df-oi 9507 df-dju 9898 df-card 9936 df-acn 9939 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-xnn0 12549 df-z 12563 df-dec 12682 df-uz 12827 df-q 12937 df-rp 12981 df-xneg 13098 df-xadd 13099 df-xmul 13100 df-ioo 13334 df-ioc 13335 df-ico 13336 df-icc 13337 df-fz 13491 df-fzo 13634 df-fl 13763 df-mod 13841 df-seq 13973 df-exp 14033 df-fac 14239 df-bc 14268 df-hash 14296 df-word 14471 df-concat 14527 df-s1 14552 df-shft 15020 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-limsup 15421 df-clim 15438 df-rlim 15439 df-sum 15639 df-ef 16017 df-sin 16019 df-cos 16020 df-pi 16022 df-dvds 16205 df-gcd 16443 df-prm 16616 df-phi 16708 df-pc 16779 df-struct 17089 df-sets 17106 df-slot 17124 df-ndx 17136 df-base 17154 df-ress 17183 df-plusg 17219 df-mulr 17220 df-starv 17221 df-sca 17222 df-vsca 17223 df-ip 17224 df-tset 17225 df-ple 17226 df-ds 17228 df-unif 17229 df-hom 17230 df-cco 17231 df-rest 17377 df-topn 17378 df-0g 17396 df-gsum 17397 df-topgen 17398 df-pt 17399 df-prds 17402 df-xrs 17457 df-qtop 17462 df-imas 17463 df-qus 17464 df-xps 17465 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18573 df-sgrp 18652 df-mnd 18668 df-mhm 18713 df-submnd 18714 df-grp 18866 df-minusg 18867 df-sbg 18868 df-mulg 18996 df-subg 19050 df-nsg 19051 df-eqg 19052 df-ghm 19139 df-gim 19184 df-ga 19206 df-cntz 19233 df-oppg 19262 df-od 19448 df-gex 19449 df-pgp 19450 df-lsm 19556 df-pj1 19557 df-cmn 19702 df-abl 19703 df-cyg 19798 df-dprd 19917 df-dpj 19918 df-mgp 20040 df-rng 20058 df-ur 20087 df-ring 20140 df-cring 20141 df-oppr 20236 df-dvdsr 20259 df-unit 20260 df-invr 20290 df-rhm 20374 df-subrng 20446 df-subrg 20471 df-lmod 20708 df-lss 20779 df-lsp 20819 df-sra 21021 df-rgmod 21022 df-lidl 21067 df-rsp 21068 df-2idl 21107 df-psmet 21232 df-xmet 21233 df-met 21234 df-bl 21235 df-mopn 21236 df-fbas 21237 df-fg 21238 df-cnfld 21241 df-zring 21334 df-zrh 21390 df-zn 21393 df-top 22751 df-topon 22768 df-topsp 22790 df-bases 22804 df-cld 22878 df-ntr 22879 df-cls 22880 df-nei 22957 df-lp 22995 df-perf 22996 df-cn 23086 df-cnp 23087 df-haus 23174 df-tx 23421 df-hmeo 23614 df-fil 23705 df-fm 23797 df-flim 23798 df-flf 23799 df-xms 24181 df-ms 24182 df-tms 24183 df-cncf 24753 df-0p 25554 df-limc 25750 df-dv 25751 df-ply 26077 df-idp 26078 df-coe 26079 df-dgr 26080 df-quot 26181 df-log 26445 df-cxp 26446 df-dchr 27121

This theorem is referenced by: dchrhash 27159 sumdchr 27160

W3C validator