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 27329

Description: Lemma for sumdchr 27331. (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 2747	. 2 ⊢ ((♯‘𝐷) = if(𝐴 = 1 , (♯‘𝐷), 0) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = (♯‘𝐷) ↔ Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0)))
2		eqeq2 2747	. 2 ⊢ (0 = if(𝐴 = 1 , (♯‘𝐷), 0) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0 ↔ Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0)))
3		fveq2 6907	. . . . . 6 ⊢ (𝐴 = 1 → (𝑥‘𝐴) = (𝑥‘ 1 ))
4		sumdchr.g	. . . . . . . . 9 ⊢ 𝐺 = (DChr‘𝑁)
5		sumdchr2.z	. . . . . . . . 9 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
6		sumdchr.d	. . . . . . . . 9 ⊢ 𝐷 = (Base‘𝐺)
7	4, 5, 6	dchrmhm 27300	. . . . . . . 8 ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld))
8		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
9	7, 8	sselid 3993	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)))
10		eqid 2735	. . . . . . . . 9 ⊢ (mulGrp‘𝑍) = (mulGrp‘𝑍)
11		sumdchr2.1	. . . . . . . . 9 ⊢ 1 = (1_r‘𝑍)
12	10, 11	ringidval 20201	. . . . . . . 8 ⊢ 1 = (0_g‘(mulGrp‘𝑍))
13		eqid 2735	. . . . . . . . 9 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
14		cnfld1 21424	. . . . . . . . 9 ⊢ 1 = (1_r‘ℂ_fld)
15	13, 14	ringidval 20201	. . . . . . . 8 ⊢ 1 = (0_g‘(mulGrp‘ℂ_fld))
16	12, 15	mhm0 18820	. . . . . . 7 ⊢ (𝑥 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)) → (𝑥‘ 1 ) = 1)
17	9, 16	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥‘ 1 ) = 1)
18	3, 17	sylan9eqr 2797	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝐴 = 1 ) → (𝑥‘𝐴) = 1)
19	18	an32s 652	. . . 4 ⊢ (((𝜑 ∧ 𝐴 = 1 ) ∧ 𝑥 ∈ 𝐷) → (𝑥‘𝐴) = 1)
20	19	sumeq2dv 15735	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = Σ𝑥 ∈ 𝐷 1)
21		sumdchr2.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ)
22	4, 6	dchrfi 27314	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin)
23	21, 22	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ Fin)
24		ax-1cn 11211	. . . . . 6 ⊢ 1 ∈ ℂ
25		fsumconst 15823	. . . . . 6 ⊢ ((𝐷 ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑥 ∈ 𝐷 1 = ((♯‘𝐷) · 1))
26	23, 24, 25	sylancl 586	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 1 = ((♯‘𝐷) · 1))
27		hashcl 14392	. . . . . . . 8 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
28	21, 22, 27	3syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
29	28	nn0cnd 12587	. . . . . 6 ⊢ (𝜑 → (♯‘𝐷) ∈ ℂ)
30	29	mulridd 11276	. . . . 5 ⊢ (𝜑 → ((♯‘𝐷) · 1) = (♯‘𝐷))
31	26, 30	eqtrd 2775	. . . 4 ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 1 = (♯‘𝐷))
32	31	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 1 = (♯‘𝐷))
33	20, 32	eqtrd 2775	. 2 ⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = (♯‘𝐷))
34		df-ne 2939	. . 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 27326	. . . 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 27301	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐵⟶ℂ)
45	39	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝐴 ∈ 𝐵)
46	45	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝐵)
47	44, 46	ffvelcdmd 7105	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → (𝑥‘𝐴) ∈ ℂ)
48	42, 47	fsumcl 15766	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) ∈ ℂ)
49		0cnd 11252	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 0 ∈ ℂ)
50		simprl 771	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝑦 ∈ 𝐷)
51	4, 5, 6, 35, 50	dchrf 27301	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝑦:𝐵⟶ℂ)
52	51, 45	ffvelcdmd 7105	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (𝑦‘𝐴) ∈ ℂ)
53		subcl 11505	. . . . . 6 ⊢ (((𝑦‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑦‘𝐴) − 1) ∈ ℂ)
54	52, 24, 53	sylancl 586	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) − 1) ∈ ℂ)
55		simprr 773	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (𝑦‘𝐴) ≠ 1)
56		subeq0 11533	. . . . . . . 8 ⊢ (((𝑦‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑦‘𝐴) − 1) = 0 ↔ (𝑦‘𝐴) = 1))
57	52, 24, 56	sylancl 586	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) = 0 ↔ (𝑦‘𝐴) = 1))
58	57	necon3bid 2983	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) ≠ 0 ↔ (𝑦‘𝐴) ≠ 1))
59	55, 58	mpbird 257	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) − 1) ≠ 0)
60		oveq2 7439	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑦(+_g‘𝐺)𝑧) = (𝑦(+_g‘𝐺)𝑥))
61	60	fveq1d 6909	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → ((𝑦(+_g‘𝐺)𝑧)‘𝐴) = ((𝑦(+_g‘𝐺)𝑥)‘𝐴))
62	61	cbvsumv 15729	. . . . . . . . . 10 ⊢ Σ𝑧 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑧)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑥)‘𝐴)
63		eqid 2735	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
64	50	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦 ∈ 𝐷)
65	4, 5, 6, 63, 64, 43	dchrmul 27307	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → (𝑦(+_g‘𝐺)𝑥) = (𝑦 ∘_f · 𝑥))
66	65	fveq1d 6909	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → ((𝑦(+_g‘𝐺)𝑥)‘𝐴) = ((𝑦 ∘_f · 𝑥)‘𝐴))
67	51	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦:𝐵⟶ℂ)
68	67	ffnd 6738	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦 Fn 𝐵)
69	44	ffnd 6738	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑥 Fn 𝐵)
70	35	fvexi 6921	. . . . . . . . . . . . . 14 ⊢ 𝐵 ∈ V
71	70	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ V)
72		fnfvof 7714	. . . . . . . . . . . . 13 ⊢ (((𝑦 Fn 𝐵 ∧ 𝑥 Fn 𝐵) ∧ (𝐵 ∈ V ∧ 𝐴 ∈ 𝐵)) → ((𝑦 ∘_f · 𝑥)‘𝐴) = ((𝑦‘𝐴) · (𝑥‘𝐴)))
73	68, 69, 71, 46, 72	syl22anc 839	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → ((𝑦 ∘_f · 𝑥)‘𝐴) = ((𝑦‘𝐴) · (𝑥‘𝐴)))
74	66, 73	eqtrd 2775	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → ((𝑦(+_g‘𝐺)𝑥)‘𝐴) = ((𝑦‘𝐴) · (𝑥‘𝐴)))
75	74	sumeq2dv 15735	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑥)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴)))
76	62, 75	eqtrid 2787	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑧 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑧)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴)))
77		fveq1 6906	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦(+_g‘𝐺)𝑧) → (𝑥‘𝐴) = ((𝑦(+_g‘𝐺)𝑧)‘𝐴))
78	4	dchrabl 27313	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
79		ablgrp 19818	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
80	41, 78, 79	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝐺 ∈ Grp)
81		eqid 2735	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏))) = (𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))
82	81, 6, 63	grplactf1o 19075	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐷) → ((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦):𝐷–1-1-onto→𝐷)
83	80, 50, 82	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦):𝐷–1-1-onto→𝐷)
84	81, 6	grplactval 19073	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦)‘𝑧) = (𝑦(+_g‘𝐺)𝑧))
85	50, 84	sylan 580	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑧 ∈ 𝐷) → (((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+_g‘𝐺)𝑏)))‘𝑦)‘𝑧) = (𝑦(+_g‘𝐺)𝑧))
86	77, 42, 83, 85, 47	fsumf1o 15756	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = Σ𝑧 ∈ 𝐷 ((𝑦(+_g‘𝐺)𝑧)‘𝐴))
87	42, 52, 47	fsummulc2 15817	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴)))
88	76, 86, 87	3eqtr4rd 2786	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))
89	48	mullidd 11277	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))
90	88, 89	oveq12d 7449	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))) = (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) − Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)))
91	48	subidd 11606	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) − Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = 0)
92	90, 91	eqtrd 2775	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))) = 0)
93	24	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 1 ∈ ℂ)
94	52, 93, 48	subdird 11718	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))))
95	54	mul01d 11458	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · 0) = 0)
96	92, 94, 95	3eqtr4d 2785	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = (((𝑦‘𝐴) − 1) · 0))
97	48, 49, 54, 59, 96	mulcanad 11896	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0)
98	40, 97	rexlimddv 3159	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0)
99	34, 98	sylan2br 595	. 2 ⊢ ((𝜑 ∧ ¬ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0)
100	1, 2, 33, 99	ifbothda 4569	1 ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 Vcvv 3478 ifcif 4531 ↦ cmpt 5231 Fn wfn 6558 ⟶wf 6559 –1-1-onto→wf1o 6562 ‘cfv 6563 (class class class)co 7431 ∘_f cof 7695 Fincfn 8984 ℂcc 11151 0cc0 11153 1c1 11154 · cmul 11158 − cmin 11490 ℕcn 12264 ℕ₀cn0 12524 ♯chash 14366 Σcsu 15719 Basecbs 17245 +_gcplusg 17298 MndHom cmhm 18807 Grpcgrp 18964 Abelcabl 19814 mulGrpcmgp 20152 1_rcur 20199 ℂ_fldccnfld 21382 ℤ/nℤczn 21531 DChrcdchr 27291

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-inf2 9679 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231 ax-addf 11232 ax-mulf 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-tp 4636 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-iin 4999 df-disj 5116 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-se 5642 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-isom 6572 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-rpss 7742 df-om 7888 df-1st 8013 df-2nd 8014 df-supp 8185 df-tpos 8250 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-2o 8506 df-oadd 8509 df-omul 8510 df-er 8744 df-ec 8746 df-qs 8750 df-map 8867 df-pm 8868 df-ixp 8937 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-fsupp 9400 df-fi 9449 df-sup 9480 df-inf 9481 df-oi 9548 df-dju 9939 df-card 9977 df-acn 9980 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12525 df-xnn0 12598 df-z 12612 df-dec 12732 df-uz 12877 df-q 12989 df-rp 13033 df-xneg 13152 df-xadd 13153 df-xmul 13154 df-ioo 13388 df-ioc 13389 df-ico 13390 df-icc 13391 df-fz 13545 df-fzo 13692 df-fl 13829 df-mod 13907 df-seq 14040 df-exp 14100 df-fac 14310 df-bc 14339 df-hash 14367 df-word 14550 df-concat 14606 df-s1 14631 df-shft 15103 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272 df-limsup 15504 df-clim 15521 df-rlim 15522 df-sum 15720 df-ef 16100 df-sin 16102 df-cos 16103 df-pi 16105 df-dvds 16288 df-gcd 16529 df-prm 16706 df-phi 16800 df-pc 16871 df-struct 17181 df-sets 17198 df-slot 17216 df-ndx 17228 df-base 17246 df-ress 17275 df-plusg 17311 df-mulr 17312 df-starv 17313 df-sca 17314 df-vsca 17315 df-ip 17316 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-hom 17322 df-cco 17323 df-rest 17469 df-topn 17470 df-0g 17488 df-gsum 17489 df-topgen 17490 df-pt 17491 df-prds 17494 df-xrs 17549 df-qtop 17554 df-imas 17555 df-qus 17556 df-xps 17557 df-mre 17631 df-mrc 17632 df-acs 17634 df-mgm 18666 df-sgrp 18745 df-mnd 18761 df-mhm 18809 df-submnd 18810 df-grp 18967 df-minusg 18968 df-sbg 18969 df-mulg 19099 df-subg 19154 df-nsg 19155 df-eqg 19156 df-ghm 19244 df-gim 19290 df-ga 19321 df-cntz 19348 df-oppg 19377 df-od 19561 df-gex 19562 df-pgp 19563 df-lsm 19669 df-pj1 19670 df-cmn 19815 df-abl 19816 df-cyg 19911 df-dprd 20030 df-dpj 20031 df-mgp 20153 df-rng 20171 df-ur 20200 df-ring 20253 df-cring 20254 df-oppr 20351 df-dvdsr 20374 df-unit 20375 df-invr 20405 df-rhm 20489 df-subrng 20563 df-subrg 20587 df-lmod 20877 df-lss 20948 df-lsp 20988 df-sra 21190 df-rgmod 21191 df-lidl 21236 df-rsp 21237 df-2idl 21278 df-psmet 21374 df-xmet 21375 df-met 21376 df-bl 21377 df-mopn 21378 df-fbas 21379 df-fg 21380 df-cnfld 21383 df-zring 21476 df-zrh 21532 df-zn 21535 df-top 22916 df-topon 22933 df-topsp 22955 df-bases 22969 df-cld 23043 df-ntr 23044 df-cls 23045 df-nei 23122 df-lp 23160 df-perf 23161 df-cn 23251 df-cnp 23252 df-haus 23339 df-tx 23586 df-hmeo 23779 df-fil 23870 df-fm 23962 df-flim 23963 df-flf 23964 df-xms 24346 df-ms 24347 df-tms 24348 df-cncf 24918 df-0p 25719 df-limc 25916 df-dv 25917 df-ply 26242 df-idp 26243 df-coe 26244 df-dgr 26245 df-quot 26348 df-log 26613 df-cxp 26614 df-dchr 27292

This theorem is referenced by: dchrhash 27330 sumdchr 27331

W3C validator