Step | Hyp | Ref
| Expression |
1 | | eqeq2 2621 |
. 2
⊢
((ϕ‘𝑁) =
if(𝑋 = 1 , (ϕ‘𝑁), 0) → (Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = (ϕ‘𝑁) ↔ Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = if(𝑋 = 1 , (ϕ‘𝑁), 0))) |
2 | | eqeq2 2621 |
. 2
⊢ (0 =
if(𝑋 = 1 , (ϕ‘𝑁), 0) → (Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0 ↔ Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = if(𝑋 = 1 , (ϕ‘𝑁), 0))) |
3 | | fveq1 6102 |
. . . . . 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 24765 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ) |
11 | 8, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑈) → 𝑁 ∈ ℕ) |
13 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑈) → 𝑎 ∈ 𝑈) |
14 | 4, 5, 6, 7, 12, 13 | dchr1 24782 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑈) → ( 1 ‘𝑎) = 1) |
15 | 3, 14 | sylan9eqr 2666 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑈) ∧ 𝑋 = 1 ) → (𝑋‘𝑎) = 1) |
16 | 15 | an32s 842 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 = 1 ) ∧ 𝑎 ∈ 𝑈) → (𝑋‘𝑎) = 1) |
17 | 16 | sumeq2dv 14281 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = 1 ) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = Σ𝑎 ∈ 𝑈 1) |
18 | 5, 7 | znunithash 19732 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(#‘𝑈) =
(ϕ‘𝑁)) |
19 | 11, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝑈) = (ϕ‘𝑁)) |
20 | 11 | phicld 15315 |
. . . . . . . . 9
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ) |
21 | 20 | nnnn0d 11228 |
. . . . . . . 8
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ0) |
22 | 19, 21 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝜑 → (#‘𝑈) ∈
ℕ0) |
23 | | fvex 6113 |
. . . . . . . . 9
⊢
(Unit‘𝑍)
∈ V |
24 | 7, 23 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑈 ∈ V |
25 | | hashclb 13011 |
. . . . . . . 8
⊢ (𝑈 ∈ V → (𝑈 ∈ Fin ↔
(#‘𝑈) ∈
ℕ0)) |
26 | 24, 25 | ax-mp 5 |
. . . . . . 7
⊢ (𝑈 ∈ Fin ↔
(#‘𝑈) ∈
ℕ0) |
27 | 22, 26 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ Fin) |
28 | | ax-1cn 9873 |
. . . . . 6
⊢ 1 ∈
ℂ |
29 | | fsumconst 14364 |
. . . . . 6
⊢ ((𝑈 ∈ Fin ∧ 1 ∈
ℂ) → Σ𝑎
∈ 𝑈 1 =
((#‘𝑈) ·
1)) |
30 | 27, 28, 29 | sylancl 693 |
. . . . 5
⊢ (𝜑 → Σ𝑎 ∈ 𝑈 1 = ((#‘𝑈) · 1)) |
31 | 19 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → ((#‘𝑈) · 1) =
((ϕ‘𝑁) ·
1)) |
32 | 20 | nncnd 10913 |
. . . . . 6
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℂ) |
33 | 32 | mulid1d 9936 |
. . . . 5
⊢ (𝜑 → ((ϕ‘𝑁) · 1) =
(ϕ‘𝑁)) |
34 | 30, 31, 33 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → Σ𝑎 ∈ 𝑈 1 = (ϕ‘𝑁)) |
35 | 34 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = 1 ) → Σ𝑎 ∈ 𝑈 1 = (ϕ‘𝑁)) |
36 | 17, 35 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ 𝑋 = 1 ) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = (ϕ‘𝑁)) |
37 | 4 | dchrabl 24779 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
38 | | ablgrp 18021 |
. . . . . . . 8
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
39 | 9, 6 | grpidcl 17273 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp → 1 ∈ 𝐷) |
40 | 11, 37, 38, 39 | 4syl 19 |
. . . . . . 7
⊢ (𝜑 → 1 ∈ 𝐷) |
41 | 4, 5, 9, 7, 8, 40 | dchreq 24783 |
. . . . . 6
⊢ (𝜑 → (𝑋 = 1 ↔ ∀𝑘 ∈ 𝑈 (𝑋‘𝑘) = ( 1 ‘𝑘))) |
42 | 41 | notbid 307 |
. . . . 5
⊢ (𝜑 → (¬ 𝑋 = 1 ↔ ¬ ∀𝑘 ∈ 𝑈 (𝑋‘𝑘) = ( 1 ‘𝑘))) |
43 | | rexnal 2978 |
. . . . 5
⊢
(∃𝑘 ∈
𝑈 ¬ (𝑋‘𝑘) = ( 1 ‘𝑘) ↔ ¬ ∀𝑘 ∈ 𝑈 (𝑋‘𝑘) = ( 1 ‘𝑘)) |
44 | 42, 43 | syl6bbr 277 |
. . . 4
⊢ (𝜑 → (¬ 𝑋 = 1 ↔ ∃𝑘 ∈ 𝑈 ¬ (𝑋‘𝑘) = ( 1 ‘𝑘))) |
45 | | df-ne 2782 |
. . . . . 6
⊢ ((𝑋‘𝑘) ≠ ( 1 ‘𝑘) ↔ ¬ (𝑋‘𝑘) = ( 1 ‘𝑘)) |
46 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑁 ∈ ℕ) |
47 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑈) |
48 | 4, 5, 6, 7, 46, 47 | dchr1 24782 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → ( 1 ‘𝑘) = 1) |
49 | 48 | neeq2d 2842 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → ((𝑋‘𝑘) ≠ ( 1 ‘𝑘) ↔ (𝑋‘𝑘) ≠ 1)) |
50 | 27 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 𝑈 ∈ Fin) |
51 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑍) =
(Base‘𝑍) |
52 | 4, 5, 9, 51, 8 | dchrf 24767 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℂ) |
53 | 51, 7 | unitss 18483 |
. . . . . . . . . . . . 13
⊢ 𝑈 ⊆ (Base‘𝑍) |
54 | 53 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝑈 → 𝑎 ∈ (Base‘𝑍)) |
55 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝑋:(Base‘𝑍)⟶ℂ ∧ 𝑎 ∈ (Base‘𝑍)) → (𝑋‘𝑎) ∈ ℂ) |
56 | 52, 54, 55 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑈) → (𝑋‘𝑎) ∈ ℂ) |
57 | 56 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑎 ∈ 𝑈) → (𝑋‘𝑎) ∈ ℂ) |
58 | 50, 57 | fsumcl 14311 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) ∈ ℂ) |
59 | | 0cnd 9912 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 0 ∈
ℂ) |
60 | 52 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 𝑋:(Base‘𝑍)⟶ℂ) |
61 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 𝑘 ∈ 𝑈) |
62 | 53, 61 | sseldi 3566 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 𝑘 ∈ (Base‘𝑍)) |
63 | 60, 62 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (𝑋‘𝑘) ∈ ℂ) |
64 | | subcl 10159 |
. . . . . . . . . 10
⊢ (((𝑋‘𝑘) ∈ ℂ ∧ 1 ∈ ℂ)
→ ((𝑋‘𝑘) − 1) ∈
ℂ) |
65 | 63, 28, 64 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → ((𝑋‘𝑘) − 1) ∈ ℂ) |
66 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (𝑋‘𝑘) ≠ 1) |
67 | | subeq0 10186 |
. . . . . . . . . . . 12
⊢ (((𝑋‘𝑘) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝑋‘𝑘) − 1) = 0 ↔ (𝑋‘𝑘) = 1)) |
68 | 63, 28, 67 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) − 1) = 0 ↔ (𝑋‘𝑘) = 1)) |
69 | 68 | necon3bid 2826 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) − 1) ≠ 0 ↔ (𝑋‘𝑘) ≠ 1)) |
70 | 66, 69 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → ((𝑋‘𝑘) − 1) ≠ 0) |
71 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (𝑘(.r‘𝑍)𝑥) = (𝑘(.r‘𝑍)𝑎)) |
72 | 71 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (𝑋‘(𝑘(.r‘𝑍)𝑥)) = (𝑋‘(𝑘(.r‘𝑍)𝑎))) |
73 | 72 | cbvsumv 14274 |
. . . . . . . . . . . . . 14
⊢
Σ𝑥 ∈
𝑈 (𝑋‘(𝑘(.r‘𝑍)𝑥)) = Σ𝑎 ∈ 𝑈 (𝑋‘(𝑘(.r‘𝑍)𝑎)) |
74 | 4, 5, 9 | dchrmhm 24766 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) |
75 | 74, 8 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
76 | 75 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑎 ∈ 𝑈) → 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
77 | 62 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑎 ∈ 𝑈) → 𝑘 ∈ (Base‘𝑍)) |
78 | 54 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑎 ∈ 𝑈) → 𝑎 ∈ (Base‘𝑍)) |
79 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
80 | 79, 51 | mgpbas 18318 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑍) =
(Base‘(mulGrp‘𝑍)) |
81 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(.r‘𝑍) = (.r‘𝑍) |
82 | 79, 81 | mgpplusg 18316 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑍) = (+g‘(mulGrp‘𝑍)) |
83 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
84 | | cnfldmul 19573 |
. . . . . . . . . . . . . . . . . 18
⊢ ·
= (.r‘ℂfld) |
85 | 83, 84 | mgpplusg 18316 |
. . . . . . . . . . . . . . . . 17
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
86 | 80, 82, 85 | mhmlin 17165 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ 𝑘 ∈ (Base‘𝑍) ∧ 𝑎 ∈ (Base‘𝑍)) → (𝑋‘(𝑘(.r‘𝑍)𝑎)) = ((𝑋‘𝑘) · (𝑋‘𝑎))) |
87 | 76, 77, 78, 86 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑎 ∈ 𝑈) → (𝑋‘(𝑘(.r‘𝑍)𝑎)) = ((𝑋‘𝑘) · (𝑋‘𝑎))) |
88 | 87 | sumeq2dv 14281 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → Σ𝑎 ∈ 𝑈 (𝑋‘(𝑘(.r‘𝑍)𝑎)) = Σ𝑎 ∈ 𝑈 ((𝑋‘𝑘) · (𝑋‘𝑎))) |
89 | 73, 88 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → Σ𝑥 ∈ 𝑈 (𝑋‘(𝑘(.r‘𝑍)𝑥)) = Σ𝑎 ∈ 𝑈 ((𝑋‘𝑘) · (𝑋‘𝑎))) |
90 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑘(.r‘𝑍)𝑥) → (𝑋‘𝑎) = (𝑋‘(𝑘(.r‘𝑍)𝑥))) |
91 | 11 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
92 | 5 | zncrng 19712 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
93 | | crngring 18381 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
94 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
((mulGrp‘𝑍)
↾s 𝑈) =
((mulGrp‘𝑍)
↾s 𝑈) |
95 | 7, 94 | unitgrp 18490 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍 ∈ Ring →
((mulGrp‘𝑍)
↾s 𝑈)
∈ Grp) |
96 | 91, 92, 93, 95 | 4syl 19 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((mulGrp‘𝑍) ↾s 𝑈) ∈ Grp) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → ((mulGrp‘𝑍) ↾s 𝑈) ∈ Grp) |
98 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐))) = (𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐))) |
99 | 7, 94 | unitgrpbas 18489 |
. . . . . . . . . . . . . . . 16
⊢ 𝑈 =
(Base‘((mulGrp‘𝑍) ↾s 𝑈)) |
100 | 94, 82 | ressplusg 15818 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ V →
(.r‘𝑍) =
(+g‘((mulGrp‘𝑍) ↾s 𝑈))) |
101 | 24, 100 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(.r‘𝑍) =
(+g‘((mulGrp‘𝑍) ↾s 𝑈)) |
102 | 98, 99, 101 | grplactf1o 17342 |
. . . . . . . . . . . . . . 15
⊢
((((mulGrp‘𝑍)
↾s 𝑈)
∈ Grp ∧ 𝑘 ∈
𝑈) → ((𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐)))‘𝑘):𝑈–1-1-onto→𝑈) |
103 | 97, 61, 102 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → ((𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐)))‘𝑘):𝑈–1-1-onto→𝑈) |
104 | 98, 99 | grplactval 17340 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈) → (((𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐)))‘𝑘)‘𝑥) = (𝑘(.r‘𝑍)𝑥)) |
105 | 61, 104 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) ∧ 𝑥 ∈ 𝑈) → (((𝑏 ∈ 𝑈 ↦ (𝑐 ∈ 𝑈 ↦ (𝑏(.r‘𝑍)𝑐)))‘𝑘)‘𝑥) = (𝑘(.r‘𝑍)𝑥)) |
106 | 90, 50, 103, 105, 57 | fsumf1o 14301 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = Σ𝑥 ∈ 𝑈 (𝑋‘(𝑘(.r‘𝑍)𝑥))) |
107 | 50, 63, 57 | fsummulc2 14358 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → ((𝑋‘𝑘) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = Σ𝑎 ∈ 𝑈 ((𝑋‘𝑘) · (𝑋‘𝑎))) |
108 | 89, 106, 107 | 3eqtr4rd 2655 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → ((𝑋‘𝑘) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) |
109 | 58 | mulid2d 9937 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (1 · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) |
110 | 108, 109 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) − (1 · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎))) = (Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) − Σ𝑎 ∈ 𝑈 (𝑋‘𝑎))) |
111 | 58 | subidd 10259 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) − Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = 0) |
112 | 110, 111 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) − (1 · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎))) = 0) |
113 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → 1 ∈
ℂ) |
114 | 63, 113, 58 | subdird 10366 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) − 1) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = (((𝑋‘𝑘) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) − (1 · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)))) |
115 | 65 | mul01d 10114 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) − 1) · 0) =
0) |
116 | 112, 114,
115 | 3eqtr4d 2654 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → (((𝑋‘𝑘) − 1) · Σ𝑎 ∈ 𝑈 (𝑋‘𝑎)) = (((𝑋‘𝑘) − 1) · 0)) |
117 | 58, 59, 65, 70, 116 | mulcanad 10541 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑈 ∧ (𝑋‘𝑘) ≠ 1)) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0) |
118 | 117 | expr 641 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → ((𝑋‘𝑘) ≠ 1 → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0)) |
119 | 49, 118 | sylbid 229 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → ((𝑋‘𝑘) ≠ ( 1 ‘𝑘) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0)) |
120 | 45, 119 | syl5bir 232 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (¬ (𝑋‘𝑘) = ( 1 ‘𝑘) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0)) |
121 | 120 | rexlimdva 3013 |
. . . 4
⊢ (𝜑 → (∃𝑘 ∈ 𝑈 ¬ (𝑋‘𝑘) = ( 1 ‘𝑘) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0)) |
122 | 44, 121 | sylbid 229 |
. . 3
⊢ (𝜑 → (¬ 𝑋 = 1 → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0)) |
123 | 122 | imp 444 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = 1 ) → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = 0) |
124 | 1, 2, 36, 123 | ifbothda 4073 |
1
⊢ (𝜑 → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = if(𝑋 = 1 , (ϕ‘𝑁), 0)) |