| Step | Hyp | Ref
| Expression |
| 1 | | eqeq2 2749 |
. 2
⊢
((♯‘𝐷) =
if(𝐴 = 1 , (♯‘𝐷), 0) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = (♯‘𝐷) ↔ Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0))) |
| 2 | | eqeq2 2749 |
. 2
⊢ (0 =
if(𝐴 = 1 , (♯‘𝐷), 0) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0 ↔ Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0))) |
| 3 | | fveq2 6906 |
. . . . . 6
⊢ (𝐴 = 1 → (𝑥‘𝐴) = (𝑥‘ 1 )) |
| 4 | | sumdchr.g |
. . . . . . . . 9
⊢ 𝐺 = (DChr‘𝑁) |
| 5 | | sumdchr2.z |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
| 6 | | sumdchr.d |
. . . . . . . . 9
⊢ 𝐷 = (Base‘𝐺) |
| 7 | 4, 5, 6 | dchrmhm 27285 |
. . . . . . . 8
⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) |
| 8 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷) |
| 9 | 7, 8 | sselid 3981 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
| 10 | | eqid 2737 |
. . . . . . . . 9
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
| 11 | | sumdchr2.1 |
. . . . . . . . 9
⊢ 1 =
(1r‘𝑍) |
| 12 | 10, 11 | ringidval 20180 |
. . . . . . . 8
⊢ 1 =
(0g‘(mulGrp‘𝑍)) |
| 13 | | eqid 2737 |
. . . . . . . . 9
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
| 14 | | cnfld1 21406 |
. . . . . . . . 9
⊢ 1 =
(1r‘ℂfld) |
| 15 | 13, 14 | ringidval 20180 |
. . . . . . . 8
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
| 16 | 12, 15 | mhm0 18807 |
. . . . . . 7
⊢ (𝑥 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) → (𝑥‘ 1 ) = 1) |
| 17 | 9, 16 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥‘ 1 ) = 1) |
| 18 | 3, 17 | sylan9eqr 2799 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝐴 = 1 ) → (𝑥‘𝐴) = 1) |
| 19 | 18 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 = 1 ) ∧ 𝑥 ∈ 𝐷) → (𝑥‘𝐴) = 1) |
| 20 | 19 | sumeq2dv 15738 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = Σ𝑥 ∈ 𝐷 1) |
| 21 | | sumdchr2.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 22 | 4, 6 | dchrfi 27299 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) |
| 23 | 21, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ Fin) |
| 24 | | ax-1cn 11213 |
. . . . . 6
⊢ 1 ∈
ℂ |
| 25 | | fsumconst 15826 |
. . . . . 6
⊢ ((𝐷 ∈ Fin ∧ 1 ∈
ℂ) → Σ𝑥
∈ 𝐷 1 =
((♯‘𝐷) ·
1)) |
| 26 | 23, 24, 25 | sylancl 586 |
. . . . 5
⊢ (𝜑 → Σ𝑥 ∈ 𝐷 1 = ((♯‘𝐷) · 1)) |
| 27 | | hashcl 14395 |
. . . . . . . 8
⊢ (𝐷 ∈ Fin →
(♯‘𝐷) ∈
ℕ0) |
| 28 | 21, 22, 27 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐷) ∈
ℕ0) |
| 29 | 28 | nn0cnd 12589 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐷) ∈
ℂ) |
| 30 | 29 | mulridd 11278 |
. . . . 5
⊢ (𝜑 → ((♯‘𝐷) · 1) =
(♯‘𝐷)) |
| 31 | 26, 30 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → Σ𝑥 ∈ 𝐷 1 = (♯‘𝐷)) |
| 32 | 31 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 1 = (♯‘𝐷)) |
| 33 | 20, 32 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = (♯‘𝐷)) |
| 34 | | df-ne 2941 |
. . 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 27311 |
. . . 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 27286 |
. . . . . . 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 15769 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) ∈ ℂ) |
| 49 | | 0cnd 11254 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 0 ∈
ℂ) |
| 50 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝑦 ∈ 𝐷) |
| 51 | 4, 5, 6, 35, 50 | dchrf 27286 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝑦:𝐵⟶ℂ) |
| 52 | 51, 45 | ffvelcdmd 7105 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (𝑦‘𝐴) ∈ ℂ) |
| 53 | | subcl 11507 |
. . . . . 6
⊢ (((𝑦‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ)
→ ((𝑦‘𝐴) − 1) ∈
ℂ) |
| 54 | 52, 24, 53 | sylancl 586 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) − 1) ∈
ℂ) |
| 55 | | simprr 773 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (𝑦‘𝐴) ≠ 1) |
| 56 | | subeq0 11535 |
. . . . . . . 8
⊢ (((𝑦‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝑦‘𝐴) − 1) = 0 ↔ (𝑦‘𝐴) = 1)) |
| 57 | 52, 24, 56 | sylancl 586 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) = 0 ↔ (𝑦‘𝐴) = 1)) |
| 58 | 57 | necon3bid 2985 |
. . . . . 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 6908 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → ((𝑦(+g‘𝐺)𝑧)‘𝐴) = ((𝑦(+g‘𝐺)𝑥)‘𝐴)) |
| 62 | 61 | cbvsumv 15732 |
. . . . . . . . . 10
⊢
Σ𝑧 ∈
𝐷 ((𝑦(+g‘𝐺)𝑧)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦(+g‘𝐺)𝑥)‘𝐴) |
| 63 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 64 | 50 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦 ∈ 𝐷) |
| 65 | 4, 5, 6, 63, 64, 43 | dchrmul 27292 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → (𝑦(+g‘𝐺)𝑥) = (𝑦 ∘f · 𝑥)) |
| 66 | 65 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → ((𝑦(+g‘𝐺)𝑥)‘𝐴) = ((𝑦 ∘f · 𝑥)‘𝐴)) |
| 67 | 51 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦:𝐵⟶ℂ) |
| 68 | 67 | ffnd 6737 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑦 Fn 𝐵) |
| 69 | 44 | ffnd 6737 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → 𝑥 Fn 𝐵) |
| 70 | 35 | fvexi 6920 |
. . . . . . . . . . . . . 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 2777 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑥 ∈ 𝐷) → ((𝑦(+g‘𝐺)𝑥)‘𝐴) = ((𝑦‘𝐴) · (𝑥‘𝐴))) |
| 75 | 74 | sumeq2dv 15738 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 ((𝑦(+g‘𝐺)𝑥)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴))) |
| 76 | 62, 75 | eqtrid 2789 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑧 ∈ 𝐷 ((𝑦(+g‘𝐺)𝑧)‘𝐴) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴))) |
| 77 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → (𝑥‘𝐴) = ((𝑦(+g‘𝐺)𝑧)‘𝐴)) |
| 78 | 4 | dchrabl 27298 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
| 79 | | ablgrp 19803 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
| 80 | 41, 78, 79 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 𝐺 ∈ Grp) |
| 81 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+g‘𝐺)𝑏))) = (𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+g‘𝐺)𝑏))) |
| 82 | 81, 6, 63 | grplactf1o 19062 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐷) → ((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+g‘𝐺)𝑏)))‘𝑦):𝐷–1-1-onto→𝐷) |
| 83 | 80, 50, 82 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+g‘𝐺)𝑏)))‘𝑦):𝐷–1-1-onto→𝐷) |
| 84 | 81, 6 | grplactval 19060 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+g‘𝐺)𝑏)))‘𝑦)‘𝑧) = (𝑦(+g‘𝐺)𝑧)) |
| 85 | 50, 84 | sylan 580 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) ∧ 𝑧 ∈ 𝐷) → (((𝑎 ∈ 𝐷 ↦ (𝑏 ∈ 𝐷 ↦ (𝑎(+g‘𝐺)𝑏)))‘𝑦)‘𝑧) = (𝑦(+g‘𝐺)𝑧)) |
| 86 | 77, 42, 83, 85, 47 | fsumf1o 15759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = Σ𝑧 ∈ 𝐷 ((𝑦(+g‘𝐺)𝑧)‘𝐴)) |
| 87 | 42, 52, 47 | fsummulc2 15820 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 ((𝑦‘𝐴) · (𝑥‘𝐴))) |
| 88 | 76, 86, 87 | 3eqtr4rd 2788 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → ((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) |
| 89 | 48 | mullidd 11279 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) |
| 90 | 88, 89 | oveq12d 7449 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))) = (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) − Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))) |
| 91 | 48 | subidd 11608 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) − Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = 0) |
| 92 | 90, 91 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴))) = 0) |
| 93 | 24 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → 1 ∈
ℂ) |
| 94 | 52, 93, 48 | subdird 11720 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = (((𝑦‘𝐴) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) − (1 · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)))) |
| 95 | 54 | mul01d 11460 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · 0) =
0) |
| 96 | 92, 94, 95 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → (((𝑦‘𝐴) − 1) · Σ𝑥 ∈ 𝐷 (𝑥‘𝐴)) = (((𝑦‘𝐴) − 1) · 0)) |
| 97 | 48, 49, 54, 59, 96 | mulcanad 11898 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 1 ) ∧ (𝑦 ∈ 𝐷 ∧ (𝑦‘𝐴) ≠ 1)) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0) |
| 98 | 40, 97 | rexlimddv 3161 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0) |
| 99 | 34, 98 | sylan2br 595 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐴 = 1 ) → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = 0) |
| 100 | 1, 2, 33, 99 | ifbothda 4564 |
1
⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0)) |