Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . 5
⊢
(↑‘𝑧)
∈ V |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝑧 = 〈𝑝, 𝑘〉 → (↑‘𝑧) ∈ V) |
3 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑝, 𝑘〉 → (↑‘𝑧) = (↑‘〈𝑝, 𝑘〉)) |
4 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝑝↑𝑘) = (↑‘〈𝑝, 𝑘〉) |
5 | 3, 4 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑧 = 〈𝑝, 𝑘〉 → (↑‘𝑧) = (𝑝↑𝑘)) |
6 | 5 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑧 = 〈𝑝, 𝑘〉 → (𝑥 = (↑‘𝑧) ↔ 𝑥 = (𝑝↑𝑘))) |
7 | 6 | biimpa 500 |
. . . . 5
⊢ ((𝑧 = 〈𝑝, 𝑘〉 ∧ 𝑥 = (↑‘𝑧)) → 𝑥 = (𝑝↑𝑘)) |
8 | | fsumvma.1 |
. . . . 5
⊢ (𝑥 = (𝑝↑𝑘) → 𝐵 = 𝐶) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ ((𝑧 = 〈𝑝, 𝑘〉 ∧ 𝑥 = (↑‘𝑧)) → 𝐵 = 𝐶) |
10 | 2, 9 | csbied 3526 |
. . 3
⊢ (𝑧 = 〈𝑝, 𝑘〉 →
⦋(↑‘𝑧) / 𝑥⦌𝐵 = 𝐶) |
11 | | fsumvma.4 |
. . 3
⊢ (𝜑 → 𝑃 ∈ Fin) |
12 | | fsumvma.2 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ Fin) |
13 | 12 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ Fin) |
14 | | fsumvma.5 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ 𝐴))) |
15 | 14 | biimpd 218 |
. . . . . . . 8
⊢ (𝜑 → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) → ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ 𝐴))) |
16 | 15 | impl 648 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑘 ∈ 𝐾) → ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ 𝐴)) |
17 | 16 | simprd 478 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑘 ∈ 𝐾) → (𝑝↑𝑘) ∈ 𝐴) |
18 | 17 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → (𝑘 ∈ 𝐾 → (𝑝↑𝑘) ∈ 𝐴)) |
19 | 16 | simpld 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑘 ∈ 𝐾) → (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) |
20 | 19 | simpld 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑘 ∈ 𝐾) → 𝑝 ∈ ℙ) |
21 | 20 | adantrr 749 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑝 ∈ ℙ) |
22 | 19 | simprd 478 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑘 ∈ 𝐾) → 𝑘 ∈ ℕ) |
23 | 22 | adantrr 749 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑘 ∈ ℕ) |
24 | 22 | ex 449 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → (𝑘 ∈ 𝐾 → 𝑘 ∈ ℕ)) |
25 | 24 | ssrdv 3574 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝐾 ⊆ ℕ) |
26 | 25 | sselda 3568 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑧 ∈ 𝐾) → 𝑧 ∈ ℕ) |
27 | 26 | adantrl 748 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑧 ∈ ℕ) |
28 | | eqid 2610 |
. . . . . . . 8
⊢ 𝑝 = 𝑝 |
29 | | prmexpb 15268 |
. . . . . . . . 9
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∈ ℙ) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ ℕ)) → ((𝑝↑𝑘) = (𝑝↑𝑧) ↔ (𝑝 = 𝑝 ∧ 𝑘 = 𝑧))) |
30 | 29 | baibd 946 |
. . . . . . . 8
⊢ ((((𝑝 ∈ ℙ ∧ 𝑝 ∈ ℙ) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ ℕ)) ∧ 𝑝 = 𝑝) → ((𝑝↑𝑘) = (𝑝↑𝑧) ↔ 𝑘 = 𝑧)) |
31 | 28, 30 | mpan2 703 |
. . . . . . 7
⊢ (((𝑝 ∈ ℙ ∧ 𝑝 ∈ ℙ) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ ℕ)) → ((𝑝↑𝑘) = (𝑝↑𝑧) ↔ 𝑘 = 𝑧)) |
32 | 21, 21, 23, 27, 31 | syl22anc 1319 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑝↑𝑘) = (𝑝↑𝑧) ↔ 𝑘 = 𝑧)) |
33 | 32 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → ((𝑝↑𝑘) = (𝑝↑𝑧) ↔ 𝑘 = 𝑧))) |
34 | 18, 33 | dom2lem 7881 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → (𝑘 ∈ 𝐾 ↦ (𝑝↑𝑘)):𝐾–1-1→𝐴) |
35 | | f1fi 8136 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝑘 ∈ 𝐾 ↦ (𝑝↑𝑘)):𝐾–1-1→𝐴) → 𝐾 ∈ Fin) |
36 | 13, 34, 35 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝐾 ∈ Fin) |
37 | 14 | simplbda 652 |
. . . 4
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (𝑝↑𝑘) ∈ 𝐴) |
38 | | fsumvma.6 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
39 | 38 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ ℂ) |
40 | 39 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → ∀𝑥 ∈ 𝐴 𝐵 ∈ ℂ) |
41 | 8 | eleq1d 2672 |
. . . . 5
⊢ (𝑥 = (𝑝↑𝑘) → (𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ)) |
42 | 41 | rspcv 3278 |
. . . 4
⊢ ((𝑝↑𝑘) ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝐵 ∈ ℂ → 𝐶 ∈ ℂ)) |
43 | 37, 40, 42 | sylc 63 |
. . 3
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → 𝐶 ∈ ℂ) |
44 | 10, 11, 36, 43 | fsum2d 14344 |
. 2
⊢ (𝜑 → Σ𝑝 ∈ 𝑃 Σ𝑘 ∈ 𝐾 𝐶 = Σ𝑧 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)⦋(↑‘𝑧) / 𝑥⦌𝐵) |
45 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑦𝐵 |
46 | | nfcsb1v 3515 |
. . . 4
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
47 | | csbeq1a 3508 |
. . . 4
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
48 | 45, 46, 47 | cbvsumi 14275 |
. . 3
⊢
Σ𝑥 ∈ ran
(𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))𝐵 = Σ𝑦 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))⦋𝑦 / 𝑥⦌𝐵 |
49 | | csbeq1 3502 |
. . . 4
⊢ (𝑦 = (↑‘𝑧) → ⦋𝑦 / 𝑥⦌𝐵 = ⦋(↑‘𝑧) / 𝑥⦌𝐵) |
50 | | snfi 7923 |
. . . . . . 7
⊢ {𝑝} ∈ Fin |
51 | | xpfi 8116 |
. . . . . . 7
⊢ (({𝑝} ∈ Fin ∧ 𝐾 ∈ Fin) → ({𝑝} × 𝐾) ∈ Fin) |
52 | 50, 36, 51 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → ({𝑝} × 𝐾) ∈ Fin) |
53 | 52 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∈ Fin) |
54 | | iunfi 8137 |
. . . . 5
⊢ ((𝑃 ∈ Fin ∧ ∀𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∈ Fin) → ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∈ Fin) |
55 | 11, 53, 54 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∈ Fin) |
56 | | fvex 6113 |
. . . . . . 7
⊢
(↑‘𝑎)
∈ V |
57 | 56 | 2a1i 12 |
. . . . . 6
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) → (↑‘𝑎) ∈ V)) |
58 | | eliunxp 5181 |
. . . . . . . . 9
⊢ (𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↔ ∃𝑝∃𝑘(𝑎 = 〈𝑝, 𝑘〉 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾))) |
59 | 14 | simprbda 651 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) |
60 | | opelxp 5070 |
. . . . . . . . . . . . . 14
⊢
(〈𝑝, 𝑘〉 ∈ (ℙ ×
ℕ) ↔ (𝑝 ∈
ℙ ∧ 𝑘 ∈
ℕ)) |
61 | 59, 60 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → 〈𝑝, 𝑘〉 ∈ (ℙ ×
ℕ)) |
62 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑝, 𝑘〉 → (𝑎 ∈ (ℙ × ℕ) ↔
〈𝑝, 𝑘〉 ∈ (ℙ ×
ℕ))) |
63 | 61, 62 | syl5ibrcom 236 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (𝑎 = 〈𝑝, 𝑘〉 → 𝑎 ∈ (ℙ ×
ℕ))) |
64 | 63 | impancom 455 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 = 〈𝑝, 𝑘〉) → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) → 𝑎 ∈ (ℙ ×
ℕ))) |
65 | 64 | expimpd 627 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑎 = 〈𝑝, 𝑘〉 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → 𝑎 ∈ (ℙ ×
ℕ))) |
66 | 65 | exlimdvv 1849 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑝∃𝑘(𝑎 = 〈𝑝, 𝑘〉 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → 𝑎 ∈ (ℙ ×
ℕ))) |
67 | 58, 66 | syl5bi 231 |
. . . . . . . 8
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) → 𝑎 ∈ (ℙ ×
ℕ))) |
68 | 67 | ssrdv 3574 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ⊆ (ℙ ×
ℕ)) |
69 | 68 | sseld 3567 |
. . . . . . . 8
⊢ (𝜑 → (𝑏 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) → 𝑏 ∈ (ℙ ×
ℕ))) |
70 | 67, 69 | anim12d 584 |
. . . . . . 7
⊢ (𝜑 → ((𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∧ 𝑏 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)) → (𝑎 ∈ (ℙ × ℕ) ∧ 𝑏 ∈ (ℙ ×
ℕ)))) |
71 | | 1st2nd2 7096 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (ℙ ×
ℕ) → 𝑎 =
〈(1st ‘𝑎), (2nd ‘𝑎)〉) |
72 | 71 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (ℙ ×
ℕ) → (↑‘𝑎) = (↑‘〈(1st
‘𝑎), (2nd
‘𝑎)〉)) |
73 | | df-ov 6552 |
. . . . . . . . . 10
⊢
((1st ‘𝑎)↑(2nd ‘𝑎)) =
(↑‘〈(1st ‘𝑎), (2nd ‘𝑎)〉) |
74 | 72, 73 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑎 ∈ (ℙ ×
ℕ) → (↑‘𝑎) = ((1st ‘𝑎)↑(2nd
‘𝑎))) |
75 | | 1st2nd2 7096 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (ℙ ×
ℕ) → 𝑏 =
〈(1st ‘𝑏), (2nd ‘𝑏)〉) |
76 | 75 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (ℙ ×
ℕ) → (↑‘𝑏) = (↑‘〈(1st
‘𝑏), (2nd
‘𝑏)〉)) |
77 | | df-ov 6552 |
. . . . . . . . . 10
⊢
((1st ‘𝑏)↑(2nd ‘𝑏)) =
(↑‘〈(1st ‘𝑏), (2nd ‘𝑏)〉) |
78 | 76, 77 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑏 ∈ (ℙ ×
ℕ) → (↑‘𝑏) = ((1st ‘𝑏)↑(2nd
‘𝑏))) |
79 | 74, 78 | eqeqan12d 2626 |
. . . . . . . 8
⊢ ((𝑎 ∈ (ℙ ×
ℕ) ∧ 𝑏 ∈
(ℙ × ℕ)) → ((↑‘𝑎) = (↑‘𝑏) ↔ ((1st ‘𝑎)↑(2nd
‘𝑎)) =
((1st ‘𝑏)↑(2nd ‘𝑏)))) |
80 | | xp1st 7089 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (ℙ ×
ℕ) → (1st ‘𝑎) ∈ ℙ) |
81 | | xp2nd 7090 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (ℙ ×
ℕ) → (2nd ‘𝑎) ∈ ℕ) |
82 | 80, 81 | jca 553 |
. . . . . . . . 9
⊢ (𝑎 ∈ (ℙ ×
ℕ) → ((1st ‘𝑎) ∈ ℙ ∧ (2nd
‘𝑎) ∈
ℕ)) |
83 | | xp1st 7089 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (ℙ ×
ℕ) → (1st ‘𝑏) ∈ ℙ) |
84 | | xp2nd 7090 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (ℙ ×
ℕ) → (2nd ‘𝑏) ∈ ℕ) |
85 | 83, 84 | jca 553 |
. . . . . . . . 9
⊢ (𝑏 ∈ (ℙ ×
ℕ) → ((1st ‘𝑏) ∈ ℙ ∧ (2nd
‘𝑏) ∈
ℕ)) |
86 | | prmexpb 15268 |
. . . . . . . . . 10
⊢
((((1st ‘𝑎) ∈ ℙ ∧ (1st
‘𝑏) ∈ ℙ)
∧ ((2nd ‘𝑎) ∈ ℕ ∧ (2nd
‘𝑏) ∈ ℕ))
→ (((1st ‘𝑎)↑(2nd ‘𝑎)) = ((1st
‘𝑏)↑(2nd ‘𝑏)) ↔ ((1st
‘𝑎) = (1st
‘𝑏) ∧
(2nd ‘𝑎) =
(2nd ‘𝑏)))) |
87 | 86 | an4s 865 |
. . . . . . . . 9
⊢
((((1st ‘𝑎) ∈ ℙ ∧ (2nd
‘𝑎) ∈ ℕ)
∧ ((1st ‘𝑏) ∈ ℙ ∧ (2nd
‘𝑏) ∈ ℕ))
→ (((1st ‘𝑎)↑(2nd ‘𝑎)) = ((1st
‘𝑏)↑(2nd ‘𝑏)) ↔ ((1st
‘𝑎) = (1st
‘𝑏) ∧
(2nd ‘𝑎) =
(2nd ‘𝑏)))) |
88 | 82, 85, 87 | syl2an 493 |
. . . . . . . 8
⊢ ((𝑎 ∈ (ℙ ×
ℕ) ∧ 𝑏 ∈
(ℙ × ℕ)) → (((1st ‘𝑎)↑(2nd ‘𝑎)) = ((1st
‘𝑏)↑(2nd ‘𝑏)) ↔ ((1st
‘𝑎) = (1st
‘𝑏) ∧
(2nd ‘𝑎) =
(2nd ‘𝑏)))) |
89 | | xpopth 7098 |
. . . . . . . 8
⊢ ((𝑎 ∈ (ℙ ×
ℕ) ∧ 𝑏 ∈
(ℙ × ℕ)) → (((1st ‘𝑎) = (1st ‘𝑏) ∧ (2nd ‘𝑎) = (2nd ‘𝑏)) ↔ 𝑎 = 𝑏)) |
90 | 79, 88, 89 | 3bitrd 293 |
. . . . . . 7
⊢ ((𝑎 ∈ (ℙ ×
ℕ) ∧ 𝑏 ∈
(ℙ × ℕ)) → ((↑‘𝑎) = (↑‘𝑏) ↔ 𝑎 = 𝑏)) |
91 | 70, 90 | syl6 34 |
. . . . . 6
⊢ (𝜑 → ((𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ∧ 𝑏 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)) → ((↑‘𝑎) = (↑‘𝑏) ↔ 𝑎 = 𝑏))) |
92 | 57, 91 | dom2lem 7881 |
. . . . 5
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)):∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)–1-1→V) |
93 | | f1f1orn 6061 |
. . . . 5
⊢ ((𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)):∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)–1-1→V → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)):∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)–1-1-onto→ran
(𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) |
94 | 92, 93 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)):∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)–1-1-onto→ran
(𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) |
95 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = 𝑧 → (↑‘𝑎) = (↑‘𝑧)) |
96 | | eqid 2610 |
. . . . . 6
⊢ (𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) = (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) |
97 | 95, 96, 1 | fvmpt 6191 |
. . . . 5
⊢ (𝑧 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) → ((𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))‘𝑧) = (↑‘𝑧)) |
98 | 97 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)) → ((𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))‘𝑧) = (↑‘𝑧)) |
99 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 〈𝑝, 𝑘〉 → (↑‘𝑎) = (↑‘〈𝑝, 𝑘〉)) |
100 | 99, 4 | syl6eqr 2662 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 〈𝑝, 𝑘〉 → (↑‘𝑎) = (𝑝↑𝑘)) |
101 | 100 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 〈𝑝, 𝑘〉 → ((↑‘𝑎) ∈ 𝐴 ↔ (𝑝↑𝑘) ∈ 𝐴)) |
102 | 37, 101 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (𝑎 = 〈𝑝, 𝑘〉 → (↑‘𝑎) ∈ 𝐴)) |
103 | 102 | impancom 455 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 = 〈𝑝, 𝑘〉) → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) → (↑‘𝑎) ∈ 𝐴)) |
104 | 103 | expimpd 627 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑎 = 〈𝑝, 𝑘〉 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (↑‘𝑎) ∈ 𝐴)) |
105 | 104 | exlimdvv 1849 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑝∃𝑘(𝑎 = 〈𝑝, 𝑘〉 ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) → (↑‘𝑎) ∈ 𝐴)) |
106 | 58, 105 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) → (↑‘𝑎) ∈ 𝐴)) |
107 | 106 | imp 444 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)) → (↑‘𝑎) ∈ 𝐴) |
108 | 107, 96 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)):∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)⟶𝐴) |
109 | | frn 5966 |
. . . . . . 7
⊢ ((𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)):∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)⟶𝐴 → ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) ⊆ 𝐴) |
110 | 108, 109 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) ⊆ 𝐴) |
111 | 110 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → 𝑦 ∈ 𝐴) |
112 | 46 | nfel1 2765 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ℂ |
113 | 47 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐵 ∈ ℂ ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ ℂ)) |
114 | 112, 113 | rspc 3276 |
. . . . . 6
⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℂ)) |
115 | 39, 114 | mpan9 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℂ) |
116 | 111, 115 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℂ) |
117 | 49, 55, 94, 98, 116 | fsumf1o 14301 |
. . 3
⊢ (𝜑 → Σ𝑦 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))⦋𝑦 / 𝑥⦌𝐵 = Σ𝑧 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)⦋(↑‘𝑧) / 𝑥⦌𝐵) |
118 | 48, 117 | syl5eq 2656 |
. 2
⊢ (𝜑 → Σ𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))𝐵 = Σ𝑧 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)⦋(↑‘𝑧) / 𝑥⦌𝐵) |
119 | 110 | sselda 3568 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → 𝑥 ∈ 𝐴) |
120 | 119, 38 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → 𝐵 ∈ ℂ) |
121 | | eldif 3550 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)))) |
122 | 96, 56 | elrnmpti 5297 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) ↔ ∃𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾)𝑥 = (↑‘𝑎)) |
123 | 100 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑎 = 〈𝑝, 𝑘〉 → (𝑥 = (↑‘𝑎) ↔ 𝑥 = (𝑝↑𝑘))) |
124 | 123 | rexiunxp 5184 |
. . . . . . . . . 10
⊢
(∃𝑎 ∈
∪ 𝑝 ∈ 𝑃 ({𝑝} × 𝐾)𝑥 = (↑‘𝑎) ↔ ∃𝑝 ∈ 𝑃 ∃𝑘 ∈ 𝐾 𝑥 = (𝑝↑𝑘)) |
125 | 122, 124 | bitri 263 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) ↔ ∃𝑝 ∈ 𝑃 ∃𝑘 ∈ 𝐾 𝑥 = (𝑝↑𝑘)) |
126 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = (𝑝↑𝑘)) → 𝑥 = (𝑝↑𝑘)) |
127 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = (𝑝↑𝑘)) → 𝑥 ∈ 𝐴) |
128 | 126, 127 | eqeltrrd 2689 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = (𝑝↑𝑘)) → (𝑝↑𝑘) ∈ 𝐴) |
129 | 14 | rbaibd 947 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑝↑𝑘) ∈ 𝐴) → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ↔ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ))) |
130 | 129 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑝↑𝑘) ∈ 𝐴) → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ↔ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ))) |
131 | 128, 130 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = (𝑝↑𝑘)) → ((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ↔ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ))) |
132 | 131 | pm5.32da 671 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 = (𝑝↑𝑘) ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾)) ↔ (𝑥 = (𝑝↑𝑘) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)))) |
133 | | ancom 465 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ∧ 𝑥 = (𝑝↑𝑘)) ↔ (𝑥 = (𝑝↑𝑘) ∧ (𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾))) |
134 | | ancom 465 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 𝑥 = (𝑝↑𝑘)) ↔ (𝑥 = (𝑝↑𝑘) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ))) |
135 | 132, 133,
134 | 3bitr4g 302 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ∧ 𝑥 = (𝑝↑𝑘)) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 𝑥 = (𝑝↑𝑘)))) |
136 | 135 | 2exbidv 1839 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑝∃𝑘((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ∧ 𝑥 = (𝑝↑𝑘)) ↔ ∃𝑝∃𝑘((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 𝑥 = (𝑝↑𝑘)))) |
137 | | r2ex 3043 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
𝑃 ∃𝑘 ∈ 𝐾 𝑥 = (𝑝↑𝑘) ↔ ∃𝑝∃𝑘((𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾) ∧ 𝑥 = (𝑝↑𝑘))) |
138 | | r2ex 3043 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
ℙ ∃𝑘 ∈
ℕ 𝑥 = (𝑝↑𝑘) ↔ ∃𝑝∃𝑘((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 𝑥 = (𝑝↑𝑘))) |
139 | 136, 137,
138 | 3bitr4g 302 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑝 ∈ 𝑃 ∃𝑘 ∈ 𝐾 𝑥 = (𝑝↑𝑘) ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝑥 = (𝑝↑𝑘))) |
140 | | fsumvma.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
141 | 140 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℕ) |
142 | | isppw2 24641 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ →
((Λ‘𝑥) ≠ 0
↔ ∃𝑝 ∈
ℙ ∃𝑘 ∈
ℕ 𝑥 = (𝑝↑𝑘))) |
143 | 141, 142 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Λ‘𝑥) ≠ 0 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝑥 = (𝑝↑𝑘))) |
144 | 139, 143 | bitr4d 270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑝 ∈ 𝑃 ∃𝑘 ∈ 𝐾 𝑥 = (𝑝↑𝑘) ↔ (Λ‘𝑥) ≠ 0)) |
145 | 125, 144 | syl5bb 271 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)) ↔ (Λ‘𝑥) ≠ 0)) |
146 | 145 | necon2bbid 2825 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Λ‘𝑥) = 0 ↔ ¬ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)))) |
147 | 146 | pm5.32da 671 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ (Λ‘𝑥) = 0) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))))) |
148 | | fsumvma.7 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (Λ‘𝑥) = 0)) → 𝐵 = 0) |
149 | 148 | ex 449 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ (Λ‘𝑥) = 0) → 𝐵 = 0)) |
150 | 147, 149 | sylbird 249 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → 𝐵 = 0)) |
151 | 121, 150 | syl5bi 231 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))) → 𝐵 = 0)) |
152 | 151 | imp 444 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎)))) → 𝐵 = 0) |
153 | 110, 120,
152, 12 | fsumss 14303 |
. 2
⊢ (𝜑 → Σ𝑥 ∈ ran (𝑎 ∈ ∪
𝑝 ∈ 𝑃 ({𝑝} × 𝐾) ↦ (↑‘𝑎))𝐵 = Σ𝑥 ∈ 𝐴 𝐵) |
154 | 44, 118, 153 | 3eqtr2rd 2651 |
1
⊢ (𝜑 → Σ𝑥 ∈ 𝐴 𝐵 = Σ𝑝 ∈ 𝑃 Σ𝑘 ∈ 𝐾 𝐶) |