Step | Hyp | Ref
| Expression |
1 | | ssid 3848 |
. 2
⊢ 𝐵 ⊆ 𝐵 |
2 | | fsumrlim.2 |
. . 3
⊢ (𝜑 → 𝐵 ∈ Fin) |
3 | | sseq1 3851 |
. . . . . 6
⊢ (𝑤 = ∅ → (𝑤 ⊆ 𝐵 ↔ ∅ ⊆ 𝐵)) |
4 | | sumeq1 14796 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → Σ𝑘 ∈ 𝑤 𝐶 = Σ𝑘 ∈ ∅ 𝐶) |
5 | | sum0 14829 |
. . . . . . . . 9
⊢
Σ𝑘 ∈
∅ 𝐶 =
0 |
6 | 4, 5 | syl6eq 2877 |
. . . . . . . 8
⊢ (𝑤 = ∅ → Σ𝑘 ∈ 𝑤 𝐶 = 0) |
7 | 6 | mpteq2dv 4968 |
. . . . . . 7
⊢ (𝑤 = ∅ → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ 0)) |
8 | | sumeq1 14796 |
. . . . . . . 8
⊢ (𝑤 = ∅ → Σ𝑘 ∈ 𝑤 𝐷 = Σ𝑘 ∈ ∅ 𝐷) |
9 | | sum0 14829 |
. . . . . . . 8
⊢
Σ𝑘 ∈
∅ 𝐷 =
0 |
10 | 8, 9 | syl6eq 2877 |
. . . . . . 7
⊢ (𝑤 = ∅ → Σ𝑘 ∈ 𝑤 𝐷 = 0) |
11 | 7, 10 | breq12d 4886 |
. . . . . 6
⊢ (𝑤 = ∅ → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷 ↔ (𝑥 ∈ 𝐴 ↦ 0) ⇝𝑟
0)) |
12 | 3, 11 | imbi12d 336 |
. . . . 5
⊢ (𝑤 = ∅ → ((𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷) ↔ (∅ ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 0) ⇝𝑟
0))) |
13 | 12 | imbi2d 332 |
. . . 4
⊢ (𝑤 = ∅ → ((𝜑 → (𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷)) ↔ (𝜑 → (∅ ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 0) ⇝𝑟
0)))) |
14 | | sseq1 3851 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (𝑤 ⊆ 𝐵 ↔ 𝑦 ⊆ 𝐵)) |
15 | | sumeq1 14796 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → Σ𝑘 ∈ 𝑤 𝐶 = Σ𝑘 ∈ 𝑦 𝐶) |
16 | 15 | mpteq2dv 4968 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶)) |
17 | | sumeq1 14796 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → Σ𝑘 ∈ 𝑤 𝐷 = Σ𝑘 ∈ 𝑦 𝐷) |
18 | 16, 17 | breq12d 4886 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷 ↔ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷)) |
19 | 14, 18 | imbi12d 336 |
. . . . 5
⊢ (𝑤 = 𝑦 → ((𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷) ↔ (𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷))) |
20 | 19 | imbi2d 332 |
. . . 4
⊢ (𝑤 = 𝑦 → ((𝜑 → (𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷)) ↔ (𝜑 → (𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷)))) |
21 | | sseq1 3851 |
. . . . . 6
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤 ⊆ 𝐵 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) |
22 | | sumeq1 14796 |
. . . . . . . 8
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → Σ𝑘 ∈ 𝑤 𝐶 = Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) |
23 | 22 | mpteq2dv 4968 |
. . . . . . 7
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶)) |
24 | | sumeq1 14796 |
. . . . . . 7
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → Σ𝑘 ∈ 𝑤 𝐷 = Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷) |
25 | 23, 24 | breq12d 4886 |
. . . . . 6
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷 ↔ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)) |
26 | 21, 25 | imbi12d 336 |
. . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷))) |
27 | 26 | imbi2d 332 |
. . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝜑 → (𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷)) ↔ (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)))) |
28 | | sseq1 3851 |
. . . . . 6
⊢ (𝑤 = 𝐵 → (𝑤 ⊆ 𝐵 ↔ 𝐵 ⊆ 𝐵)) |
29 | | sumeq1 14796 |
. . . . . . . 8
⊢ (𝑤 = 𝐵 → Σ𝑘 ∈ 𝑤 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) |
30 | 29 | mpteq2dv 4968 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶)) |
31 | | sumeq1 14796 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → Σ𝑘 ∈ 𝑤 𝐷 = Σ𝑘 ∈ 𝐵 𝐷) |
32 | 30, 31 | breq12d 4886 |
. . . . . 6
⊢ (𝑤 = 𝐵 → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷 ↔ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝐵 𝐷)) |
33 | 28, 32 | imbi12d 336 |
. . . . 5
⊢ (𝑤 = 𝐵 → ((𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷) ↔ (𝐵 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝐵 𝐷))) |
34 | 33 | imbi2d 332 |
. . . 4
⊢ (𝑤 = 𝐵 → ((𝜑 → (𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑤 𝐷)) ↔ (𝜑 → (𝐵 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝐵 𝐷)))) |
35 | | fsumrlim.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
36 | | 0cn 10348 |
. . . . . 6
⊢ 0 ∈
ℂ |
37 | | rlimconst 14652 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 0 ∈
ℂ) → (𝑥 ∈
𝐴 ↦ 0)
⇝𝑟 0) |
38 | 35, 36, 37 | sylancl 580 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 0) ⇝𝑟
0) |
39 | 38 | a1d 25 |
. . . 4
⊢ (𝜑 → (∅ ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 0) ⇝𝑟
0)) |
40 | | ssun1 4003 |
. . . . . . . . . 10
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
41 | | sstr 3835 |
. . . . . . . . . 10
⊢ ((𝑦 ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵) → 𝑦 ⊆ 𝐵) |
42 | 40, 41 | mpan 681 |
. . . . . . . . 9
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → 𝑦 ⊆ 𝐵) |
43 | 42 | imim1i 63 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷)) |
44 | | sumex 14795 |
. . . . . . . . . . . . . 14
⊢
Σ𝑘 ∈
𝑦 ⦋𝑤 / 𝑥⦌𝐶 ∈ V |
45 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) ∧ 𝑤 ∈ 𝐴) → Σ𝑘 ∈ 𝑦 ⦋𝑤 / 𝑥⦌𝐶 ∈ V) |
46 | | simprr 789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦 ∪ {𝑧}) ⊆ 𝐵) |
47 | 46 | unssbd 4018 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → {𝑧} ⊆ 𝐵) |
48 | | vex 3417 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑧 ∈ V |
49 | 48 | snss 4535 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝐵 ↔ {𝑧} ⊆ 𝐵) |
50 | 47, 49 | sylibr 226 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → 𝑧 ∈ 𝐵) |
51 | 50 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐵) |
52 | | fsumrlim.3 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ 𝑉) |
53 | 52 | anass1rs 645 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
54 | | fsumrlim.4 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷) |
55 | 53, 54 | rlimmptrcl 14715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
56 | 55 | an32s 642 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
57 | 56 | adantllr 710 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
58 | 57 | ralrimiva 3175 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ) |
59 | | nfcsb1v 3773 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐶 |
60 | 59 | nfel1 2984 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ |
61 | | csbeq1a 3766 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑧 → 𝐶 = ⦋𝑧 / 𝑘⦌𝐶) |
62 | 61 | eleq1d 2891 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑧 → (𝐶 ∈ ℂ ↔ ⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ)) |
63 | 60, 62 | rspc 3520 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝐵 → (∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ → ⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ)) |
64 | 51, 58, 63 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ) |
65 | 64 | ralrimiva 3175 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ∀𝑥 ∈ 𝐴 ⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ) |
66 | 65 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → ∀𝑥 ∈ 𝐴 ⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ) |
67 | | nfcsb1v 3773 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶 |
68 | 67 | nfel1 2984 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ |
69 | | csbeq1a 3766 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑤 → ⦋𝑧 / 𝑘⦌𝐶 = ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶) |
70 | 69 | eleq1d 2891 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑤 → (⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ ↔ ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ)) |
71 | 68, 70 | rspc 3520 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ → ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ)) |
72 | 66, 71 | mpan9 502 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ) |
73 | | elex 3429 |
. . . . . . . . . . . . . 14
⊢
(⦋𝑤 /
𝑥⦌⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ → ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶 ∈ V) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶 ∈ V) |
75 | | nfcv 2969 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑤Σ𝑘 ∈ 𝑦 𝐶 |
76 | | nfcv 2969 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥𝑦 |
77 | | nfcsb1v 3773 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐶 |
78 | 76, 77 | nfsum 14798 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥Σ𝑘 ∈ 𝑦 ⦋𝑤 / 𝑥⦌𝐶 |
79 | | csbeq1a 3766 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑤 → 𝐶 = ⦋𝑤 / 𝑥⦌𝐶) |
80 | 79 | sumeq2sdv 14812 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → Σ𝑘 ∈ 𝑦 𝐶 = Σ𝑘 ∈ 𝑦 ⦋𝑤 / 𝑥⦌𝐶) |
81 | 75, 78, 80 | cbvmpt 4972 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) = (𝑤 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 ⦋𝑤 / 𝑥⦌𝐶) |
82 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) |
83 | 81, 82 | syl5eqbrr 4909 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → (𝑤 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 ⦋𝑤 / 𝑥⦌𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) |
84 | | nfcv 2969 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑤⦋𝑧 / 𝑘⦌𝐶 |
85 | 84, 67, 69 | cbvmpt 4972 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) = (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶) |
86 | 54 | ralrimiva 3175 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑘 ∈ 𝐵 (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷) |
87 | 86 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ∀𝑘 ∈ 𝐵 (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷) |
88 | | nfcv 2969 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑘𝐴 |
89 | 88, 59 | nfmpt 4969 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘(𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) |
90 | | nfcv 2969 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘
⇝𝑟 |
91 | | nfcsb1v 3773 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐷 |
92 | 89, 90, 91 | nfbr 4920 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘(𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) ⇝𝑟
⦋𝑧 / 𝑘⦌𝐷 |
93 | 61 | mpteq2dv 4968 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑧 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶)) |
94 | | csbeq1a 3766 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑧 → 𝐷 = ⦋𝑧 / 𝑘⦌𝐷) |
95 | 93, 94 | breq12d 4886 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷 ↔ (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) ⇝𝑟
⦋𝑧 / 𝑘⦌𝐷)) |
96 | 92, 95 | rspc 3520 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝐵 → (∀𝑘 ∈ 𝐵 (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷 → (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) ⇝𝑟
⦋𝑧 / 𝑘⦌𝐷)) |
97 | 50, 87, 96 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) ⇝𝑟
⦋𝑧 / 𝑘⦌𝐷) |
98 | 97 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) ⇝𝑟
⦋𝑧 / 𝑘⦌𝐷) |
99 | 85, 98 | syl5eqbrr 4909 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶) ⇝𝑟
⦋𝑧 / 𝑘⦌𝐷) |
100 | 45, 74, 83, 99 | rlimadd 14750 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → (𝑤 ∈ 𝐴 ↦ (Σ𝑘 ∈ 𝑦 ⦋𝑤 / 𝑥⦌𝐶 + ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶)) ⇝𝑟 (Σ𝑘 ∈ 𝑦 𝐷 + ⦋𝑧 / 𝑘⦌𝐷)) |
101 | | simprl 787 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ¬ 𝑧 ∈ 𝑦) |
102 | | disjsn 4465 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
103 | 101, 102 | sylibr 226 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦 ∩ {𝑧}) = ∅) |
104 | 103 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∩ {𝑧}) = ∅) |
105 | | eqidd 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧})) |
106 | 2 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → 𝐵 ∈ Fin) |
107 | | ssfi 8449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵) → (𝑦 ∪ {𝑧}) ∈ Fin) |
108 | 106, 46, 107 | syl2anc 579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦 ∪ {𝑧}) ∈ Fin) |
109 | 108 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∪ {𝑧}) ∈ Fin) |
110 | 46 | sselda 3827 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑘 ∈ 𝐵) |
111 | 110 | adantlr 706 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑘 ∈ 𝐵) |
112 | 111, 57 | syldan 585 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝐶 ∈ ℂ) |
113 | 104, 105,
109, 112 | fsumsplit 14848 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶 = (Σ𝑘 ∈ 𝑦 𝐶 + Σ𝑘 ∈ {𝑧}𝐶)) |
114 | | nfcv 2969 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑤𝐶 |
115 | | nfcsb1v 3773 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑘⦋𝑤 / 𝑘⦌𝐶 |
116 | | csbeq1a 3766 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑤 → 𝐶 = ⦋𝑤 / 𝑘⦌𝐶) |
117 | 114, 115,
116 | cbvsumi 14804 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ𝑘 ∈
{𝑧}𝐶 = Σ𝑤 ∈ {𝑧}⦋𝑤 / 𝑘⦌𝐶 |
118 | | csbeq1 3760 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑧 → ⦋𝑤 / 𝑘⦌𝐶 = ⦋𝑧 / 𝑘⦌𝐶) |
119 | 118 | sumsn 14852 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝐵 ∧ ⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ) → Σ𝑤 ∈ {𝑧}⦋𝑤 / 𝑘⦌𝐶 = ⦋𝑧 / 𝑘⦌𝐶) |
120 | 51, 64, 119 | syl2anc 579 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → Σ𝑤 ∈ {𝑧}⦋𝑤 / 𝑘⦌𝐶 = ⦋𝑧 / 𝑘⦌𝐶) |
121 | 117, 120 | syl5eq 2873 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → Σ𝑘 ∈ {𝑧}𝐶 = ⦋𝑧 / 𝑘⦌𝐶) |
122 | 121 | oveq2d 6921 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (Σ𝑘 ∈ 𝑦 𝐶 + Σ𝑘 ∈ {𝑧}𝐶) = (Σ𝑘 ∈ 𝑦 𝐶 + ⦋𝑧 / 𝑘⦌𝐶)) |
123 | 113, 122 | eqtrd 2861 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶 = (Σ𝑘 ∈ 𝑦 𝐶 + ⦋𝑧 / 𝑘⦌𝐶)) |
124 | 123 | mpteq2dva 4967 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) = (𝑥 ∈ 𝐴 ↦ (Σ𝑘 ∈ 𝑦 𝐶 + ⦋𝑧 / 𝑘⦌𝐶))) |
125 | 124 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) = (𝑥 ∈ 𝐴 ↦ (Σ𝑘 ∈ 𝑦 𝐶 + ⦋𝑧 / 𝑘⦌𝐶))) |
126 | | nfcv 2969 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑤(Σ𝑘 ∈ 𝑦 𝐶 + ⦋𝑧 / 𝑘⦌𝐶) |
127 | | nfcv 2969 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥
+ |
128 | 78, 127, 67 | nfov 6935 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(Σ𝑘 ∈ 𝑦 ⦋𝑤 / 𝑥⦌𝐶 + ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶) |
129 | 80, 69 | oveq12d 6923 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (Σ𝑘 ∈ 𝑦 𝐶 + ⦋𝑧 / 𝑘⦌𝐶) = (Σ𝑘 ∈ 𝑦 ⦋𝑤 / 𝑥⦌𝐶 + ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶)) |
130 | 126, 128,
129 | cbvmpt 4972 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 ↦ (Σ𝑘 ∈ 𝑦 𝐶 + ⦋𝑧 / 𝑘⦌𝐶)) = (𝑤 ∈ 𝐴 ↦ (Σ𝑘 ∈ 𝑦 ⦋𝑤 / 𝑥⦌𝐶 + ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶)) |
131 | 125, 130 | syl6eq 2877 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) = (𝑤 ∈ 𝐴 ↦ (Σ𝑘 ∈ 𝑦 ⦋𝑤 / 𝑥⦌𝐶 + ⦋𝑤 / 𝑥⦌⦋𝑧 / 𝑘⦌𝐶))) |
132 | | eqidd 2826 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧})) |
133 | | rlimcl 14611 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷 → 𝐷 ∈ ℂ) |
134 | 54, 133 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐷 ∈ ℂ) |
135 | 134 | adantlr 706 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑘 ∈ 𝐵) → 𝐷 ∈ ℂ) |
136 | 110, 135 | syldan 585 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝐷 ∈ ℂ) |
137 | 103, 132,
108, 136 | fsumsplit 14848 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷 = (Σ𝑘 ∈ 𝑦 𝐷 + Σ𝑘 ∈ {𝑧}𝐷)) |
138 | | nfcv 2969 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑤𝐷 |
139 | | nfcsb1v 3773 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘⦋𝑤 / 𝑘⦌𝐷 |
140 | | csbeq1a 3766 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑤 → 𝐷 = ⦋𝑤 / 𝑘⦌𝐷) |
141 | 138, 139,
140 | cbvsumi 14804 |
. . . . . . . . . . . . . . . 16
⊢
Σ𝑘 ∈
{𝑧}𝐷 = Σ𝑤 ∈ {𝑧}⦋𝑤 / 𝑘⦌𝐷 |
142 | 135 | ralrimiva 3175 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ∀𝑘 ∈ 𝐵 𝐷 ∈ ℂ) |
143 | 91 | nfel1 2984 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐷 ∈ ℂ |
144 | 94 | eleq1d 2891 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑧 → (𝐷 ∈ ℂ ↔ ⦋𝑧 / 𝑘⦌𝐷 ∈ ℂ)) |
145 | 143, 144 | rspc 3520 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝐵 → (∀𝑘 ∈ 𝐵 𝐷 ∈ ℂ → ⦋𝑧 / 𝑘⦌𝐷 ∈ ℂ)) |
146 | 50, 142, 145 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ⦋𝑧 / 𝑘⦌𝐷 ∈ ℂ) |
147 | | csbeq1 3760 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → ⦋𝑤 / 𝑘⦌𝐷 = ⦋𝑧 / 𝑘⦌𝐷) |
148 | 147 | sumsn 14852 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝐵 ∧ ⦋𝑧 / 𝑘⦌𝐷 ∈ ℂ) → Σ𝑤 ∈ {𝑧}⦋𝑤 / 𝑘⦌𝐷 = ⦋𝑧 / 𝑘⦌𝐷) |
149 | 50, 146, 148 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → Σ𝑤 ∈ {𝑧}⦋𝑤 / 𝑘⦌𝐷 = ⦋𝑧 / 𝑘⦌𝐷) |
150 | 141, 149 | syl5eq 2873 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → Σ𝑘 ∈ {𝑧}𝐷 = ⦋𝑧 / 𝑘⦌𝐷) |
151 | 150 | oveq2d 6921 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (Σ𝑘 ∈ 𝑦 𝐷 + Σ𝑘 ∈ {𝑧}𝐷) = (Σ𝑘 ∈ 𝑦 𝐷 + ⦋𝑧 / 𝑘⦌𝐷)) |
152 | 137, 151 | eqtrd 2861 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷 = (Σ𝑘 ∈ 𝑦 𝐷 + ⦋𝑧 / 𝑘⦌𝐷)) |
153 | 152 | adantr 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷 = (Σ𝑘 ∈ 𝑦 𝐷 + ⦋𝑧 / 𝑘⦌𝐷)) |
154 | 100, 131,
153 | 3brtr4d 4905 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷) |
155 | 154 | ex 403 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)) |
156 | 155 | expr 450 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷))) |
157 | 156 | a2d 29 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑧 ∈ 𝑦) → (((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷))) |
158 | 43, 157 | syl5 34 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷))) |
159 | 158 | expcom 404 |
. . . . . 6
⊢ (¬
𝑧 ∈ 𝑦 → (𝜑 → ((𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)))) |
160 | 159 | a2d 29 |
. . . . 5
⊢ (¬
𝑧 ∈ 𝑦 → ((𝜑 → (𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷)) → (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)))) |
161 | 160 | adantl 475 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝜑 → (𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝑦 𝐷)) → (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)))) |
162 | 13, 20, 27, 34, 39, 161 | findcard2s 8470 |
. . 3
⊢ (𝐵 ∈ Fin → (𝜑 → (𝐵 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝐵 𝐷))) |
163 | 2, 162 | mpcom 38 |
. 2
⊢ (𝜑 → (𝐵 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝐵 𝐷)) |
164 | 1, 163 | mpi 20 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ⇝𝑟 Σ𝑘 ∈ 𝐵 𝐷) |