| 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 | | fveq1 6905 |
. . . . . 6
⊢ (𝑋 = 1 → (𝑋‘𝑎) = ( 1 ‘𝑎)) |
| 4 | | dchrsum.g |
. . . . . . 7
⊢ 𝐺 = (DChr‘𝑁) |
| 5 | | dchrsum.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
| 6 | | dchrsum.1 |
. . . . . . 7
⊢ 1 =
(0g‘𝐺) |
| 7 | | dchrsum2.u |
. . . . . . 7
⊢ 𝑈 = (Unit‘𝑍) |
| 8 | | dchrsum.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
| 9 | | dchrsum.d |
. . . . . . . . . 10
⊢ 𝐷 = (Base‘𝐺) |
| 10 | 4, 9 | dchrrcl 27284 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ) |
| 11 | 8, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑈) → 𝑁 ∈ ℕ) |
| 13 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑈) → 𝑎 ∈ 𝑈) |
| 14 | 4, 5, 6, 7, 12, 13 | dchr1 27301 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑈) → ( 1 ‘𝑎) = 1) |
| 15 | 3, 14 | sylan9eqr 2799 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑈) ∧ 𝑋 = 1 ) → (𝑋‘𝑎) = 1) |
| 16 | 15 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 = 1 ) ∧ 𝑎 ∈ 𝑈) → (𝑋‘𝑎) = 1) |
| 17 | 16 | sumeq2dv 15738 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = 1 ) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = Σ𝑎 ∈ 𝑈 1) |
| 18 | 5, 7 | znunithash 21583 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(♯‘𝑈) =
(ϕ‘𝑁)) |
| 19 | 11, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝑈) = (ϕ‘𝑁)) |
| 20 | 11 | phicld 16809 |
. . . . . . . . 9
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ) |
| 21 | 20 | nnnn0d 12587 |
. . . . . . . 8
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ0) |
| 22 | 19, 21 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑈) ∈
ℕ0) |
| 23 | 7 | fvexi 6920 |
. . . . . . . 8
⊢ 𝑈 ∈ V |
| 24 | | hashclb 14397 |
. . . . . . . 8
⊢ (𝑈 ∈ V → (𝑈 ∈ Fin ↔
(♯‘𝑈) ∈
ℕ0)) |
| 25 | 23, 24 | ax-mp 5 |
. . . . . . 7
⊢ (𝑈 ∈ Fin ↔
(♯‘𝑈) ∈
ℕ0) |
| 26 | 22, 25 | sylibr 234 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ Fin) |
| 27 | | ax-1cn 11213 |
. . . . . 6
⊢ 1 ∈
ℂ |
| 28 | | fsumconst 15826 |
. . . . . 6
⊢ ((𝑈 ∈ Fin ∧ 1 ∈
ℂ) → Σ𝑎
∈ 𝑈 1 =
((♯‘𝑈) ·
1)) |
| 29 | 26, 27, 28 | sylancl 586 |
. . . . 5
⊢ (𝜑 → Σ𝑎 ∈ 𝑈 1 = ((♯‘𝑈) · 1)) |
| 30 | 19 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → ((♯‘𝑈) · 1) =
((ϕ‘𝑁) ·
1)) |
| 31 | 20 | nncnd 12282 |
. . . . . 6
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℂ) |
| 32 | 31 | mulridd 11278 |
. . . . 5
⊢ (𝜑 → ((ϕ‘𝑁) · 1) =
(ϕ‘𝑁)) |
| 33 | 29, 30, 32 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → Σ𝑎 ∈ 𝑈 1 = (ϕ‘𝑁)) |
| 34 | 33 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = 1 ) → Σ𝑎 ∈ 𝑈 1 = (ϕ‘𝑁)) |
| 35 | 17, 34 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝑋 = 1 ) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = (ϕ‘𝑁)) |
| 36 | 4 | dchrabl 27298 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
| 37 | | ablgrp 19803 |
. . . . . . . 8
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
| 38 | 9, 6 | grpidcl 18983 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp → 1 ∈ 𝐷) |
| 39 | 11, 36, 37, 38 | 4syl 19 |
. . . . . . 7
⊢ (𝜑 → 1 ∈ 𝐷) |
| 40 | 4, 5, 9, 7, 8, 39 | dchreq 27302 |
. . . . . 6
⊢ (𝜑 → (𝑋 = 1 ↔ ∀𝑘 ∈ 𝑈 (𝑋‘𝑘) = ( 1 ‘𝑘))) |
| 41 | 40 | notbid 318 |
. . . . 5
⊢ (𝜑 → (¬ 𝑋 = 1 ↔ ¬ ∀𝑘 ∈ 𝑈 (𝑋‘𝑘) = ( 1 ‘𝑘))) |
| 42 | | rexnal 3100 |
. . . . 5
⊢
(∃𝑘 ∈
𝑈 ¬ (𝑋‘𝑘) = ( 1 ‘𝑘) ↔ ¬ ∀𝑘 ∈ 𝑈 (𝑋‘𝑘) = ( 1 ‘𝑘)) |
| 43 | 41, 42 | bitr4di 289 |
. . . 4
⊢ (𝜑 → (¬ 𝑋 = 1 ↔ ∃𝑘 ∈ 𝑈 ¬ (𝑋‘𝑘) = ( 1 ‘𝑘))) |
| 44 | | df-ne 2941 |
. . . . . 6
⊢ ((𝑋‘𝑘) ≠ ( 1 ‘𝑘) ↔ ¬ (𝑋‘𝑘) = ( 1 ‘𝑘)) |
| 45 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑁 ∈ ℕ) |
| 46 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑈) |
| 47 | 4, 5, 6, 7, 45, 46 | dchr1 27301 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → ( 1 ‘𝑘) = 1) |
| 48 | 47 | neeq2d 3001 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → ((𝑋‘𝑘) ≠ ( 1 ‘𝑘) ↔ (𝑋‘𝑘) ≠ 1)) |
| 49 | 26 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 𝑈 ∈ Fin) |
| 50 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑍) =
(Base‘𝑍) |
| 51 | 4, 5, 9, 50, 8 | dchrf 27286 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℂ) |
| 52 | 50, 7 | unitss 20376 |
. . . . . . . . . . . . 13
⊢ 𝑈 ⊆ (Base‘𝑍) |
| 53 | 52 | sseli 3979 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝑈 → 𝑎 ∈ (Base‘𝑍)) |
| 54 | | ffvelcdm 7101 |
. . . . . . . . . . . 12
⊢ ((𝑋:(Base‘𝑍)⟶ℂ ∧ 𝑎 ∈ (Base‘𝑍)) → (𝑋‘𝑎) ∈ ℂ) |
| 55 | 51, 53, 54 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑈) → (𝑋‘𝑎) ∈ ℂ) |
| 56 | 55 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑎 ∈ 𝑈) → (𝑋‘𝑎) ∈ ℂ) |
| 57 | 49, 56 | fsumcl 15769 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) ∈ ℂ) |
| 58 | | 0cnd 11254 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 0 ∈
ℂ) |
| 59 | 51 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 𝑋:(Base‘𝑍)⟶ℂ) |
| 60 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 𝑘 ∈ 𝑈) |
| 61 | 52, 60 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 𝑘 ∈ (Base‘𝑍)) |
| 62 | 59, 61 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (𝑋‘𝑘) ∈ ℂ) |
| 63 | | subcl 11507 |
. . . . . . . . . 10
⊢ (((𝑋‘𝑘) ∈ ℂ ∧ 1 ∈ ℂ)
→ ((𝑋‘𝑘) − 1) ∈
ℂ) |
| 64 | 62, 27, 63 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → ((𝑋‘𝑘) − 1) ∈ ℂ) |
| 65 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (𝑋‘𝑘) ≠ 1) |
| 66 | | subeq0 11535 |
. . . . . . . . . . . 12
⊢ (((𝑋‘𝑘) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝑋‘𝑘) − 1) = 0 ↔ (𝑋‘𝑘) = 1)) |
| 67 | 62, 27, 66 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) − 1) = 0 ↔ (𝑋‘𝑘) = 1)) |
| 68 | 67 | necon3bid 2985 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) − 1) ≠ 0 ↔ (𝑋‘𝑘) ≠ 1)) |
| 69 | 65, 68 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → ((𝑋‘𝑘) − 1) ≠ 0) |
| 70 | | oveq2 7439 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (𝑘(.r‘𝑍)𝑥) = (𝑘(.r‘𝑍)𝑎)) |
| 71 | 70 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (𝑋‘(𝑘(.r‘𝑍)𝑥)) = (𝑋‘(𝑘(.r‘𝑍)𝑎))) |
| 72 | 71 | cbvsumv 15732 |
. . . . . . . . . . . . . 14
⊢
Σ𝑥 ∈
𝑈 (𝑋‘(𝑘(.r‘𝑍)𝑥)) = Σ𝑎 ∈ 𝑈 (𝑋‘(𝑘(.r‘𝑍)𝑎)) |
| 73 | 4, 5, 9 | dchrmhm 27285 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) |
| 74 | 73, 8 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
| 75 | 74 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑎 ∈ 𝑈) → 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
| 76 | 61 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑎 ∈ 𝑈) → 𝑘 ∈ (Base‘𝑍)) |
| 77 | 53 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑎 ∈ 𝑈) → 𝑎 ∈ (Base‘𝑍)) |
| 78 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
| 79 | 78, 50 | mgpbas 20142 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑍) =
(Base‘(mulGrp‘𝑍)) |
| 80 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(.r‘𝑍) = (.r‘𝑍) |
| 81 | 78, 80 | mgpplusg 20141 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑍) = (+g‘(mulGrp‘𝑍)) |
| 82 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
| 83 | | cnfldmul 21372 |
. . . . . . . . . . . . . . . . . 18
⊢ ·
= (.r‘ℂfld) |
| 84 | 82, 83 | mgpplusg 20141 |
. . . . . . . . . . . . . . . . 17
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
| 85 | 79, 81, 84 | mhmlin 18806 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ 𝑘 ∈ (Base‘𝑍) ∧ 𝑎 ∈ (Base‘𝑍)) → (𝑋‘(𝑘(.r‘𝑍)𝑎)) = ((𝑋‘𝑘) · (𝑋‘𝑎))) |
| 86 | 75, 76, 77, 85 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑎 ∈ 𝑈) → (𝑋‘(𝑘(.r‘𝑍)𝑎)) = ((𝑋‘𝑘) · (𝑋‘𝑎))) |
| 87 | 86 | sumeq2dv 15738 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → Σ𝑎 ∈ 𝑈 (𝑋‘(𝑘(.r‘𝑍)𝑎)) = Σ𝑎 ∈ 𝑈 ((𝑋‘𝑘) · (𝑋‘𝑎))) |
| 88 | 72, 87 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → Σ𝑥 ∈ 𝑈 (𝑋‘(𝑘(.r‘𝑍)𝑥)) = Σ𝑎 ∈ 𝑈 ((𝑋‘𝑘) · (𝑋‘𝑎))) |
| 89 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑘(.r‘𝑍)𝑥) → (𝑋‘𝑎) = (𝑋‘(𝑘(.r‘𝑍)𝑥))) |
| 90 | 11 | nnnn0d 12587 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 91 | 5 | zncrng 21563 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
| 92 | | crngring 20242 |
. . . . . . . . . . . . . . . 16
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
| 93 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
((mulGrp‘𝑍)
↾s 𝑈) =
((mulGrp‘𝑍)
↾s 𝑈) |
| 94 | 7, 93 | unitgrp 20383 |
. . . . . . . . . . . . . . . 16
⊢ (𝑍 ∈ Ring →
((mulGrp‘𝑍)
↾s 𝑈)
∈ Grp) |
| 95 | 90, 91, 92, 94 | 4syl 19 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((mulGrp‘𝑍) ↾s 𝑈) ∈ Grp) |
| 96 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐))) = (𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐))) |
| 97 | 7, 93 | unitgrpbas 20382 |
. . . . . . . . . . . . . . . 16
⊢ 𝑈 =
(Base‘((mulGrp‘𝑍) ↾s 𝑈)) |
| 98 | 93, 81 | ressplusg 17334 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ V →
(.r‘𝑍) =
(+g‘((mulGrp‘𝑍) ↾s 𝑈))) |
| 99 | 23, 98 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(.r‘𝑍) =
(+g‘((mulGrp‘𝑍) ↾s 𝑈)) |
| 100 | 96, 97, 99 | grplactf1o 19062 |
. . . . . . . . . . . . . . 15
⊢
((((mulGrp‘𝑍)
↾s 𝑈)
∈ Grp ∧ 𝑘 ∈
𝑈) → ((𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐)))‘𝑘):𝑈–1-1-onto→𝑈) |
| 101 | 95, 60, 100 | syl2an2r 685 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → ((𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐)))‘𝑘):𝑈–1-1-onto→𝑈) |
| 102 | 96, 97 | grplactval 19060 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) → (((𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐)))‘𝑘)‘𝑥) = (𝑘(.r‘𝑍)𝑥)) |
| 103 | 60, 102 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑥 ∈ 𝑈) → (((𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐)))‘𝑘)‘𝑥) = (𝑘(.r‘𝑍)𝑥)) |
| 104 | 89, 49, 101, 103, 56 | fsumf1o 15759 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = Σ𝑥 ∈ 𝑈 (𝑋‘(𝑘(.r‘𝑍)𝑥))) |
| 105 | 49, 62, 56 | fsummulc2 15820 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → ((𝑋‘𝑘) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = Σ𝑎 ∈ 𝑈 ((𝑋‘𝑘) · (𝑋‘𝑎))) |
| 106 | 88, 104, 105 | 3eqtr4rd 2788 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → ((𝑋‘𝑘) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) |
| 107 | 57 | mullidd 11279 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (1 · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) |
| 108 | 106, 107 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) − (1 · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎))) = (Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) − Σ𝑎 ∈ 𝑈 (𝑋‘𝑎))) |
| 109 | 57 | subidd 11608 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) − Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = 0) |
| 110 | 108, 109 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) − (1 · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎))) = 0) |
| 111 | | 1cnd 11256 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 1 ∈
ℂ) |
| 112 | 62, 111, 57 | subdird 11720 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) − 1) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = (((𝑋‘𝑘) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) − (1 · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)))) |
| 113 | 64 | mul01d 11460 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) − 1) · 0) =
0) |
| 114 | 110, 112,
113 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) − 1) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = (((𝑋‘𝑘) − 1) · 0)) |
| 115 | 57, 58, 64, 69, 114 | mulcanad 11898 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0) |
| 116 | 115 | expr 456 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → ((𝑋‘𝑘) ≠ 1 → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0)) |
| 117 | 48, 116 | sylbid 240 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → ((𝑋‘𝑘) ≠ ( 1 ‘𝑘) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0)) |
| 118 | 44, 117 | biimtrrid 243 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (¬ (𝑋‘𝑘) = ( 1 ‘𝑘) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0)) |
| 119 | 118 | rexlimdva 3155 |
. . . 4
⊢ (𝜑 → (∃𝑘 ∈ 𝑈 ¬ (𝑋‘𝑘) = ( 1 ‘𝑘) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0)) |
| 120 | 43, 119 | sylbid 240 |
. . 3
⊢ (𝜑 → (¬ 𝑋 = 1 → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0)) |
| 121 | 120 | imp 406 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = 1 ) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0) |
| 122 | 1, 2, 35, 121 | ifbothda 4564 |
1
⊢ (𝜑 → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = if(𝑋 = 1 , (ϕ‘𝑁), 0)) |