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 26323

Description: Lemma for sumdchr 26325. (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 2750	. 2 ⊢ ((♯‘𝐷) = if(𝐴 = 1 , (♯‘𝐷), 0) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = (♯‘𝐷) ↔ Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0)))
2		eqeq2 2750	. 2 ⊢ (0 = if(𝐴 = 1 , (♯‘𝐷), 0) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0 ↔ Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0)))
3		fveq2 6756	. . . . . 6 ⊢ (𝐴 = 1 → (𝑥‘𝐴) = (𝑥‘ 1 ))
4		sumdchr.g	. . . . . . . . 9 ⊢ 𝐺 = (DChr‘𝑁)
5		sumdchr2.z	. . . . . . . . 9 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
6		sumdchr.d	. . . . . . . . 9 ⊢ 𝐷 = (Base‘𝐺)
7	4, 5, 6	dchrmhm 26294	. . . . . . . 8 ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld))
8		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
9	7, 8	sselid 3915	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)))
10		eqid 2738	. . . . . . . . 9 ⊢ (mulGrp‘𝑍) = (mulGrp‘𝑍)
11		sumdchr2.1	. . . . . . . . 9 ⊢ 1 = (1_r‘𝑍)
12	10, 11	ringidval 19654	. . . . . . . 8 ⊢ 1 = (0_g‘(mulGrp‘𝑍))
13		eqid 2738	. . . . . . . . 9 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
14		cnfld1 20535	. . . . . . . . 9 ⊢ 1 = (1_r‘ℂ_fld)
15	13, 14	ringidval 19654	. . . . . . . 8 ⊢ 1 = (0_g‘(mulGrp‘ℂ_fld))
16	12, 15	mhm0 18353	. . . . . . 7 ⊢ (𝑥 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)) → (𝑥‘ 1 ) = 1)
17	9, 16	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥‘ 1 ) = 1)
18	3, 17	sylan9eqr 2801	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝐴 = 1 ) → (𝑥‘𝐴) = 1)
19	18	an32s 648	. . . 4 ⊢ (((𝜑 ∧ 𝐴 = 1 ) ∧ 𝑥 ∈ 𝐷) → (𝑥‘𝐴) = 1)
20	19	sumeq2dv 15343	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = Σ𝑥 ∈ 𝐷 1)
21		sumdchr2.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ)
22	4, 6	dchrfi 26308	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin)
23	21, 22	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ Fin)
24		ax-1cn 10860	. . . . . 6 ⊢ 1 ∈ ℂ
25		fsumconst 15430	. . . . . 6 ⊢ ((𝐷 ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑥 ∈ 𝐷 1 = ((♯‘𝐷) · 1))
26	23, 24, 25	sylancl 585	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 1 = ((♯‘𝐷) · 1))
27		hashcl 13999	. . . . . . . 8 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
28	21, 22, 27	3syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
29	28	nn0cnd 12225	. . . . . 6 ⊢ (𝜑 → (♯‘𝐷) ∈ ℂ)
30	29	mulid1d 10923	. . . . 5 ⊢ (𝜑 → ((♯‘𝐷) · 1) = (♯‘𝐷))
31	26, 30	eqtrd 2778	. . . 4 ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 1 = (♯‘𝐷))
32	31	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 1 = (♯‘𝐷))
33	20, 32	eqtrd 2778	. 2 ⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = (♯‘𝐷))
34		df-ne 2943	. . 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 26320	. . . 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 26295	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐵⟶ℂ)
45	39	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝐴 ∈ 𝐵)
46	45	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝐵)
47	44, 46	ffvelrnd 6944	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → (𝑥‘𝐴) ∈ ℂ)
48	42, 47	fsumcl 15373	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) ∈ ℂ)
49		0cnd 10899	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 0 ∈ ℂ)
50		simprl 767	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝑦 ∈ 𝐷)
51	4, 5, 6, 35, 50	dchrf 26295	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝑦:𝐵⟶ℂ)
52	51, 45	ffvelrnd 6944	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (𝑦‘𝐴) ∈ ℂ)
53		subcl 11150	. . . . . 6 ⊢ (((𝑦‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑦‘𝐴) − 1) ∈ ℂ)
54	52, 24, 53	sylancl 585	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) − 1) ∈ ℂ)
55		simprr 769	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (𝑦‘𝐴) ≠ 1)
56		subeq0 11177	. . . . . . . 8 ⊢ (((𝑦‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑦‘𝐴) − 1) = 0 ↔ (𝑦‘𝐴) = 1))
57	52, 24, 56	sylancl 585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) = 0 ↔ (𝑦‘𝐴) = 1))
58	57	necon3bid 2987	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) ≠ 0 ↔ (𝑦‘𝐴) ≠ 1))
59	55, 58	mpbird 256	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) − 1) ≠ 0)
60		oveq2 7263	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑦(+_g‘𝐺)𝑧) = (𝑦(+_g‘𝐺)𝑥))
61	60	fveq1d 6758	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → ((𝑦(+_g‘𝐺)𝑧)‘𝐴) = ((𝑦(+_g‘𝐺)𝑥)‘𝐴))
62	61	cbvsumv 15336	. . . . . . . . . 10 ⊢ Σ𝑧 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑧)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑥)‘𝐴)
63		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
64	50	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦 ∈ 𝐷)
65	4, 5, 6, 63, 64, 43	dchrmul 26301	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → (𝑦(+_g‘𝐺)𝑥) = (𝑦 ∘_f · 𝑥))
66	65	fveq1d 6758	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → ((𝑦(+_g‘𝐺)𝑥)‘𝐴) = ((𝑦 ∘_f · 𝑥)‘𝐴))
67	51	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦:𝐵⟶ℂ)
68	67	ffnd 6585	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦 Fn 𝐵)
69	44	ffnd 6585	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑥 Fn 𝐵)
70	35	fvexi 6770	. . . . . . . . . . . . . 14 ⊢ 𝐵 ∈ V
71	70	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ V)
72		fnfvof 7528	. . . . . . . . . . . . 13 ⊢ (((𝑦 Fn 𝐵 ∧ 𝑥 Fn 𝐵) ∧ (𝐵 ∈ V ∧ 𝐴 ∈ 𝐵)) → ((𝑦 ∘_f · 𝑥)‘𝐴) = ((𝑦‘𝐴) · (𝑥‘𝐴)))
73	68, 69, 71, 46, 72	syl22anc 835	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → ((𝑦 ∘_f · 𝑥)‘𝐴) = ((𝑦‘𝐴) · (𝑥‘𝐴)))
74	66, 73	eqtrd 2778	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → ((𝑦(+_g‘𝐺)𝑥)‘𝐴) = ((𝑦‘𝐴) · (𝑥‘𝐴)))
75	74	sumeq2dv 15343	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑥)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴)))
76	62, 75	syl5eq 2791	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑧 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑧)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴)))
77		fveq1 6755	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦(+_g‘𝐺)𝑧) → (𝑥‘𝐴) = ((𝑦(+_g‘𝐺)𝑧)‘𝐴))
78	4	dchrabl 26307	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
79		ablgrp 19306	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
80	41, 78, 79	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝐺 ∈ Grp)
81		eqid 2738	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏))) = (𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))
82	81, 6, 63	grplactf1o 18594	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐷) → ((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦):𝐷–1-1-onto→𝐷)
83	80, 50, 82	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦):𝐷–1-1-onto→𝐷)
84	81, 6	grplactval 18592	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦)‘𝑧) = (𝑦(+_g‘𝐺)𝑧))
85	50, 84	sylan 579	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑧 ∈ 𝐷) → (((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦)‘𝑧) = (𝑦(+_g‘𝐺)𝑧))
86	77, 42, 83, 85, 47	fsumf1o 15363	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = Σ𝑧 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑧)‘𝐴))
87	42, 52, 47	fsummulc2 15424	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴)))
88	76, 86, 87	3eqtr4rd 2789	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))
89	48	mulid2d 10924	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))
90	88, 89	oveq12d 7273	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))) = (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) − Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)))
91	48	subidd 11250	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) − Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = 0)
92	90, 91	eqtrd 2778	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))) = 0)
93	24	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 1 ∈ ℂ)
94	52, 93, 48	subdird 11362	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))))
95	54	mul01d 11104	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · 0) = 0)
96	92, 94, 95	3eqtr4d 2788	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = (((𝑦‘𝐴) − 1) · 0))
97	48, 49, 54, 59, 96	mulcanad 11540	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0)
98	40, 97	rexlimddv 3219	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0)
99	34, 98	sylan2br 594	. 2 ⊢ ((𝜑 ∧ ¬ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0)
100	1, 2, 33, 99	ifbothda 4494	1 ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 Vcvv 3422 ifcif 4456 ↦ cmpt 5153 Fn wfn 6413 ⟶wf 6414 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 ∘_f cof 7509 Fincfn 8691 ℂcc 10800 0cc0 10802 1c1 10803 · cmul 10807 − cmin 11135 ℕcn 11903 ℕ₀cn0 12163 ♯chash 13972 Σcsu 15325 Basecbs 16840 +_gcplusg 16888 MndHom cmhm 18343 Grpcgrp 18492 Abelcabl 19302 mulGrpcmgp 19635 1_rcur 19652 ℂ_fldccnfld 20510 ℤ/nℤczn 20616 DChrcdchr 26285

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-addf 10881 ax-mulf 10882

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-disj 5036 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-rpss 7554 df-om 7688 df-1st 7804 df-2nd 7805 df-supp 7949 df-tpos 8013 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-oadd 8271 df-omul 8272 df-er 8456 df-ec 8458 df-qs 8462 df-map 8575 df-pm 8576 df-ixp 8644 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fsupp 9059 df-fi 9100 df-sup 9131 df-inf 9132 df-oi 9199 df-dju 9590 df-card 9628 df-acn 9631 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-xnn0 12236 df-z 12250 df-dec 12367 df-uz 12512 df-q 12618 df-rp 12660 df-xneg 12777 df-xadd 12778 df-xmul 12779 df-ioo 13012 df-ioc 13013 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-fl 13440 df-mod 13518 df-seq 13650 df-exp 13711 df-fac 13916 df-bc 13945 df-hash 13973 df-word 14146 df-concat 14202 df-s1 14229 df-shft 14706 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-limsup 15108 df-clim 15125 df-rlim 15126 df-sum 15326 df-ef 15705 df-sin 15707 df-cos 15708 df-pi 15710 df-dvds 15892 df-gcd 16130 df-prm 16305 df-phi 16395 df-pc 16466 df-struct 16776 df-sets 16793 df-slot 16811 df-ndx 16823 df-base 16841 df-ress 16868 df-plusg 16901 df-mulr 16902 df-starv 16903 df-sca 16904 df-vsca 16905 df-ip 16906 df-tset 16907 df-ple 16908 df-ds 16910 df-unif 16911 df-hom 16912 df-cco 16913 df-rest 17050 df-topn 17051 df-0g 17069 df-gsum 17070 df-topgen 17071 df-pt 17072 df-prds 17075 df-xrs 17130 df-qtop 17135 df-imas 17136 df-qus 17137 df-xps 17138 df-mre 17212 df-mrc 17213 df-acs 17215 df-mgm 18241 df-sgrp 18290 df-mnd 18301 df-mhm 18345 df-submnd 18346 df-grp 18495 df-minusg 18496 df-sbg 18497 df-mulg 18616 df-subg 18667 df-nsg 18668 df-eqg 18669 df-ghm 18747 df-gim 18790 df-ga 18811 df-cntz 18838 df-oppg 18865 df-od 19051 df-gex 19052 df-pgp 19053 df-lsm 19156 df-pj1 19157 df-cmn 19303 df-abl 19304 df-cyg 19393 df-dprd 19513 df-dpj 19514 df-mgp 19636 df-ur 19653 df-ring 19700 df-cring 19701 df-oppr 19777 df-dvdsr 19798 df-unit 19799 df-invr 19829 df-rnghom 19874 df-subrg 19937 df-lmod 20040 df-lss 20109 df-lsp 20149 df-sra 20349 df-rgmod 20350 df-lidl 20351 df-rsp 20352 df-2idl 20416 df-psmet 20502 df-xmet 20503 df-met 20504 df-bl 20505 df-mopn 20506 df-fbas 20507 df-fg 20508 df-cnfld 20511 df-zring 20583 df-zrh 20617 df-zn 20620 df-top 21951 df-topon 21968 df-topsp 21990 df-bases 22004 df-cld 22078 df-ntr 22079 df-cls 22080 df-nei 22157 df-lp 22195 df-perf 22196 df-cn 22286 df-cnp 22287 df-haus 22374 df-tx 22621 df-hmeo 22814 df-fil 22905 df-fm 22997 df-flim 22998 df-flf 22999 df-xms 23381 df-ms 23382 df-tms 23383 df-cncf 23947 df-0p 24739 df-limc 24935 df-dv 24936 df-ply 25254 df-idp 25255 df-coe 25256 df-dgr 25257 df-quot 25356 df-log 25617 df-cxp 25618 df-dchr 26286

This theorem is referenced by: dchrhash 26324 sumdchr 26325

W3C validator