Theorem sumdchr2

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

	Ref	Expression
Hypotheses	sumdchr.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	sumdchr.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	sumdchr2.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	sumdchr2.1	⊢ 1 = ( 1r ‘ 𝑍 )
	sumdchr2.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
	sumdchr2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	sumdchr2.x	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion	sumdchr2	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = if ( 𝐴 = 1 , ( ♯ ‘ 𝐷 ) , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		sumdchr.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		sumdchr.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
3		sumdchr2.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
4		sumdchr2.1	⊢ 1 = ( 1r ‘ 𝑍 )
5		sumdchr2.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
6		sumdchr2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7		sumdchr2.x	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
8		eqeq2	⊢ ( ( ♯ ‘ 𝐷 ) = if ( 𝐴 = 1 , ( ♯ ‘ 𝐷 ) , 0 ) → ( Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ↔ Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = if ( 𝐴 = 1 , ( ♯ ‘ 𝐷 ) , 0 ) ) )
9		eqeq2	⊢ ( 0 = if ( 𝐴 = 1 , ( ♯ ‘ 𝐷 ) , 0 ) → ( Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = 0 ↔ Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = if ( 𝐴 = 1 , ( ♯ ‘ 𝐷 ) , 0 ) ) )
10		fveq2	⊢ ( 𝐴 = 1 → ( 𝑥 ‘ 𝐴 ) = ( 𝑥 ‘ 1 ) )
11	1 3 2	dchrmhm	⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
13	11 12	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
14		eqid	⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
15	14 4	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑍 ) )
16		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
17		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
18	16 17	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
19	15 18	mhm0	⊢ ( 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑥 ‘ 1 ) = 1 )
20	13 19	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ 1 ) = 1 )
21	10 20	sylan9eqr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 = 1 ) → ( 𝑥 ‘ 𝐴 ) = 1 )
22	21	an32s	⊢ ( ( ( 𝜑 ∧ 𝐴 = 1 ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ 𝐴 ) = 1 )
23	22	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝐴 = 1 ) → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = Σ 𝑥 ∈ 𝐷 1 )
24	1 2	dchrfi	⊢ ( 𝑁 ∈ ℕ → 𝐷 ∈ Fin )
25	6 24	syl	⊢ ( 𝜑 → 𝐷 ∈ Fin )
26		ax-1cn	⊢ 1 ∈ ℂ
27		fsumconst	⊢ ( ( 𝐷 ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑥 ∈ 𝐷 1 = ( ( ♯ ‘ 𝐷 ) · 1 ) )
28	25 26 27	sylancl	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 1 = ( ( ♯ ‘ 𝐷 ) · 1 ) )
29		hashcl	⊢ ( 𝐷 ∈ Fin → ( ♯ ‘ 𝐷 ) ∈ ℕ0 )
30	6 24 29	3syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐷 ) ∈ ℕ0 )
31	30	nn0cnd	⊢ ( 𝜑 → ( ♯ ‘ 𝐷 ) ∈ ℂ )
32	31	mulridd	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐷 ) · 1 ) = ( ♯ ‘ 𝐷 ) )
33	28 32	eqtrd	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 1 = ( ♯ ‘ 𝐷 ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 1 ) → Σ 𝑥 ∈ 𝐷 1 = ( ♯ ‘ 𝐷 ) )
35	23 34	eqtrd	⊢ ( ( 𝜑 ∧ 𝐴 = 1 ) → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) )
36		df-ne	⊢ ( 𝐴 ≠ 1 ↔ ¬ 𝐴 = 1 )
37	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 1 ) → 𝑁 ∈ ℕ )
38		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 1 ) → 𝐴 ≠ 1 )
39	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 1 ) → 𝐴 ∈ 𝐵 )
40	1 3 2 5 4 37 38 39	dchrpt	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 1 ) → ∃ 𝑦 ∈ 𝐷 ( 𝑦 ‘ 𝐴 ) ≠ 1 )
41	37	adantr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → 𝑁 ∈ ℕ )
42	41 24	syl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → 𝐷 ∈ Fin )
43		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
44	1 3 2 5 43	dchrf	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 : 𝐵 ⟶ ℂ )
45	39	adantr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → 𝐴 ∈ 𝐵 )
46	45	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝐵 )
47	44 46	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ 𝐴 ) ∈ ℂ )
48	42 47	fsumcl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ∈ ℂ )
49		0cnd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → 0 ∈ ℂ )
50		simprl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → 𝑦 ∈ 𝐷 )
51	1 3 2 5 50	dchrf	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → 𝑦 : 𝐵 ⟶ ℂ )
52	51 45	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( 𝑦 ‘ 𝐴 ) ∈ ℂ )
53		subcl	⊢ ( ( ( 𝑦 ‘ 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑦 ‘ 𝐴 ) − 1 ) ∈ ℂ )
54	52 26 53	sylancl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( 𝑦 ‘ 𝐴 ) − 1 ) ∈ ℂ )
55		simprr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( 𝑦 ‘ 𝐴 ) ≠ 1 )
56		subeq0	⊢ ( ( ( 𝑦 ‘ 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝑦 ‘ 𝐴 ) − 1 ) = 0 ↔ ( 𝑦 ‘ 𝐴 ) = 1 ) )
57	52 26 56	sylancl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( ( 𝑦 ‘ 𝐴 ) − 1 ) = 0 ↔ ( 𝑦 ‘ 𝐴 ) = 1 ) )
58	57	necon3bid	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( ( 𝑦 ‘ 𝐴 ) − 1 ) ≠ 0 ↔ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) )
59	55 58	mpbird	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( 𝑦 ‘ 𝐴 ) − 1 ) ≠ 0 )
60		oveq2	⊢ ( 𝑧 = 𝑥 → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
61	60	fveq1d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ‘ 𝐴 ) = ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ‘ 𝐴 ) )
62	61	cbvsumv	⊢ Σ 𝑧 ∈ 𝐷 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ‘ 𝐴 ) = Σ 𝑥 ∈ 𝐷 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ‘ 𝐴 )
63		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
64	50	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 )
65	1 3 2 63 64 43	dchrmul	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑦 ∘f · 𝑥 ) )
66	65	fveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ‘ 𝐴 ) = ( ( 𝑦 ∘f · 𝑥 ) ‘ 𝐴 ) )
67	51	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑦 : 𝐵 ⟶ ℂ )
68	67	ffnd	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑦 Fn 𝐵 )
69	44	ffnd	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 Fn 𝐵 )
70	5	fvexi	⊢ 𝐵 ∈ V
71	70	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ V )
72		fnfvof	⊢ ( ( ( 𝑦 Fn 𝐵 ∧ 𝑥 Fn 𝐵 ) ∧ ( 𝐵 ∈ V ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 𝑦 ∘f · 𝑥 ) ‘ 𝐴 ) = ( ( 𝑦 ‘ 𝐴 ) · ( 𝑥 ‘ 𝐴 ) ) )
73	68 69 71 46 72	syl22anc	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑦 ∘f · 𝑥 ) ‘ 𝐴 ) = ( ( 𝑦 ‘ 𝐴 ) · ( 𝑥 ‘ 𝐴 ) ) )
74	66 73	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ‘ 𝐴 ) = ( ( 𝑦 ‘ 𝐴 ) · ( 𝑥 ‘ 𝐴 ) ) )
75	74	sumeq2dv	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → Σ 𝑥 ∈ 𝐷 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ‘ 𝐴 ) = Σ 𝑥 ∈ 𝐷 ( ( 𝑦 ‘ 𝐴 ) · ( 𝑥 ‘ 𝐴 ) ) )
76	62 75	eqtrid	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → Σ 𝑧 ∈ 𝐷 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ‘ 𝐴 ) = Σ 𝑥 ∈ 𝐷 ( ( 𝑦 ‘ 𝐴 ) · ( 𝑥 ‘ 𝐴 ) ) )
77		fveq1	⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ( 𝑥 ‘ 𝐴 ) = ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ‘ 𝐴 ) )
78	1	dchrabl	⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )
79		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
80	41 78 79	3syl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → 𝐺 ∈ Grp )
81		eqid	⊢ ( 𝑎 ∈ 𝐷 ↦ ( 𝑏 ∈ 𝐷 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) ) = ( 𝑎 ∈ 𝐷 ↦ ( 𝑏 ∈ 𝐷 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) )
82	81 2 63	grplactf1o	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑎 ∈ 𝐷 ↦ ( 𝑏 ∈ 𝐷 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) ) ‘ 𝑦 ) : 𝐷 –1-1-onto→ 𝐷 )
83	80 50 82	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( 𝑎 ∈ 𝐷 ↦ ( 𝑏 ∈ 𝐷 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) ) ‘ 𝑦 ) : 𝐷 –1-1-onto→ 𝐷 )
84	81 2	grplactval	⊢ ( ( 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) → ( ( ( 𝑎 ∈ 𝐷 ↦ ( 𝑏 ∈ 𝐷 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) ) ‘ 𝑦 ) ‘ 𝑧 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) )
85	50 84	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) ∧ 𝑧 ∈ 𝐷 ) → ( ( ( 𝑎 ∈ 𝐷 ↦ ( 𝑏 ∈ 𝐷 ↦ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) ) ‘ 𝑦 ) ‘ 𝑧 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) )
86	77 42 83 85 47	fsumf1o	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = Σ 𝑧 ∈ 𝐷 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ‘ 𝐴 ) )
87	42 52 47	fsummulc2	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( 𝑦 ‘ 𝐴 ) · Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) = Σ 𝑥 ∈ 𝐷 ( ( 𝑦 ‘ 𝐴 ) · ( 𝑥 ‘ 𝐴 ) ) )
88	76 86 87	3eqtr4rd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( 𝑦 ‘ 𝐴 ) · Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) = Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) )
89	48	mullidd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( 1 · Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) = Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) )
90	88 89	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( ( 𝑦 ‘ 𝐴 ) · Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) − ( 1 · Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) ) = ( Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) − Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) )
91	48	subidd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) − Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) = 0 )
92	90 91	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( ( 𝑦 ‘ 𝐴 ) · Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) − ( 1 · Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) ) = 0 )
93	26	a1i	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → 1 ∈ ℂ )
94	52 93 48	subdird	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( ( 𝑦 ‘ 𝐴 ) − 1 ) · Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) = ( ( ( 𝑦 ‘ 𝐴 ) · Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) − ( 1 · Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) ) )
95	54	mul01d	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( ( 𝑦 ‘ 𝐴 ) − 1 ) · 0 ) = 0 )
96	92 94 95	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → ( ( ( 𝑦 ‘ 𝐴 ) − 1 ) · Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ) = ( ( ( 𝑦 ‘ 𝐴 ) − 1 ) · 0 ) )
97	48 49 54 59 96	mulcanad	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 1 ) ∧ ( 𝑦 ∈ 𝐷 ∧ ( 𝑦 ‘ 𝐴 ) ≠ 1 ) ) → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = 0 )
98	40 97	rexlimddv	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 1 ) → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = 0 )
99	36 98	sylan2br	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 1 ) → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = 0 )
100	8 9 35 99	ifbothda	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) = if ( 𝐴 = 1 , ( ♯ ‘ 𝐷 ) , 0 ) )