Step | Hyp | Ref
| Expression |
1 | | sumeq1 11318 |
. . . 4
⊢ (𝑤 = ∅ → Σ𝑘 ∈ 𝑤 𝐵 = Σ𝑘 ∈ ∅ 𝐵) |
2 | 1 | fveq2d 5500 |
. . 3
⊢ (𝑤 = ∅ → (𝐹‘Σ𝑘 ∈ 𝑤 𝐵) = (𝐹‘Σ𝑘 ∈ ∅ 𝐵)) |
3 | | sumeq1 11318 |
. . 3
⊢ (𝑤 = ∅ → Σ𝑘 ∈ 𝑤 (𝐹‘𝐵) = Σ𝑘 ∈ ∅ (𝐹‘𝐵)) |
4 | 2, 3 | eqeq12d 2185 |
. 2
⊢ (𝑤 = ∅ → ((𝐹‘Σ𝑘 ∈ 𝑤 𝐵) = Σ𝑘 ∈ 𝑤 (𝐹‘𝐵) ↔ (𝐹‘Σ𝑘 ∈ ∅ 𝐵) = Σ𝑘 ∈ ∅ (𝐹‘𝐵))) |
5 | | sumeq1 11318 |
. . . 4
⊢ (𝑤 = 𝑢 → Σ𝑘 ∈ 𝑤 𝐵 = Σ𝑘 ∈ 𝑢 𝐵) |
6 | 5 | fveq2d 5500 |
. . 3
⊢ (𝑤 = 𝑢 → (𝐹‘Σ𝑘 ∈ 𝑤 𝐵) = (𝐹‘Σ𝑘 ∈ 𝑢 𝐵)) |
7 | | sumeq1 11318 |
. . 3
⊢ (𝑤 = 𝑢 → Σ𝑘 ∈ 𝑤 (𝐹‘𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) |
8 | 6, 7 | eqeq12d 2185 |
. 2
⊢ (𝑤 = 𝑢 → ((𝐹‘Σ𝑘 ∈ 𝑤 𝐵) = Σ𝑘 ∈ 𝑤 (𝐹‘𝐵) ↔ (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵))) |
9 | | sumeq1 11318 |
. . . 4
⊢ (𝑤 = (𝑢 ∪ {𝑣}) → Σ𝑘 ∈ 𝑤 𝐵 = Σ𝑘 ∈ (𝑢 ∪ {𝑣})𝐵) |
10 | 9 | fveq2d 5500 |
. . 3
⊢ (𝑤 = (𝑢 ∪ {𝑣}) → (𝐹‘Σ𝑘 ∈ 𝑤 𝐵) = (𝐹‘Σ𝑘 ∈ (𝑢 ∪ {𝑣})𝐵)) |
11 | | sumeq1 11318 |
. . 3
⊢ (𝑤 = (𝑢 ∪ {𝑣}) → Σ𝑘 ∈ 𝑤 (𝐹‘𝐵) = Σ𝑘 ∈ (𝑢 ∪ {𝑣})(𝐹‘𝐵)) |
12 | 10, 11 | eqeq12d 2185 |
. 2
⊢ (𝑤 = (𝑢 ∪ {𝑣}) → ((𝐹‘Σ𝑘 ∈ 𝑤 𝐵) = Σ𝑘 ∈ 𝑤 (𝐹‘𝐵) ↔ (𝐹‘Σ𝑘 ∈ (𝑢 ∪ {𝑣})𝐵) = Σ𝑘 ∈ (𝑢 ∪ {𝑣})(𝐹‘𝐵))) |
13 | | sumeq1 11318 |
. . . 4
⊢ (𝑤 = 𝐴 → Σ𝑘 ∈ 𝑤 𝐵 = Σ𝑘 ∈ 𝐴 𝐵) |
14 | 13 | fveq2d 5500 |
. . 3
⊢ (𝑤 = 𝐴 → (𝐹‘Σ𝑘 ∈ 𝑤 𝐵) = (𝐹‘Σ𝑘 ∈ 𝐴 𝐵)) |
15 | | sumeq1 11318 |
. . 3
⊢ (𝑤 = 𝐴 → Σ𝑘 ∈ 𝑤 (𝐹‘𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵)) |
16 | 14, 15 | eqeq12d 2185 |
. 2
⊢ (𝑤 = 𝐴 → ((𝐹‘Σ𝑘 ∈ 𝑤 𝐵) = Σ𝑘 ∈ 𝑤 (𝐹‘𝐵) ↔ (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵))) |
17 | | 0cn 7912 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
18 | | fsumrelem.3 |
. . . . . . . . 9
⊢ 𝐹:ℂ⟶ℂ |
19 | 18 | ffvelrni 5630 |
. . . . . . . 8
⊢ (0 ∈
ℂ → (𝐹‘0)
∈ ℂ) |
20 | 17, 19 | ax-mp 5 |
. . . . . . 7
⊢ (𝐹‘0) ∈
ℂ |
21 | 20 | addid1i 8061 |
. . . . . 6
⊢ ((𝐹‘0) + 0) = (𝐹‘0) |
22 | | fvoveq1 5876 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(0 + 𝑦))) |
23 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (𝐹‘𝑥) = (𝐹‘0)) |
24 | 23 | oveq1d 5868 |
. . . . . . . . 9
⊢ (𝑥 = 0 → ((𝐹‘𝑥) + (𝐹‘𝑦)) = ((𝐹‘0) + (𝐹‘𝑦))) |
25 | 22, 24 | eqeq12d 2185 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) + (𝐹‘𝑦)) ↔ (𝐹‘(0 + 𝑦)) = ((𝐹‘0) + (𝐹‘𝑦)))) |
26 | | oveq2 5861 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → (0 + 𝑦) = (0 + 0)) |
27 | | 00id 8060 |
. . . . . . . . . . 11
⊢ (0 + 0) =
0 |
28 | 26, 27 | eqtrdi 2219 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (0 + 𝑦) = 0) |
29 | 28 | fveq2d 5500 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (𝐹‘(0 + 𝑦)) = (𝐹‘0)) |
30 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (𝐹‘𝑦) = (𝐹‘0)) |
31 | 30 | oveq2d 5869 |
. . . . . . . . 9
⊢ (𝑦 = 0 → ((𝐹‘0) + (𝐹‘𝑦)) = ((𝐹‘0) + (𝐹‘0))) |
32 | 29, 31 | eqeq12d 2185 |
. . . . . . . 8
⊢ (𝑦 = 0 → ((𝐹‘(0 + 𝑦)) = ((𝐹‘0) + (𝐹‘𝑦)) ↔ (𝐹‘0) = ((𝐹‘0) + (𝐹‘0)))) |
33 | | fsumrelem.4 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) + (𝐹‘𝑦))) |
34 | 25, 32, 33 | vtocl2ga 2798 |
. . . . . . 7
⊢ ((0
∈ ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) = ((𝐹‘0) + (𝐹‘0))) |
35 | 17, 17, 34 | mp2an 424 |
. . . . . 6
⊢ (𝐹‘0) = ((𝐹‘0) + (𝐹‘0)) |
36 | 21, 35 | eqtr2i 2192 |
. . . . 5
⊢ ((𝐹‘0) + (𝐹‘0)) = ((𝐹‘0) + 0) |
37 | 20, 20, 17 | addcani 8101 |
. . . . 5
⊢ (((𝐹‘0) + (𝐹‘0)) = ((𝐹‘0) + 0) ↔ (𝐹‘0) = 0) |
38 | 36, 37 | mpbi 144 |
. . . 4
⊢ (𝐹‘0) = 0 |
39 | | sum0 11351 |
. . . . 5
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 |
40 | 39 | fveq2i 5499 |
. . . 4
⊢ (𝐹‘Σ𝑘 ∈ ∅ 𝐵) = (𝐹‘0) |
41 | | sum0 11351 |
. . . 4
⊢
Σ𝑘 ∈
∅ (𝐹‘𝐵) = 0 |
42 | 38, 40, 41 | 3eqtr4i 2201 |
. . 3
⊢ (𝐹‘Σ𝑘 ∈ ∅ 𝐵) = Σ𝑘 ∈ ∅ (𝐹‘𝐵) |
43 | 42 | a1i 9 |
. 2
⊢ (𝜑 → (𝐹‘Σ𝑘 ∈ ∅ 𝐵) = Σ𝑘 ∈ ∅ (𝐹‘𝐵)) |
44 | | nfv 1521 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) |
45 | | nfcsb1v 3082 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑣 / 𝑘⦌𝐵 |
46 | | simplr 525 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → 𝑢 ∈ Fin) |
47 | | vex 2733 |
. . . . . . . . 9
⊢ 𝑣 ∈ V |
48 | 47 | a1i 9 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → 𝑣 ∈ V) |
49 | | simprr 527 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → 𝑣 ∈ (𝐴 ∖ 𝑢)) |
50 | 49 | eldifbd 3133 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → ¬ 𝑣 ∈ 𝑢) |
51 | | simplll 528 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ 𝑘 ∈ 𝑢) → 𝜑) |
52 | | simprl 526 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → 𝑢 ⊆ 𝐴) |
53 | 52 | sselda 3147 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ 𝑘 ∈ 𝑢) → 𝑘 ∈ 𝐴) |
54 | | fsumre.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
55 | 51, 53, 54 | syl2anc 409 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ 𝑘 ∈ 𝑢) → 𝐵 ∈ ℂ) |
56 | | csbeq1a 3058 |
. . . . . . . 8
⊢ (𝑘 = 𝑣 → 𝐵 = ⦋𝑣 / 𝑘⦌𝐵) |
57 | 49 | eldifad 3132 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → 𝑣 ∈ 𝐴) |
58 | 54 | ralrimiva 2543 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
59 | 58 | ad2antrr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
60 | 45 | nfel1 2323 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑣 / 𝑘⦌𝐵 ∈ ℂ |
61 | 56 | eleq1d 2239 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑣 → (𝐵 ∈ ℂ ↔ ⦋𝑣 / 𝑘⦌𝐵 ∈ ℂ)) |
62 | 60, 61 | rspc 2828 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑣 / 𝑘⦌𝐵 ∈ ℂ)) |
63 | 57, 59, 62 | sylc 62 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → ⦋𝑣 / 𝑘⦌𝐵 ∈ ℂ) |
64 | 44, 45, 46, 48, 50, 55, 56, 63 | fsumsplitsn 11373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → Σ𝑘 ∈ (𝑢 ∪ {𝑣})𝐵 = (Σ𝑘 ∈ 𝑢 𝐵 + ⦋𝑣 / 𝑘⦌𝐵)) |
65 | 64 | adantr 274 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) → Σ𝑘 ∈ (𝑢 ∪ {𝑣})𝐵 = (Σ𝑘 ∈ 𝑢 𝐵 + ⦋𝑣 / 𝑘⦌𝐵)) |
66 | 65 | fveq2d 5500 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) → (𝐹‘Σ𝑘 ∈ (𝑢 ∪ {𝑣})𝐵) = (𝐹‘(Σ𝑘 ∈ 𝑢 𝐵 + ⦋𝑣 / 𝑘⦌𝐵))) |
67 | 46, 55 | fsumcl 11363 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → Σ𝑘 ∈ 𝑢 𝐵 ∈ ℂ) |
68 | 67 | adantr 274 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) → Σ𝑘 ∈ 𝑢 𝐵 ∈ ℂ) |
69 | 63 | adantr 274 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) → ⦋𝑣 / 𝑘⦌𝐵 ∈ ℂ) |
70 | | fvoveq1 5876 |
. . . . . . . 8
⊢ (𝑥 = Σ𝑘 ∈ 𝑢 𝐵 → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(Σ𝑘 ∈ 𝑢 𝐵 + 𝑦))) |
71 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑥 = Σ𝑘 ∈ 𝑢 𝐵 → (𝐹‘𝑥) = (𝐹‘Σ𝑘 ∈ 𝑢 𝐵)) |
72 | 71 | oveq1d 5868 |
. . . . . . . 8
⊢ (𝑥 = Σ𝑘 ∈ 𝑢 𝐵 → ((𝐹‘𝑥) + (𝐹‘𝑦)) = ((𝐹‘Σ𝑘 ∈ 𝑢 𝐵) + (𝐹‘𝑦))) |
73 | 70, 72 | eqeq12d 2185 |
. . . . . . 7
⊢ (𝑥 = Σ𝑘 ∈ 𝑢 𝐵 → ((𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) + (𝐹‘𝑦)) ↔ (𝐹‘(Σ𝑘 ∈ 𝑢 𝐵 + 𝑦)) = ((𝐹‘Σ𝑘 ∈ 𝑢 𝐵) + (𝐹‘𝑦)))) |
74 | | oveq2 5861 |
. . . . . . . . 9
⊢ (𝑦 = ⦋𝑣 / 𝑘⦌𝐵 → (Σ𝑘 ∈ 𝑢 𝐵 + 𝑦) = (Σ𝑘 ∈ 𝑢 𝐵 + ⦋𝑣 / 𝑘⦌𝐵)) |
75 | 74 | fveq2d 5500 |
. . . . . . . 8
⊢ (𝑦 = ⦋𝑣 / 𝑘⦌𝐵 → (𝐹‘(Σ𝑘 ∈ 𝑢 𝐵 + 𝑦)) = (𝐹‘(Σ𝑘 ∈ 𝑢 𝐵 + ⦋𝑣 / 𝑘⦌𝐵))) |
76 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑦 = ⦋𝑣 / 𝑘⦌𝐵 → (𝐹‘𝑦) = (𝐹‘⦋𝑣 / 𝑘⦌𝐵)) |
77 | 76 | oveq2d 5869 |
. . . . . . . 8
⊢ (𝑦 = ⦋𝑣 / 𝑘⦌𝐵 → ((𝐹‘Σ𝑘 ∈ 𝑢 𝐵) + (𝐹‘𝑦)) = ((𝐹‘Σ𝑘 ∈ 𝑢 𝐵) + (𝐹‘⦋𝑣 / 𝑘⦌𝐵))) |
78 | 75, 77 | eqeq12d 2185 |
. . . . . . 7
⊢ (𝑦 = ⦋𝑣 / 𝑘⦌𝐵 → ((𝐹‘(Σ𝑘 ∈ 𝑢 𝐵 + 𝑦)) = ((𝐹‘Σ𝑘 ∈ 𝑢 𝐵) + (𝐹‘𝑦)) ↔ (𝐹‘(Σ𝑘 ∈ 𝑢 𝐵 + ⦋𝑣 / 𝑘⦌𝐵)) = ((𝐹‘Σ𝑘 ∈ 𝑢 𝐵) + (𝐹‘⦋𝑣 / 𝑘⦌𝐵)))) |
79 | 73, 78, 33 | vtocl2ga 2798 |
. . . . . 6
⊢
((Σ𝑘 ∈
𝑢 𝐵 ∈ ℂ ∧ ⦋𝑣 / 𝑘⦌𝐵 ∈ ℂ) → (𝐹‘(Σ𝑘 ∈ 𝑢 𝐵 + ⦋𝑣 / 𝑘⦌𝐵)) = ((𝐹‘Σ𝑘 ∈ 𝑢 𝐵) + (𝐹‘⦋𝑣 / 𝑘⦌𝐵))) |
80 | 68, 69, 79 | syl2anc 409 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) → (𝐹‘(Σ𝑘 ∈ 𝑢 𝐵 + ⦋𝑣 / 𝑘⦌𝐵)) = ((𝐹‘Σ𝑘 ∈ 𝑢 𝐵) + (𝐹‘⦋𝑣 / 𝑘⦌𝐵))) |
81 | | simpr 109 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) → (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) |
82 | 81 | oveq1d 5868 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) → ((𝐹‘Σ𝑘 ∈ 𝑢 𝐵) + (𝐹‘⦋𝑣 / 𝑘⦌𝐵)) = (Σ𝑘 ∈ 𝑢 (𝐹‘𝐵) + (𝐹‘⦋𝑣 / 𝑘⦌𝐵))) |
83 | 66, 80, 82 | 3eqtrd 2207 |
. . . 4
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) → (𝐹‘Σ𝑘 ∈ (𝑢 ∪ {𝑣})𝐵) = (Σ𝑘 ∈ 𝑢 (𝐹‘𝐵) + (𝐹‘⦋𝑣 / 𝑘⦌𝐵))) |
84 | | nfcv 2312 |
. . . . . . 7
⊢
Ⅎ𝑘𝐹 |
85 | 84, 45 | nffv 5506 |
. . . . . 6
⊢
Ⅎ𝑘(𝐹‘⦋𝑣 / 𝑘⦌𝐵) |
86 | 18 | a1i 9 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ 𝑘 ∈ 𝑢) → 𝐹:ℂ⟶ℂ) |
87 | 86, 55 | ffvelrnd 5632 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ 𝑘 ∈ 𝑢) → (𝐹‘𝐵) ∈ ℂ) |
88 | 56 | fveq2d 5500 |
. . . . . 6
⊢ (𝑘 = 𝑣 → (𝐹‘𝐵) = (𝐹‘⦋𝑣 / 𝑘⦌𝐵)) |
89 | 18 | a1i 9 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → 𝐹:ℂ⟶ℂ) |
90 | 89, 63 | ffvelrnd 5632 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → (𝐹‘⦋𝑣 / 𝑘⦌𝐵) ∈ ℂ) |
91 | 44, 85, 46, 48, 50, 87, 88, 90 | fsumsplitsn 11373 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → Σ𝑘 ∈ (𝑢 ∪ {𝑣})(𝐹‘𝐵) = (Σ𝑘 ∈ 𝑢 (𝐹‘𝐵) + (𝐹‘⦋𝑣 / 𝑘⦌𝐵))) |
92 | 91 | adantr 274 |
. . . 4
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) → Σ𝑘 ∈ (𝑢 ∪ {𝑣})(𝐹‘𝐵) = (Σ𝑘 ∈ 𝑢 (𝐹‘𝐵) + (𝐹‘⦋𝑣 / 𝑘⦌𝐵))) |
93 | 83, 92 | eqtr4d 2206 |
. . 3
⊢ ((((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) ∧ (𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵)) → (𝐹‘Σ𝑘 ∈ (𝑢 ∪ {𝑣})𝐵) = Σ𝑘 ∈ (𝑢 ∪ {𝑣})(𝐹‘𝐵)) |
94 | 93 | ex 114 |
. 2
⊢ (((𝜑 ∧ 𝑢 ∈ Fin) ∧ (𝑢 ⊆ 𝐴 ∧ 𝑣 ∈ (𝐴 ∖ 𝑢))) → ((𝐹‘Σ𝑘 ∈ 𝑢 𝐵) = Σ𝑘 ∈ 𝑢 (𝐹‘𝐵) → (𝐹‘Σ𝑘 ∈ (𝑢 ∪ {𝑣})𝐵) = Σ𝑘 ∈ (𝑢 ∪ {𝑣})(𝐹‘𝐵))) |
95 | | fsumre.1 |
. 2
⊢ (𝜑 → 𝐴 ∈ Fin) |
96 | 4, 8, 12, 16, 43, 94, 95 | findcard2sd 6870 |
1
⊢ (𝜑 → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵)) |