Step | Hyp | Ref
| Expression |
1 | | carageniuncllem1.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈ 𝑍) |
2 | | carageniuncllem1.z |
. . . 4
⊢ 𝑍 =
(ℤ≥‘𝑀) |
3 | 1, 2 | syl6eleq 2698 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) |
4 | | eluzfz2 12220 |
. . 3
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝐾 ∈ (𝑀...𝐾)) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝐾)) |
6 | | id 22 |
. 2
⊢ (𝜑 → 𝜑) |
7 | | oveq2 6557 |
. . . . . 6
⊢ (𝑘 = 𝑀 → (𝑀...𝑘) = (𝑀...𝑀)) |
8 | 7 | sumeq1d 14279 |
. . . . 5
⊢ (𝑘 = 𝑀 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹‘𝑛)))) |
9 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝑀 → (𝐺‘𝑘) = (𝐺‘𝑀)) |
10 | 9 | ineq2d 3776 |
. . . . . 6
⊢ (𝑘 = 𝑀 → (𝐴 ∩ (𝐺‘𝑘)) = (𝐴 ∩ (𝐺‘𝑀))) |
11 | 10 | fveq2d 6107 |
. . . . 5
⊢ (𝑘 = 𝑀 → (𝑂‘(𝐴 ∩ (𝐺‘𝑘))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑀)))) |
12 | 8, 11 | eqeq12d 2625 |
. . . 4
⊢ (𝑘 = 𝑀 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑀))))) |
13 | 12 | imbi2d 329 |
. . 3
⊢ (𝑘 = 𝑀 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑀)))))) |
14 | | oveq2 6557 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝑀...𝑘) = (𝑀...𝑗)) |
15 | 14 | sumeq1d 14279 |
. . . . 5
⊢ (𝑘 = 𝑗 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛)))) |
16 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝐺‘𝑘) = (𝐺‘𝑗)) |
17 | 16 | ineq2d 3776 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝐴 ∩ (𝐺‘𝑘)) = (𝐴 ∩ (𝐺‘𝑗))) |
18 | 17 | fveq2d 6107 |
. . . . 5
⊢ (𝑘 = 𝑗 → (𝑂‘(𝐴 ∩ (𝐺‘𝑘))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) |
19 | 15, 18 | eqeq12d 2625 |
. . . 4
⊢ (𝑘 = 𝑗 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗))))) |
20 | 19 | imbi2d 329 |
. . 3
⊢ (𝑘 = 𝑗 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))))) |
21 | | oveq2 6557 |
. . . . . 6
⊢ (𝑘 = (𝑗 + 1) → (𝑀...𝑘) = (𝑀...(𝑗 + 1))) |
22 | 21 | sumeq1d 14279 |
. . . . 5
⊢ (𝑘 = (𝑗 + 1) → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹‘𝑛)))) |
23 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = (𝑗 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑗 + 1))) |
24 | 23 | ineq2d 3776 |
. . . . . 6
⊢ (𝑘 = (𝑗 + 1) → (𝐴 ∩ (𝐺‘𝑘)) = (𝐴 ∩ (𝐺‘(𝑗 + 1)))) |
25 | 24 | fveq2d 6107 |
. . . . 5
⊢ (𝑘 = (𝑗 + 1) → (𝑂‘(𝐴 ∩ (𝐺‘𝑘))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1))))) |
26 | 22, 25 | eqeq12d 2625 |
. . . 4
⊢ (𝑘 = (𝑗 + 1) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑘))) ↔ Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))) |
27 | 26 | imbi2d 329 |
. . 3
⊢ (𝑘 = (𝑗 + 1) → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1))))))) |
28 | | oveq2 6557 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑀...𝑘) = (𝑀...𝐾)) |
29 | 28 | sumeq1d 14279 |
. . . . 5
⊢ (𝑘 = 𝐾 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹‘𝑛)))) |
30 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝐺‘𝑘) = (𝐺‘𝐾)) |
31 | 30 | ineq2d 3776 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝐴 ∩ (𝐺‘𝑘)) = (𝐴 ∩ (𝐺‘𝐾))) |
32 | 31 | fveq2d 6107 |
. . . . 5
⊢ (𝑘 = 𝐾 → (𝑂‘(𝐴 ∩ (𝐺‘𝑘))) = (𝑂‘(𝐴 ∩ (𝐺‘𝐾)))) |
33 | 29, 32 | eqeq12d 2625 |
. . . 4
⊢ (𝑘 = 𝐾 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝐾))))) |
34 | 33 | imbi2d 329 |
. . 3
⊢ (𝑘 = 𝐾 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝐾)))))) |
35 | | eluzel2 11568 |
. . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
36 | 3, 35 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
37 | | fzsn 12254 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
38 | 36, 37 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝑀) = {𝑀}) |
39 | 38 | sumeq1d 14279 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹‘𝑛)))) |
40 | | carageniuncllem1.o |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
41 | | carageniuncllem1.x |
. . . . . . . 8
⊢ 𝑋 = ∪
dom 𝑂 |
42 | | carageniuncllem1.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ 𝑋) |
43 | | carageniuncllem1.re |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ) |
44 | | inss1 3795 |
. . . . . . . . 9
⊢ (𝐴 ∩ (𝐹‘𝑀)) ⊆ 𝐴 |
45 | 44 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∩ (𝐹‘𝑀)) ⊆ 𝐴) |
46 | 40, 41, 42, 43, 45 | omessre 39400 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘(𝐴 ∩ (𝐹‘𝑀))) ∈ ℝ) |
47 | 46 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (𝑂‘(𝐴 ∩ (𝐹‘𝑀))) ∈ ℂ) |
48 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (𝐹‘𝑛) = (𝐹‘𝑀)) |
49 | 48 | ineq2d 3776 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (𝐴 ∩ (𝐹‘𝑛)) = (𝐴 ∩ (𝐹‘𝑀))) |
50 | 49 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐹‘𝑀)))) |
51 | 50 | sumsn 14319 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑂‘(𝐴 ∩ (𝐹‘𝑀))) ∈ ℂ) → Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐹‘𝑀)))) |
52 | 36, 47, 51 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐹‘𝑀)))) |
53 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑂‘(𝐴 ∩ (𝐸‘𝑀))) = (𝑂‘(𝐴 ∩ (𝐸‘𝑀)))) |
54 | | carageniuncllem1.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) |
55 | 54 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖)))) |
56 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑀 → (𝐸‘𝑛) = (𝐸‘𝑀)) |
57 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑀 → (𝑀..^𝑛) = (𝑀..^𝑀)) |
58 | 57 | iuneq1d 4481 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑀 → ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖)) |
59 | 56, 58 | difeq12d 3691 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑀 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝑀) ∖ ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖))) |
60 | 59 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝑀) ∖ ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖))) |
61 | | uzid 11578 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
62 | 36, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
63 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 = (ℤ≥‘𝑀)) |
64 | 63 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (𝜑 →
(ℤ≥‘𝑀) = 𝑍) |
65 | 62, 64 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
66 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝐸‘𝑀) ∈ V |
67 | | difexg 4735 |
. . . . . . . . . . . 12
⊢ ((𝐸‘𝑀) ∈ V → ((𝐸‘𝑀) ∖ ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖)) ∈ V) |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝐸‘𝑀) ∖ ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖)) ∈ V |
69 | 68 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸‘𝑀) ∖ ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖)) ∈ V) |
70 | 55, 60, 65, 69 | fvmptd 6197 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑀) = ((𝐸‘𝑀) ∖ ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖))) |
71 | | fzo0 12361 |
. . . . . . . . . . . . 13
⊢ (𝑀..^𝑀) = ∅ |
72 | | iuneq1 4470 |
. . . . . . . . . . . . 13
⊢ ((𝑀..^𝑀) = ∅ → ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖) = ∪ 𝑖 ∈ ∅ (𝐸‘𝑖)) |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖) = ∪ 𝑖 ∈ ∅ (𝐸‘𝑖) |
74 | | 0iun 4513 |
. . . . . . . . . . . 12
⊢ ∪ 𝑖 ∈ ∅ (𝐸‘𝑖) = ∅ |
75 | 73, 74 | eqtri 2632 |
. . . . . . . . . . 11
⊢ ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖) = ∅ |
76 | 75 | difeq2i 3687 |
. . . . . . . . . 10
⊢ ((𝐸‘𝑀) ∖ ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖)) = ((𝐸‘𝑀) ∖ ∅) |
77 | 76 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸‘𝑀) ∖ ∪ 𝑖 ∈ (𝑀..^𝑀)(𝐸‘𝑖)) = ((𝐸‘𝑀) ∖ ∅)) |
78 | | dif0 3904 |
. . . . . . . . . 10
⊢ ((𝐸‘𝑀) ∖ ∅) = (𝐸‘𝑀) |
79 | 78 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸‘𝑀) ∖ ∅) = (𝐸‘𝑀)) |
80 | 70, 77, 79 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑀) = (𝐸‘𝑀)) |
81 | 80 | ineq2d 3776 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∩ (𝐹‘𝑀)) = (𝐴 ∩ (𝐸‘𝑀))) |
82 | 81 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (𝑂‘(𝐴 ∩ (𝐹‘𝑀))) = (𝑂‘(𝐴 ∩ (𝐸‘𝑀)))) |
83 | | carageniuncllem1.g |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) |
84 | 83 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))) |
85 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀)) |
86 | 85 | iuneq1d 4481 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑀 → ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖)) |
87 | 86 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖)) |
88 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (𝑀...𝑀) ∈ V |
89 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝐸‘𝑖) ∈ V |
90 | 88, 89 | iunex 7039 |
. . . . . . . . . . 11
⊢ ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V |
91 | 90 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V) |
92 | 84, 87, 65, 91 | fvmptd 6197 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝑀) = ∪
𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖)) |
93 | 38 | iuneq1d 4481 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) = ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖)) |
94 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑀 → (𝐸‘𝑖) = (𝐸‘𝑀)) |
95 | 94 | iunxsng 4538 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀)) |
96 | 36, 95 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀)) |
97 | 92, 93, 96 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝑀) = (𝐸‘𝑀)) |
98 | 97 | ineq2d 3776 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∩ (𝐺‘𝑀)) = (𝐴 ∩ (𝐸‘𝑀))) |
99 | 98 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (𝑂‘(𝐴 ∩ (𝐺‘𝑀))) = (𝑂‘(𝐴 ∩ (𝐸‘𝑀)))) |
100 | 53, 82, 99 | 3eqtr4d 2654 |
. . . . 5
⊢ (𝜑 → (𝑂‘(𝐴 ∩ (𝐹‘𝑀))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑀)))) |
101 | 39, 52, 100 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑀)))) |
102 | 101 | a1i 11 |
. . 3
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑀))))) |
103 | | simp3 1056 |
. . . . 5
⊢ ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) ∧ 𝜑) → 𝜑) |
104 | | simp1 1054 |
. . . . 5
⊢ ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) ∧ 𝜑) → 𝑗 ∈ (𝑀..^𝐾)) |
105 | | id 22 |
. . . . . . 7
⊢ ((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) → (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗))))) |
106 | 105 | imp 444 |
. . . . . 6
⊢ (((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) |
107 | 106 | 3adant1 1072 |
. . . . 5
⊢ ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) |
108 | | elfzouz 12343 |
. . . . . . . . 9
⊢ (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ (ℤ≥‘𝑀)) |
109 | 108 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → 𝑗 ∈ (ℤ≥‘𝑀)) |
110 | 40 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑗 + 1))) → 𝑂 ∈ OutMeas) |
111 | 42 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑗 + 1))) → 𝐴 ⊆ 𝑋) |
112 | 43 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘𝐴) ∈ ℝ) |
113 | | inss1 3795 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ (𝐹‘𝑛)) ⊆ 𝐴 |
114 | 113 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝐴 ∩ (𝐹‘𝑛)) ⊆ 𝐴) |
115 | 110, 41, 111, 112, 114 | omessre 39400 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ ℝ) |
116 | 115 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ ℂ) |
117 | 116 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) ∧ 𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ ℂ) |
118 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑗 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑗 + 1))) |
119 | 118 | ineq2d 3776 |
. . . . . . . . 9
⊢ (𝑛 = (𝑗 + 1) → (𝐴 ∩ (𝐹‘𝑛)) = (𝐴 ∩ (𝐹‘(𝑗 + 1)))) |
120 | 119 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑛 = (𝑗 + 1) → (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) |
121 | 109, 117,
120 | fsump1 14329 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1)))))) |
122 | 121 | 3adant3 1074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1)))))) |
123 | | oveq1 6556 |
. . . . . . 7
⊢
(Σ𝑛 ∈
(𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗))) → (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘(𝐴 ∩ (𝐺‘𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1)))))) |
124 | 123 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) → (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘(𝐴 ∩ (𝐺‘𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1)))))) |
125 | | fzssp1 12255 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀...𝑗) ⊆ (𝑀...(𝑗 + 1)) |
126 | | iunss1 4468 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀...𝑗) ⊆ (𝑀...(𝑗 + 1)) → ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ⊆ ∪
𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸‘𝑖)) |
127 | 125, 126 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ⊆ ∪
𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸‘𝑖) |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (𝑀..^𝐾) → ∪
𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ⊆ ∪
𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸‘𝑖)) |
129 | 83 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (𝑀..^𝐾) → 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))) |
130 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑗 → (𝑀...𝑛) = (𝑀...𝑗)) |
131 | 130 | iuneq1d 4481 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑗 → ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) |
132 | 131 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = 𝑗) → ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) |
133 | 108, 2 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ 𝑍) |
134 | | ovex 6577 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀...𝑗) ∈ V |
135 | 134, 89 | iunex 7039 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∈ V |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (𝑀..^𝐾) → ∪
𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∈ V) |
137 | 129, 132,
133, 136 | fvmptd 6197 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (𝑀..^𝐾) → (𝐺‘𝑗) = ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) |
138 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑗 + 1) → (𝑀...𝑛) = (𝑀...(𝑗 + 1))) |
139 | 138 | iuneq1d 4481 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑗 + 1) → ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸‘𝑖)) |
140 | 139 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = (𝑗 + 1)) → ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸‘𝑖)) |
141 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (𝑗 + 1) ∈
(ℤ≥‘𝑀)) |
142 | 108, 141 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (𝑀..^𝐾) → (𝑗 + 1) ∈
(ℤ≥‘𝑀)) |
143 | 2 | eqcomi 2619 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑀) = 𝑍 |
144 | 142, 143 | syl6eleq 2698 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (𝑀..^𝐾) → (𝑗 + 1) ∈ 𝑍) |
145 | | ovex 6577 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀...(𝑗 + 1)) ∈ V |
146 | 145, 89 | iunex 7039 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸‘𝑖) ∈ V |
147 | 146 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (𝑀..^𝐾) → ∪
𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸‘𝑖) ∈ V) |
148 | 129, 140,
144, 147 | fvmptd 6197 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (𝑀..^𝐾) → (𝐺‘(𝑗 + 1)) = ∪
𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸‘𝑖)) |
149 | 137, 148 | sseq12d 3597 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (𝑀..^𝐾) → ((𝐺‘𝑗) ⊆ (𝐺‘(𝑗 + 1)) ↔ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ⊆ ∪
𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸‘𝑖))) |
150 | 128, 149 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (𝑀..^𝐾) → (𝐺‘𝑗) ⊆ (𝐺‘(𝑗 + 1))) |
151 | | inabs3 38249 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘𝑗) ⊆ (𝐺‘(𝑗 + 1)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗)) = (𝐴 ∩ (𝐺‘𝑗))) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (𝑀..^𝐾) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗)) = (𝐴 ∩ (𝐺‘𝑗))) |
153 | 152 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (𝑀..^𝐾) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) |
154 | 153 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝑀..^𝐾) → (𝑂‘(𝐴 ∩ (𝐺‘𝑗))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗)))) |
155 | 154 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘(𝐴 ∩ (𝐺‘𝑗))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗)))) |
156 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ ℤ) |
157 | | fzval3 12404 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℤ → (𝑀...𝑗) = (𝑀..^(𝑗 + 1))) |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (𝑀..^𝐾) → (𝑀...𝑗) = (𝑀..^(𝑗 + 1))) |
159 | 158 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (𝑀..^𝐾) → (𝑀..^(𝑗 + 1)) = (𝑀...𝑗)) |
160 | 159 | iuneq1d 4481 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (𝑀..^𝐾) → ∪
𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) |
161 | 160 | difeq2d 3690 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (𝑀..^𝐾) → ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸‘𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖))) |
162 | 161 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸‘𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖))) |
163 | 54 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (𝑀..^𝐾) → 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖)))) |
164 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑗 + 1) → (𝐸‘𝑛) = (𝐸‘(𝑗 + 1))) |
165 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑗 + 1) → (𝑀..^𝑛) = (𝑀..^(𝑗 + 1))) |
166 | 165 | iuneq1d 4481 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑗 + 1) → ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸‘𝑖)) |
167 | 164, 166 | difeq12d 3691 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑗 + 1) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸‘𝑖))) |
168 | 167 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = (𝑗 + 1)) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸‘𝑖))) |
169 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸‘(𝑗 + 1)) ∈ V |
170 | | difexg 4735 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸‘(𝑗 + 1)) ∈ V → ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸‘𝑖)) ∈ V) |
171 | 169, 170 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸‘𝑖)) ∈ V |
172 | 171 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (𝑀..^𝐾) → ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸‘𝑖)) ∈ V) |
173 | 163, 168,
144, 172 | fvmptd 6197 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (𝑀..^𝐾) → (𝐹‘(𝑗 + 1)) = ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸‘𝑖))) |
174 | 173 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝐹‘(𝑗 + 1)) = ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸‘𝑖))) |
175 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖(𝐸‘(𝑗 + 1)) |
176 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = (𝑗 + 1) → (𝐸‘𝑖) = (𝐸‘(𝑗 + 1))) |
177 | 175, 108,
176 | iunp1 38260 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (𝑀..^𝐾) → ∪
𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸‘𝑖) = (∪
𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∪ (𝐸‘(𝑗 + 1)))) |
178 | 148, 177 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (𝑀..^𝐾) → (𝐺‘(𝑗 + 1)) = (∪
𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∪ (𝐸‘(𝑗 + 1)))) |
179 | 178, 137 | difeq12d 3691 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (𝑀..^𝐾) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺‘𝑗)) = ((∪
𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖))) |
180 | | difundir 3839 |
. . . . . . . . . . . . . . . . 17
⊢
((∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) = ((∪
𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∖ ∪
𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) ∪ ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖))) |
181 | | difid 3902 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∖ ∪
𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) = ∅ |
182 | 181 | uneq1i 3725 |
. . . . . . . . . . . . . . . . 17
⊢
((∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∖ ∪
𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) ∪ ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖))) = (∅ ∪ ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖))) |
183 | | 0un 38240 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∪ ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖))) = ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) |
184 | 180, 182,
183 | 3eqtri 2636 |
. . . . . . . . . . . . . . . 16
⊢
((∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) |
185 | 184 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (𝑀..^𝐾) → ((∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖))) |
186 | 179, 185 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (𝑀..^𝐾) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺‘𝑗)) = ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖))) |
187 | 186 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺‘𝑗)) = ((𝐸‘(𝑗 + 1)) ∖ ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖))) |
188 | 162, 174,
187 | 3eqtr4d 2654 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝐹‘(𝑗 + 1)) = ((𝐺‘(𝑗 + 1)) ∖ (𝐺‘𝑗))) |
189 | 188 | ineq2d 3776 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐹‘(𝑗 + 1))) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺‘𝑗)))) |
190 | | indif2 3829 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺‘𝑗))) = ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗)) |
191 | 190 | eqcomi 2619 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗)) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺‘𝑗))) |
192 | 191 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗)) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺‘𝑗)))) |
193 | 189, 192 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐹‘(𝑗 + 1))) = ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗))) |
194 | 193 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1)))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗)))) |
195 | 155, 194 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘(𝐴 ∩ (𝐺‘𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗))))) |
196 | | inss1 3795 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗)) ⊆ (𝐴 ∩ (𝐺‘(𝑗 + 1))) |
197 | | inss1 3795 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝐴 |
198 | 196, 197 | sstri 3577 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗)) ⊆ 𝐴 |
199 | 198 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗)) ⊆ 𝐴) |
200 | 40, 41, 42, 43, 199 | omessre 39400 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) ∈ ℝ) |
201 | 200 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) ∈ ℝ) |
202 | 40 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → 𝑂 ∈ OutMeas) |
203 | 42 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → 𝐴 ⊆ 𝑋) |
204 | 43 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘𝐴) ∈ ℝ) |
205 | | difss 3699 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗)) ⊆ (𝐴 ∩ (𝐺‘(𝑗 + 1))) |
206 | 205, 197 | sstri 3577 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗)) ⊆ 𝐴 |
207 | 206 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗)) ⊆ 𝐴) |
208 | 202, 41, 203, 204, 207 | omessre 39400 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗))) ∈ ℝ) |
209 | | rexadd 11937 |
. . . . . . . . . 10
⊢ (((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) ∈ ℝ ∧ (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗))) ∈ ℝ) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗))))) |
210 | 201, 208,
209 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗))))) |
211 | 210 | eqcomd 2616 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗))))) |
212 | | carageniuncllem1.s |
. . . . . . . . 9
⊢ 𝑆 = (CaraGen‘𝑂) |
213 | 137 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝐺‘𝑗) = ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖)) |
214 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖𝜑 |
215 | | fzfid 12634 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀...𝑗) ∈ Fin) |
216 | | carageniuncllem1.e |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸:𝑍⟶𝑆) |
217 | 216 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑗)) → 𝐸:𝑍⟶𝑆) |
218 | | elfzuz 12209 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...𝑗) → 𝑖 ∈ (ℤ≥‘𝑀)) |
219 | 143 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...𝑗) → (ℤ≥‘𝑀) = 𝑍) |
220 | 218, 219 | eleqtrd 2690 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀...𝑗) → 𝑖 ∈ 𝑍) |
221 | 220 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑗)) → 𝑖 ∈ 𝑍) |
222 | 217, 221 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑗)) → (𝐸‘𝑖) ∈ 𝑆) |
223 | 214, 40, 212, 215, 222 | caragenfiiuncl 39405 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∈ 𝑆) |
224 | 223 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → ∪ 𝑖 ∈ (𝑀...𝑗)(𝐸‘𝑖) ∈ 𝑆) |
225 | 213, 224 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝐺‘𝑗) ∈ 𝑆) |
226 | 42 | ssinss1d 38239 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝑋) |
227 | 226 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝑋) |
228 | 202, 212,
41, 225, 227 | caragensplit 39390 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺‘𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺‘𝑗)))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1))))) |
229 | 195, 211,
228 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘(𝐴 ∩ (𝐺‘𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1))))) |
230 | 229 | 3adant3 1074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) → ((𝑂‘(𝐴 ∩ (𝐺‘𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1))))) |
231 | 122, 124,
230 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1))))) |
232 | 103, 104,
107, 231 | syl3anc 1318 |
. . . 4
⊢ ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1))))) |
233 | 232 | 3exp 1256 |
. . 3
⊢ (𝑗 ∈ (𝑀..^𝐾) → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑗)))) → (𝜑 → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1))))))) |
234 | 13, 20, 27, 34, 102, 233 | fzind2 12448 |
. 2
⊢ (𝐾 ∈ (𝑀...𝐾) → (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝐾))))) |
235 | 5, 6, 234 | sylc 63 |
1
⊢ (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝐾)))) |