Metamath Proof Explorer

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 mulid1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐷 ) · 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 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 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 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 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 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 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 mulid2d ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 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 ) )