Step | Hyp | Ref
| Expression |
1 | | fvexd 6689 |
. . . 4
⊢ (𝑧 = 〈𝑝, 𝑘〉 → (↑‘𝑧) ∈ V) |
2 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑝, 𝑘〉 → (↑‘𝑧) = (↑‘〈𝑝, 𝑘〉)) |
3 | | df-ov 7173 |
. . . . . . . 8
⊢ (𝑝↑𝑘) = (↑‘〈𝑝, 𝑘〉) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . . 7
⊢ (𝑧 = 〈𝑝, 𝑘〉 → (↑‘𝑧) = (𝑝↑𝑘)) |
5 | 4 | eqeq2d 2749 |
. . . . . 6
⊢ (𝑧 = 〈𝑝, 𝑘〉 → (𝑥 = (↑‘𝑧) ↔ 𝑥 = (𝑝↑𝑘))) |
6 | 5 | biimpa 480 |
. . . . 5
⊢ ((𝑧 = 〈𝑝, 𝑘〉 ∧ 𝑥 = (↑‘𝑧)) → 𝑥 = (𝑝↑𝑘)) |
7 | | fsumvma.1 |
. . . . 5
⊢ (𝑥 = (𝑝↑𝑘) → 𝐵 = 𝐶) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ ((𝑧 = 〈𝑝, 𝑘〉 ∧ 𝑥 = (↑‘𝑧)) → 𝐵 = 𝐶) |
9 | 1, 8 | csbied 3826 |
. . 3
⊢ (𝑧 = 〈𝑝, 𝑘〉 →
⦋(↑‘𝑧) / 𝑥⦌𝐵 = 𝐶) |
10 | | fsumvma.4 |
. . 3
⊢ (𝜑 → 𝑃 ∈ Fin) |
11 | | fsumvma.2 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ Fin) |
12 | 11 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ Fin) |
13 | | fsumvma.5 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ 𝐴))) |
14 | 13 | biimpd 232 |
. . . . . . . 8
⊢ (𝜑 → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) → ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ 𝐴))) |
15 | 14 | impl 459 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑘 ∈ 𝐾) → ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ 𝐴)) |
16 | 15 | simprd 499 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑘 ∈ 𝐾) → (𝑝↑𝑘) ∈ 𝐴) |
17 | 16 | ex 416 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → (𝑘 ∈ 𝐾 → (𝑝↑𝑘) ∈ 𝐴)) |
18 | 15 | simpld 498 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑘 ∈ 𝐾) → (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) |
19 | 18 | simpld 498 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑘 ∈ 𝐾) → 𝑝 ∈ ℙ) |
20 | 19 | adantrr 717 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑝 ∈ ℙ) |
21 | 18 | simprd 499 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑘 ∈ 𝐾) → 𝑘 ∈ ℕ) |
22 | 21 | adantrr 717 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑘 ∈ ℕ) |
23 | 21 | ex 416 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → (𝑘 ∈ 𝐾 → 𝑘 ∈ ℕ)) |
24 | 23 | ssrdv 3883 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝐾 ⊆ ℕ) |
25 | 24 | sselda 3877 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑧 ∈ 𝐾) → 𝑧 ∈ ℕ) |
26 | 25 | adantrl 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑧 ∈ ℕ) |
27 | | eqid 2738 |
. . . . . . . 8
⊢ 𝑝 = 𝑝 |
28 | | prmexpb 16161 |
. . . . . . . . 9
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∈ ℙ) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ ℕ)) → ((𝑝↑𝑘) = (𝑝↑𝑧) ↔ (𝑝 = 𝑝 ∧ 𝑘 = 𝑧))) |
29 | 28 | baibd 543 |
. . . . . . . 8
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∈ ℙ) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ ℕ)) ∧ 𝑝 = 𝑝) → ((𝑝↑𝑘) = (𝑝↑𝑧) ↔ 𝑘 = 𝑧)) |
30 | 27, 29 | mpan2 691 |
. . . . . . 7
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∈ ℙ) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ ℕ)) → ((𝑝↑𝑘) = (𝑝↑𝑧) ↔ 𝑘 = 𝑧)) |
31 | 20, 20, 22, 26, 30 | syl22anc 838 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑝↑𝑘) = (𝑝↑𝑧) ↔ 𝑘 = 𝑧)) |
32 | 31 | ex 416 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → ((𝑝↑𝑘) = (𝑝↑𝑧) ↔ 𝑘 = 𝑧))) |
33 | 17, 32 | dom2lem 8595 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → (𝑘 ∈ 𝐾 ↦ (𝑝↑𝑘)):𝐾–1-1→𝐴) |
34 | | f1fi 8884 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑘 ∈ 𝐾 ↦ (𝑝↑𝑘)):𝐾–1-1→𝐴) → 𝐾 ∈ Fin) |
35 | 12, 33, 34 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝐾 ∈ Fin) |
36 | 7 | eleq1d 2817 |
. . . 4
⊢ (𝑥 = (𝑝↑𝑘) → (𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ)) |
37 | | fsumvma.6 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
38 | 37 | ralrimiva 3096 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ ℂ) |
39 | 38 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → ∀𝑥 ∈ 𝐴 𝐵 ∈ ℂ) |
40 | 13 | simplbda 503 |
. . . 4
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (𝑝↑𝑘) ∈ 𝐴) |
41 | 36, 39, 40 | rspcdva 3528 |
. . 3
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → 𝐶 ∈ ℂ) |
42 | 9, 10, 35, 41 | fsum2d 15219 |
. 2
⊢ (𝜑 → Σ𝑝 ∈ 𝑃 Σ𝑘 ∈ 𝐾 𝐶 = Σ𝑧 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)⦋(↑‘𝑧) / 𝑥⦌𝐵) |
43 | | nfcv 2899 |
. . . 4
⊢
Ⅎ𝑦𝐵 |
44 | | nfcsb1v 3814 |
. . . 4
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
45 | | csbeq1a 3804 |
. . . 4
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
46 | 43, 44, 45 | cbvsumi 15147 |
. . 3
⊢
Σ𝑥 ∈ ran
(𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))𝐵 = Σ𝑦 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))⦋𝑦 / 𝑥⦌𝐵 |
47 | | csbeq1 3793 |
. . . 4
⊢ (𝑦 = (↑‘𝑧) → ⦋𝑦 / 𝑥⦌𝐵 = ⦋(↑‘𝑧) / 𝑥⦌𝐵) |
48 | | snfi 8642 |
. . . . . . 7
⊢ {𝑝} ∈ Fin |
49 | | xpfi 8863 |
. . . . . . 7
⊢ (({𝑝} ∈ Fin ∧ 𝐾 ∈ Fin) → ({𝑝} × 𝐾) ∈ Fin) |
50 | 48, 35, 49 | sylancr 590 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → ({𝑝} × 𝐾) ∈ Fin) |
51 | 50 | ralrimiva 3096 |
. . . . 5
⊢ (𝜑 → ∀𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∈ Fin) |
52 | | iunfi 8885 |
. . . . 5
⊢ ((𝑃 ∈ Fin ∧ ∀𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∈ Fin) → ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∈ Fin) |
53 | 10, 51, 52 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∈ Fin) |
54 | | fvex 6687 |
. . . . . . 7
⊢
(↑‘𝑎)
∈ V |
55 | 54 | 2a1i 12 |
. . . . . 6
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) → (↑‘𝑎) ∈ V)) |
56 | | eliunxp 5680 |
. . . . . . . . 9
⊢ (𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↔ ∃𝑝∃𝑘(𝑎 = 〈𝑝, 𝑘〉 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾))) |
57 | 13 | simprbda 502 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) |
58 | | opelxp 5561 |
. . . . . . . . . . . . . 14
⊢
(〈𝑝, 𝑘〉 ∈ (ℙ ×
ℕ) ↔ (𝑝 ∈
ℙ ∧ 𝑘 ∈
ℕ)) |
59 | 57, 58 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → 〈𝑝, 𝑘〉 ∈ (ℙ ×
ℕ)) |
60 | | eleq1 2820 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑝, 𝑘〉 → (𝑎 ∈ (ℙ × ℕ) ↔
〈𝑝, 𝑘〉 ∈ (ℙ ×
ℕ))) |
61 | 59, 60 | syl5ibrcom 250 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (𝑎 = 〈𝑝, 𝑘〉 → 𝑎 ∈ (ℙ ×
ℕ))) |
62 | 61 | impancom 455 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 = 〈𝑝, 𝑘〉) → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) → 𝑎 ∈ (ℙ ×
ℕ))) |
63 | 62 | expimpd 457 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑎 = 〈𝑝, 𝑘〉 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → 𝑎 ∈ (ℙ ×
ℕ))) |
64 | 63 | exlimdvv 1941 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑝∃𝑘(𝑎 = 〈𝑝, 𝑘〉 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → 𝑎 ∈ (ℙ ×
ℕ))) |
65 | 56, 64 | syl5bi 245 |
. . . . . . . 8
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) → 𝑎 ∈ (ℙ ×
ℕ))) |
66 | 65 | ssrdv 3883 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ⊆ (ℙ ×
ℕ)) |
67 | 66 | sseld 3876 |
. . . . . . . 8
⊢ (𝜑 → (𝑏 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) → 𝑏 ∈ (ℙ ×
ℕ))) |
68 | 65, 67 | anim12d 612 |
. . . . . . 7
⊢ (𝜑 → ((𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∧ 𝑏 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)) → (𝑎 ∈ (ℙ × ℕ) ∧ 𝑏 ∈ (ℙ ×
ℕ)))) |
69 | | 1st2nd2 7753 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (ℙ ×
ℕ) → 𝑎 =
〈(1st ‘𝑎), (2nd ‘𝑎)〉) |
70 | 69 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (ℙ ×
ℕ) → (↑‘𝑎) = (↑‘〈(1st
‘𝑎), (2nd
‘𝑎)〉)) |
71 | | df-ov 7173 |
. . . . . . . . . 10
⊢
((1st ‘𝑎)↑(2nd ‘𝑎)) =
(↑‘〈(1st ‘𝑎), (2nd ‘𝑎)〉) |
72 | 70, 71 | eqtr4di 2791 |
. . . . . . . . 9
⊢ (𝑎 ∈ (ℙ ×
ℕ) → (↑‘𝑎) = ((1st ‘𝑎)↑(2nd
‘𝑎))) |
73 | | 1st2nd2 7753 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (ℙ ×
ℕ) → 𝑏 =
〈(1st ‘𝑏), (2nd ‘𝑏)〉) |
74 | 73 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (ℙ ×
ℕ) → (↑‘𝑏) = (↑‘〈(1st
‘𝑏), (2nd
‘𝑏)〉)) |
75 | | df-ov 7173 |
. . . . . . . . . 10
⊢
((1st ‘𝑏)↑(2nd ‘𝑏)) =
(↑‘〈(1st ‘𝑏), (2nd ‘𝑏)〉) |
76 | 74, 75 | eqtr4di 2791 |
. . . . . . . . 9
⊢ (𝑏 ∈ (ℙ ×
ℕ) → (↑‘𝑏) = ((1st ‘𝑏)↑(2nd
‘𝑏))) |
77 | 72, 76 | eqeqan12d 2755 |
. . . . . . . 8
⊢ ((𝑎 ∈ (ℙ ×
ℕ) ∧ 𝑏 ∈
(ℙ × ℕ)) → ((↑‘𝑎) = (↑‘𝑏) ↔ ((1st ‘𝑎)↑(2nd
‘𝑎)) =
((1st ‘𝑏)↑(2nd ‘𝑏)))) |
78 | | xp1st 7746 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (ℙ ×
ℕ) → (1st ‘𝑎) ∈ ℙ) |
79 | | xp2nd 7747 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (ℙ ×
ℕ) → (2nd ‘𝑎) ∈ ℕ) |
80 | 78, 79 | jca 515 |
. . . . . . . . 9
⊢ (𝑎 ∈ (ℙ ×
ℕ) → ((1st ‘𝑎) ∈ ℙ ∧ (2nd
‘𝑎) ∈
ℕ)) |
81 | | xp1st 7746 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (ℙ ×
ℕ) → (1st ‘𝑏) ∈ ℙ) |
82 | | xp2nd 7747 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (ℙ ×
ℕ) → (2nd ‘𝑏) ∈ ℕ) |
83 | 81, 82 | jca 515 |
. . . . . . . . 9
⊢ (𝑏 ∈ (ℙ ×
ℕ) → ((1st ‘𝑏) ∈ ℙ ∧ (2nd
‘𝑏) ∈
ℕ)) |
84 | | prmexpb 16161 |
. . . . . . . . . 10
⊢
((((1st ‘𝑎) ∈ ℙ ∧ (1st
‘𝑏) ∈ ℙ)
∧ ((2nd ‘𝑎) ∈ ℕ ∧ (2nd
‘𝑏) ∈ ℕ))
→ (((1st ‘𝑎)↑(2nd ‘𝑎)) = ((1st
‘𝑏)↑(2nd ‘𝑏)) ↔ ((1st
‘𝑎) = (1st
‘𝑏) ∧
(2nd ‘𝑎) =
(2nd ‘𝑏)))) |
85 | 84 | an4s 660 |
. . . . . . . . 9
⊢
((((1st ‘𝑎) ∈ ℙ ∧ (2nd
‘𝑎) ∈ ℕ)
∧ ((1st ‘𝑏) ∈ ℙ ∧ (2nd
‘𝑏) ∈ ℕ))
→ (((1st ‘𝑎)↑(2nd ‘𝑎)) = ((1st
‘𝑏)↑(2nd ‘𝑏)) ↔ ((1st
‘𝑎) = (1st
‘𝑏) ∧
(2nd ‘𝑎) =
(2nd ‘𝑏)))) |
86 | 80, 83, 85 | syl2an 599 |
. . . . . . . 8
⊢ ((𝑎 ∈ (ℙ ×
ℕ) ∧ 𝑏 ∈
(ℙ × ℕ)) → (((1st ‘𝑎)↑(2nd ‘𝑎)) = ((1st
‘𝑏)↑(2nd ‘𝑏)) ↔ ((1st
‘𝑎) = (1st
‘𝑏) ∧
(2nd ‘𝑎) =
(2nd ‘𝑏)))) |
87 | | xpopth 7755 |
. . . . . . . 8
⊢ ((𝑎 ∈ (ℙ ×
ℕ) ∧ 𝑏 ∈
(ℙ × ℕ)) → (((1st ‘𝑎) = (1st ‘𝑏) ∧ (2nd ‘𝑎) = (2nd ‘𝑏)) ↔ 𝑎 = 𝑏)) |
88 | 77, 86, 87 | 3bitrd 308 |
. . . . . . 7
⊢ ((𝑎 ∈ (ℙ ×
ℕ) ∧ 𝑏 ∈
(ℙ × ℕ)) → ((↑‘𝑎) = (↑‘𝑏) ↔ 𝑎 = 𝑏)) |
89 | 68, 88 | syl6 35 |
. . . . . 6
⊢ (𝜑 → ((𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∧ 𝑏 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)) → ((↑‘𝑎) = (↑‘𝑏) ↔ 𝑎 = 𝑏))) |
90 | 55, 89 | dom2lem 8595 |
. . . . 5
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)):∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)–1-1→V) |
91 | | f1f1orn 6629 |
. . . . 5
⊢ ((𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)):∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)–1-1→V → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)):∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)–1-1-onto→ran
(𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) |
92 | 90, 91 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)):∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)–1-1-onto→ran
(𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) |
93 | | fveq2 6674 |
. . . . . 6
⊢ (𝑎 = 𝑧 → (↑‘𝑎) = (↑‘𝑧)) |
94 | | eqid 2738 |
. . . . . 6
⊢ (𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) = (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) |
95 | | fvex 6687 |
. . . . . 6
⊢
(↑‘𝑧)
∈ V |
96 | 93, 94, 95 | fvmpt 6775 |
. . . . 5
⊢ (𝑧 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) → ((𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))‘𝑧) = (↑‘𝑧)) |
97 | 96 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)) → ((𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))‘𝑧) = (↑‘𝑧)) |
98 | | fveq2 6674 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 〈𝑝, 𝑘〉 → (↑‘𝑎) = (↑‘〈𝑝, 𝑘〉)) |
99 | 98, 3 | eqtr4di 2791 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 〈𝑝, 𝑘〉 → (↑‘𝑎) = (𝑝↑𝑘)) |
100 | 99 | eleq1d 2817 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 〈𝑝, 𝑘〉 → ((↑‘𝑎) ∈ 𝐴 ↔ (𝑝↑𝑘) ∈ 𝐴)) |
101 | 40, 100 | syl5ibrcom 250 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (𝑎 = 〈𝑝, 𝑘〉 → (↑‘𝑎) ∈ 𝐴)) |
102 | 101 | impancom 455 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 = 〈𝑝, 𝑘〉) → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) → (↑‘𝑎) ∈ 𝐴)) |
103 | 102 | expimpd 457 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑎 = 〈𝑝, 𝑘〉 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (↑‘𝑎) ∈ 𝐴)) |
104 | 103 | exlimdvv 1941 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑝∃𝑘(𝑎 = 〈𝑝, 𝑘〉 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (↑‘𝑎) ∈ 𝐴)) |
105 | 56, 104 | syl5bi 245 |
. . . . . . . . 9
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) → (↑‘𝑎) ∈ 𝐴)) |
106 | 105 | imp 410 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)) → (↑‘𝑎) ∈ 𝐴) |
107 | 106 | fmpttd 6889 |
. . . . . . 7
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)):∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)⟶𝐴) |
108 | 107 | frnd 6512 |
. . . . . 6
⊢ (𝜑 → ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) ⊆ 𝐴) |
109 | 108 | sselda 3877 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → 𝑦 ∈ 𝐴) |
110 | 44 | nfel1 2915 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ℂ |
111 | 45 | eleq1d 2817 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐵 ∈ ℂ ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ ℂ)) |
112 | 110, 111 | rspc 3514 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℂ)) |
113 | 38, 112 | mpan9 510 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℂ) |
114 | 109, 113 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℂ) |
115 | 47, 53, 92, 97, 114 | fsumf1o 15173 |
. . 3
⊢ (𝜑 → Σ𝑦 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))⦋𝑦 / 𝑥⦌𝐵 = Σ𝑧 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)⦋(↑‘𝑧) / 𝑥⦌𝐵) |
116 | 46, 115 | syl5eq 2785 |
. 2
⊢ (𝜑 → Σ𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))𝐵 = Σ𝑧 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)⦋(↑‘𝑧) / 𝑥⦌𝐵) |
117 | 108 | sselda 3877 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → 𝑥 ∈ 𝐴) |
118 | 117, 37 | syldan 594 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → 𝐵 ∈ ℂ) |
119 | | eldif 3853 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)))) |
120 | 94, 54 | elrnmpti 5803 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) ↔ ∃𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)𝑥 = (↑‘𝑎)) |
121 | 99 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ (𝑎 = 〈𝑝, 𝑘〉 → (𝑥 = (↑‘𝑎) ↔ 𝑥 = (𝑝↑𝑘))) |
122 | 121 | rexiunxp 5683 |
. . . . . . . . . 10
⊢
(∃𝑎 ∈
∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)𝑥 = (↑‘𝑎) ↔ ∃𝑝 ∈ 𝑃 ∃𝑘 ∈ 𝐾 𝑥 = (𝑝↑𝑘)) |
123 | 120, 122 | bitri 278 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) ↔ ∃𝑝 ∈ 𝑃 ∃𝑘 ∈ 𝐾 𝑥 = (𝑝↑𝑘)) |
124 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = (𝑝↑𝑘)) → 𝑥 = (𝑝↑𝑘)) |
125 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = (𝑝↑𝑘)) → 𝑥 ∈ 𝐴) |
126 | 124, 125 | eqeltrrd 2834 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = (𝑝↑𝑘)) → (𝑝↑𝑘) ∈ 𝐴) |
127 | 13 | rbaibd 544 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑝↑𝑘) ∈ 𝐴) → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ↔ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ))) |
128 | 127 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑝↑𝑘) ∈ 𝐴) → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ↔ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ))) |
129 | 126, 128 | syldan 594 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = (𝑝↑𝑘)) → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ↔ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ))) |
130 | 129 | pm5.32da 582 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 = (𝑝↑𝑘) ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) ↔ (𝑥 = (𝑝↑𝑘) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)))) |
131 | | ancom 464 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ∧ 𝑥 = (𝑝↑𝑘)) ↔ (𝑥 = (𝑝↑𝑘) ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾))) |
132 | | ancom 464 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 𝑥 = (𝑝↑𝑘)) ↔ (𝑥 = (𝑝↑𝑘) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ))) |
133 | 130, 131,
132 | 3bitr4g 317 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ∧ 𝑥 = (𝑝↑𝑘)) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 𝑥 = (𝑝↑𝑘)))) |
134 | 133 | 2exbidv 1931 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑝∃𝑘((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ∧ 𝑥 = (𝑝↑𝑘)) ↔ ∃𝑝∃𝑘((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 𝑥 = (𝑝↑𝑘)))) |
135 | | r2ex 3213 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
𝑃 ∃𝑘 ∈ 𝐾 𝑥 = (𝑝↑𝑘) ↔ ∃𝑝∃𝑘((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ∧ 𝑥 = (𝑝↑𝑘))) |
136 | | r2ex 3213 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
ℙ ∃𝑘 ∈
ℕ 𝑥 = (𝑝↑𝑘) ↔ ∃𝑝∃𝑘((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 𝑥 = (𝑝↑𝑘))) |
137 | 134, 135,
136 | 3bitr4g 317 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑝 ∈ 𝑃 ∃𝑘 ∈ 𝐾 𝑥 = (𝑝↑𝑘) ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝑥 = (𝑝↑𝑘))) |
138 | | fsumvma.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
139 | 138 | sselda 3877 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℕ) |
140 | | isppw2 25852 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ →
((Λ‘𝑥) ≠ 0
↔ ∃𝑝 ∈
ℙ ∃𝑘 ∈
ℕ 𝑥 = (𝑝↑𝑘))) |
141 | 139, 140 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Λ‘𝑥) ≠ 0 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝑥 = (𝑝↑𝑘))) |
142 | 137, 141 | bitr4d 285 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑝 ∈ 𝑃 ∃𝑘 ∈ 𝐾 𝑥 = (𝑝↑𝑘) ↔ (Λ‘𝑥) ≠ 0)) |
143 | 123, 142 | syl5bb 286 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) ↔ (Λ‘𝑥) ≠ 0)) |
144 | 143 | necon2bbid 2977 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Λ‘𝑥) = 0 ↔ ¬ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)))) |
145 | 144 | pm5.32da 582 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ (Λ‘𝑥) = 0) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))))) |
146 | | fsumvma.7 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (Λ‘𝑥) = 0)) → 𝐵 = 0) |
147 | 146 | ex 416 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ (Λ‘𝑥) = 0) → 𝐵 = 0)) |
148 | 145, 147 | sylbird 263 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → 𝐵 = 0)) |
149 | 119, 148 | syl5bi 245 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → 𝐵 = 0)) |
150 | 149 | imp 410 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)))) → 𝐵 = 0) |
151 | 108, 118,
150, 11 | fsumss 15175 |
. 2
⊢ (𝜑 → Σ𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))𝐵 = Σ𝑥 ∈ 𝐴 𝐵) |
152 | 42, 116, 151 | 3eqtr2rd 2780 |
1
⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑝 ∈ 𝑃 Σ𝑘 ∈ 𝐾 𝐶) |