Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  carageniuncllem1 Structured version   Visualization version   GIF version

Theorem carageniuncllem1 41218
Description: The outer measure of 𝐴 ∩ (𝐺𝑛) is the sum of the outer measures of 𝐴 ∩ (𝐹𝑚). These are lines 7 to 10 of Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
carageniuncllem1.o (𝜑𝑂 ∈ OutMeas)
carageniuncllem1.s 𝑆 = (CaraGen‘𝑂)
carageniuncllem1.x 𝑋 = dom 𝑂
carageniuncllem1.a (𝜑𝐴𝑋)
carageniuncllem1.re (𝜑 → (𝑂𝐴) ∈ ℝ)
carageniuncllem1.z 𝑍 = (ℤ𝑀)
carageniuncllem1.e (𝜑𝐸:𝑍𝑆)
carageniuncllem1.g 𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖))
carageniuncllem1.f 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)))
carageniuncllem1.k (𝜑𝐾𝑍)
Assertion
Ref Expression
carageniuncllem1 (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾))))
Distinct variable groups:   𝐴,𝑛   𝑖,𝐸,𝑛   𝑛,𝐹   𝑛,𝐾   𝑖,𝑀,𝑛   𝑛,𝑂   𝑆,𝑖   𝑛,𝑍   𝜑,𝑖,𝑛
Allowed substitution hints:   𝐴(𝑖)   𝑆(𝑛)   𝐹(𝑖)   𝐺(𝑖,𝑛)   𝐾(𝑖)   𝑂(𝑖)   𝑋(𝑖,𝑛)   𝑍(𝑖)

Proof of Theorem carageniuncllem1
Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 carageniuncllem1.k . . . 4 (𝜑𝐾𝑍)
2 carageniuncllem1.z . . . 4 𝑍 = (ℤ𝑀)
31, 2syl6eleq 2902 . . 3 (𝜑𝐾 ∈ (ℤ𝑀))
4 eluzfz2 12575 . . 3 (𝐾 ∈ (ℤ𝑀) → 𝐾 ∈ (𝑀...𝐾))
53, 4syl 17 . 2 (𝜑𝐾 ∈ (𝑀...𝐾))
6 id 22 . 2 (𝜑𝜑)
7 oveq2 6885 . . . . . 6 (𝑘 = 𝑀 → (𝑀...𝑘) = (𝑀...𝑀))
87sumeq1d 14657 . . . . 5 (𝑘 = 𝑀 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))))
9 fveq2 6411 . . . . . . 7 (𝑘 = 𝑀 → (𝐺𝑘) = (𝐺𝑀))
109ineq2d 4020 . . . . . 6 (𝑘 = 𝑀 → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺𝑀)))
1110fveq2d 6415 . . . . 5 (𝑘 = 𝑀 → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))
128, 11eqeq12d 2828 . . . 4 (𝑘 = 𝑀 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀)))))
1312imbi2d 331 . . 3 (𝑘 = 𝑀 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))))
14 oveq2 6885 . . . . . 6 (𝑘 = 𝑗 → (𝑀...𝑘) = (𝑀...𝑗))
1514sumeq1d 14657 . . . . 5 (𝑘 = 𝑗 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))))
16 fveq2 6411 . . . . . . 7 (𝑘 = 𝑗 → (𝐺𝑘) = (𝐺𝑗))
1716ineq2d 4020 . . . . . 6 (𝑘 = 𝑗 → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺𝑗)))
1817fveq2d 6415 . . . . 5 (𝑘 = 𝑗 → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
1915, 18eqeq12d 2828 . . . 4 (𝑘 = 𝑗 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))))
2019imbi2d 331 . . 3 (𝑘 = 𝑗 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))))
21 oveq2 6885 . . . . . 6 (𝑘 = (𝑗 + 1) → (𝑀...𝑘) = (𝑀...(𝑗 + 1)))
2221sumeq1d 14657 . . . . 5 (𝑘 = (𝑗 + 1) → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))))
23 fveq2 6411 . . . . . . 7 (𝑘 = (𝑗 + 1) → (𝐺𝑘) = (𝐺‘(𝑗 + 1)))
2423ineq2d 4020 . . . . . 6 (𝑘 = (𝑗 + 1) → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺‘(𝑗 + 1))))
2524fveq2d 6415 . . . . 5 (𝑘 = (𝑗 + 1) → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
2622, 25eqeq12d 2828 . . . 4 (𝑘 = (𝑗 + 1) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1))))))
2726imbi2d 331 . . 3 (𝑘 = (𝑗 + 1) → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))))
28 oveq2 6885 . . . . . 6 (𝑘 = 𝐾 → (𝑀...𝑘) = (𝑀...𝐾))
2928sumeq1d 14657 . . . . 5 (𝑘 = 𝐾 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))))
30 fveq2 6411 . . . . . . 7 (𝑘 = 𝐾 → (𝐺𝑘) = (𝐺𝐾))
3130ineq2d 4020 . . . . . 6 (𝑘 = 𝐾 → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺𝐾)))
3231fveq2d 6415 . . . . 5 (𝑘 = 𝐾 → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺𝐾))))
3329, 32eqeq12d 2828 . . . 4 (𝑘 = 𝐾 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾)))))
3433imbi2d 331 . . 3 (𝑘 = 𝐾 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾))))))
35 eluzel2 11912 . . . . . . . 8 (𝐾 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
363, 35syl 17 . . . . . . 7 (𝜑𝑀 ∈ ℤ)
37 fzsn 12609 . . . . . . 7 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
3836, 37syl 17 . . . . . 6 (𝜑 → (𝑀...𝑀) = {𝑀})
3938sumeq1d 14657 . . . . 5 (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹𝑛))))
40 carageniuncllem1.o . . . . . . . 8 (𝜑𝑂 ∈ OutMeas)
41 carageniuncllem1.x . . . . . . . 8 𝑋 = dom 𝑂
42 carageniuncllem1.a . . . . . . . 8 (𝜑𝐴𝑋)
43 carageniuncllem1.re . . . . . . . 8 (𝜑 → (𝑂𝐴) ∈ ℝ)
44 inss1 4036 . . . . . . . . 9 (𝐴 ∩ (𝐹𝑀)) ⊆ 𝐴
4544a1i 11 . . . . . . . 8 (𝜑 → (𝐴 ∩ (𝐹𝑀)) ⊆ 𝐴)
4640, 41, 42, 43, 45omessre 41207 . . . . . . 7 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) ∈ ℝ)
4746recnd 10356 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) ∈ ℂ)
48 fveq2 6411 . . . . . . . . 9 (𝑛 = 𝑀 → (𝐹𝑛) = (𝐹𝑀))
4948ineq2d 4020 . . . . . . . 8 (𝑛 = 𝑀 → (𝐴 ∩ (𝐹𝑛)) = (𝐴 ∩ (𝐹𝑀)))
5049fveq2d 6415 . . . . . . 7 (𝑛 = 𝑀 → (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹𝑀))))
5150sumsn 14701 . . . . . 6 ((𝑀 ∈ ℤ ∧ (𝑂‘(𝐴 ∩ (𝐹𝑀))) ∈ ℂ) → Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹𝑀))))
5236, 47, 51syl2anc 575 . . . . 5 (𝜑 → Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹𝑀))))
53 eqidd 2814 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐸𝑀))) = (𝑂‘(𝐴 ∩ (𝐸𝑀))))
54 carageniuncllem1.f . . . . . . . . . . 11 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)))
5554a1i 11 . . . . . . . . . 10 (𝜑𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖))))
56 fveq2 6411 . . . . . . . . . . . 12 (𝑛 = 𝑀 → (𝐸𝑛) = (𝐸𝑀))
57 oveq2 6885 . . . . . . . . . . . . 13 (𝑛 = 𝑀 → (𝑀..^𝑛) = (𝑀..^𝑀))
5857iuneq1d 4744 . . . . . . . . . . . 12 (𝑛 = 𝑀 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖))
5956, 58difeq12d 3935 . . . . . . . . . . 11 (𝑛 = 𝑀 → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)))
6059adantl 469 . . . . . . . . . 10 ((𝜑𝑛 = 𝑀) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)))
61 uzid 11922 . . . . . . . . . . . 12 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
6236, 61syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ (ℤ𝑀))
632a1i 11 . . . . . . . . . . . 12 (𝜑𝑍 = (ℤ𝑀))
6463eqcomd 2819 . . . . . . . . . . 11 (𝜑 → (ℤ𝑀) = 𝑍)
6562, 64eleqtrd 2894 . . . . . . . . . 10 (𝜑𝑀𝑍)
66 fvex 6424 . . . . . . . . . . . 12 (𝐸𝑀) ∈ V
67 difexg 5010 . . . . . . . . . . . 12 ((𝐸𝑀) ∈ V → ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) ∈ V)
6866, 67ax-mp 5 . . . . . . . . . . 11 ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) ∈ V
6968a1i 11 . . . . . . . . . 10 (𝜑 → ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) ∈ V)
7055, 60, 65, 69fvmptd 6512 . . . . . . . . 9 (𝜑 → (𝐹𝑀) = ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)))
71 fzo0 12719 . . . . . . . . . . . . 13 (𝑀..^𝑀) = ∅
72 iuneq1 4733 . . . . . . . . . . . . 13 ((𝑀..^𝑀) = ∅ → 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖) = 𝑖 ∈ ∅ (𝐸𝑖))
7371, 72ax-mp 5 . . . . . . . . . . . 12 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖) = 𝑖 ∈ ∅ (𝐸𝑖)
74 0iun 4776 . . . . . . . . . . . 12 𝑖 ∈ ∅ (𝐸𝑖) = ∅
7573, 74eqtri 2835 . . . . . . . . . . 11 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖) = ∅
7675difeq2i 3931 . . . . . . . . . 10 ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) = ((𝐸𝑀) ∖ ∅)
7776a1i 11 . . . . . . . . 9 (𝜑 → ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) = ((𝐸𝑀) ∖ ∅))
78 dif0 4158 . . . . . . . . . 10 ((𝐸𝑀) ∖ ∅) = (𝐸𝑀)
7978a1i 11 . . . . . . . . 9 (𝜑 → ((𝐸𝑀) ∖ ∅) = (𝐸𝑀))
8070, 77, 793eqtrd 2851 . . . . . . . 8 (𝜑 → (𝐹𝑀) = (𝐸𝑀))
8180ineq2d 4020 . . . . . . 7 (𝜑 → (𝐴 ∩ (𝐹𝑀)) = (𝐴 ∩ (𝐸𝑀)))
8281fveq2d 6415 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) = (𝑂‘(𝐴 ∩ (𝐸𝑀))))
83 carageniuncllem1.g . . . . . . . . . . 11 𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖))
8483a1i 11 . . . . . . . . . 10 (𝜑𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖)))
85 oveq2 6885 . . . . . . . . . . . 12 (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
8685iuneq1d 4744 . . . . . . . . . . 11 (𝑛 = 𝑀 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
8786adantl 469 . . . . . . . . . 10 ((𝜑𝑛 = 𝑀) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
88 ovex 6909 . . . . . . . . . . . 12 (𝑀...𝑀) ∈ V
89 fvex 6424 . . . . . . . . . . . 12 (𝐸𝑖) ∈ V
9088, 89iunex 7380 . . . . . . . . . . 11 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) ∈ V
9190a1i 11 . . . . . . . . . 10 (𝜑 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) ∈ V)
9284, 87, 65, 91fvmptd 6512 . . . . . . . . 9 (𝜑 → (𝐺𝑀) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
9338iuneq1d 4744 . . . . . . . . 9 (𝜑 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) = 𝑖 ∈ {𝑀} (𝐸𝑖))
94 fveq2 6411 . . . . . . . . . . 11 (𝑖 = 𝑀 → (𝐸𝑖) = (𝐸𝑀))
9594iunxsng 4801 . . . . . . . . . 10 (𝑀 ∈ ℤ → 𝑖 ∈ {𝑀} (𝐸𝑖) = (𝐸𝑀))
9636, 95syl 17 . . . . . . . . 9 (𝜑 𝑖 ∈ {𝑀} (𝐸𝑖) = (𝐸𝑀))
9792, 93, 963eqtrd 2851 . . . . . . . 8 (𝜑 → (𝐺𝑀) = (𝐸𝑀))
9897ineq2d 4020 . . . . . . 7 (𝜑 → (𝐴 ∩ (𝐺𝑀)) = (𝐴 ∩ (𝐸𝑀)))
9998fveq2d 6415 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐺𝑀))) = (𝑂‘(𝐴 ∩ (𝐸𝑀))))
10053, 82, 993eqtr4d 2857 . . . . 5 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))
10139, 52, 1003eqtrd 2851 . . . 4 (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))
102101a1i 11 . . 3 (𝐾 ∈ (ℤ𝑀) → (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀)))))
103 simp3 1161 . . . . 5 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → 𝜑)
104 simp1 1159 . . . . 5 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → 𝑗 ∈ (𝑀..^𝐾))
105 id 22 . . . . . . 7 ((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))))
106105imp 395 . . . . . 6 (((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
1071063adant1 1153 . . . . 5 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
108 elfzouz 12701 . . . . . . . . 9 (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ (ℤ𝑀))
109108adantl 469 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝑗 ∈ (ℤ𝑀))
11040adantr 468 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → 𝑂 ∈ OutMeas)
11142adantr 468 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → 𝐴𝑋)
11243adantr 468 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂𝐴) ∈ ℝ)
113 inss1 4036 . . . . . . . . . . . 12 (𝐴 ∩ (𝐹𝑛)) ⊆ 𝐴
114113a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝐴 ∩ (𝐹𝑛)) ⊆ 𝐴)
115110, 41, 111, 112, 114omessre 41207 . . . . . . . . . 10 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
116115recnd 10356 . . . . . . . . 9 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℂ)
117116adantlr 697 . . . . . . . 8 (((𝜑𝑗 ∈ (𝑀..^𝐾)) ∧ 𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℂ)
118 fveq2 6411 . . . . . . . . . 10 (𝑛 = (𝑗 + 1) → (𝐹𝑛) = (𝐹‘(𝑗 + 1)))
119118ineq2d 4020 . . . . . . . . 9 (𝑛 = (𝑗 + 1) → (𝐴 ∩ (𝐹𝑛)) = (𝐴 ∩ (𝐹‘(𝑗 + 1))))
120119fveq2d 6415 . . . . . . . 8 (𝑛 = (𝑗 + 1) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1)))))
121109, 117, 120fsump1 14713 . . . . . . 7 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
1221213adant3 1155 . . . . . 6 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
123 oveq1 6884 . . . . . . 7 𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))) → (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
1241233ad2ant3 1158 . . . . . 6 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
125 fzssp1 12610 . . . . . . . . . . . . . . . 16 (𝑀...𝑗) ⊆ (𝑀...(𝑗 + 1))
126 iunss1 4731 . . . . . . . . . . . . . . . 16 ((𝑀...𝑗) ⊆ (𝑀...(𝑗 + 1)) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
127125, 126ax-mp 5 . . . . . . . . . . . . . . 15 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖)
128127a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
12983a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖)))
130 oveq2 6885 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑗 → (𝑀...𝑛) = (𝑀...𝑗))
131130iuneq1d 4744 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
132131adantl 469 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = 𝑗) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
133108, 2syl6eleqr 2903 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝑗𝑍)
134 ovex 6909 . . . . . . . . . . . . . . . . . 18 (𝑀...𝑗) ∈ V
135134, 89iunex 7380 . . . . . . . . . . . . . . . . 17 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ V
136135a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ V)
137129, 132, 133, 136fvmptd 6512 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → (𝐺𝑗) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
138 oveq2 6885 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑗 + 1) → (𝑀...𝑛) = (𝑀...(𝑗 + 1)))
139138iuneq1d 4744 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑗 + 1) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
140139adantl 469 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = (𝑗 + 1)) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
141 peano2uz 11962 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (ℤ𝑀) → (𝑗 + 1) ∈ (ℤ𝑀))
142108, 141syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝐾) → (𝑗 + 1) ∈ (ℤ𝑀))
1432eqcomi 2822 . . . . . . . . . . . . . . . . 17 (ℤ𝑀) = 𝑍
144142, 143syl6eleq 2902 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → (𝑗 + 1) ∈ 𝑍)
145 ovex 6909 . . . . . . . . . . . . . . . . . 18 (𝑀...(𝑗 + 1)) ∈ V
146145, 89iunex 7380 . . . . . . . . . . . . . . . . 17 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖) ∈ V
147146a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖) ∈ V)
148129, 140, 144, 147fvmptd 6512 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → (𝐺‘(𝑗 + 1)) = 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
149137, 148sseq12d 3838 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → ((𝐺𝑗) ⊆ (𝐺‘(𝑗 + 1)) ↔ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖)))
150128, 149mpbird 248 . . . . . . . . . . . . 13 (𝑗 ∈ (𝑀..^𝐾) → (𝐺𝑗) ⊆ (𝐺‘(𝑗 + 1)))
151 inabs3 39718 . . . . . . . . . . . . 13 ((𝐺𝑗) ⊆ (𝐺‘(𝑗 + 1)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) = (𝐴 ∩ (𝐺𝑗)))
152150, 151syl 17 . . . . . . . . . . . 12 (𝑗 ∈ (𝑀..^𝐾) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) = (𝐴 ∩ (𝐺𝑗)))
153152fveq2d 6415 . . . . . . . . . . 11 (𝑗 ∈ (𝑀..^𝐾) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
154153eqcomd 2819 . . . . . . . . . 10 (𝑗 ∈ (𝑀..^𝐾) → (𝑂‘(𝐴 ∩ (𝐺𝑗))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))))
155154adantl 469 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘(𝐴 ∩ (𝐺𝑗))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))))
156 elfzoelz 12697 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ ℤ)
157 fzval3 12764 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℤ → (𝑀...𝑗) = (𝑀..^(𝑗 + 1)))
158156, 157syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝐾) → (𝑀...𝑗) = (𝑀..^(𝑗 + 1)))
159158eqcomd 2819 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → (𝑀..^(𝑗 + 1)) = (𝑀...𝑗))
160159iuneq1d 4744 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
161160difeq2d 3934 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
162161adantl 469 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
16354a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖))))
164 fveq2 6411 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑗 + 1) → (𝐸𝑛) = (𝐸‘(𝑗 + 1)))
165 oveq2 6885 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑗 + 1) → (𝑀..^𝑛) = (𝑀..^(𝑗 + 1)))
166165iuneq1d 4744 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑗 + 1) → 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖))
167164, 166difeq12d 3935 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑗 + 1) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
168167adantl 469 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = (𝑗 + 1)) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
169 fvex 6424 . . . . . . . . . . . . . . . . 17 (𝐸‘(𝑗 + 1)) ∈ V
170 difexg 5010 . . . . . . . . . . . . . . . . 17 ((𝐸‘(𝑗 + 1)) ∈ V → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) ∈ V)
171169, 170ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) ∈ V
172171a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) ∈ V)
173163, 168, 144, 172fvmptd 6512 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → (𝐹‘(𝑗 + 1)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
174173adantl 469 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐹‘(𝑗 + 1)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
175 nfcv 2955 . . . . . . . . . . . . . . . . . 18 𝑖(𝐸‘(𝑗 + 1))
176 fveq2 6411 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 + 1) → (𝐸𝑖) = (𝐸‘(𝑗 + 1)))
177175, 108, 176iunp1 39729 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖) = ( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))))
178148, 177eqtrd 2847 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → (𝐺‘(𝑗 + 1)) = ( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))))
179178, 137difeq12d 3935 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)) = (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
180 difundir 4089 . . . . . . . . . . . . . . . . 17 (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
181 difid 4156 . . . . . . . . . . . . . . . . . 18 ( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = ∅
182181uneq1i 3969 . . . . . . . . . . . . . . . . 17 (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))) = (∅ ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
183 0un 39709 . . . . . . . . . . . . . . . . 17 (∅ ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
184180, 182, 1833eqtri 2839 . . . . . . . . . . . . . . . 16 (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
185184a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
186179, 185eqtrd 2847 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
187186adantl 469 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
188162, 174, 1873eqtr4d 2857 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐹‘(𝑗 + 1)) = ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)))
189188ineq2d 4020 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐹‘(𝑗 + 1))) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗))))
190 indif2 4079 . . . . . . . . . . . . 13 (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗))) = ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))
191190eqcomi 2822 . . . . . . . . . . . 12 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)))
192191a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗))))
193189, 192eqtr4d 2850 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐹‘(𝑗 + 1))) = ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))
194193fveq2d 6415 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1)))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))))
195155, 194oveq12d 6895 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
196 inss1 4036 . . . . . . . . . . . . . 14 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) ⊆ (𝐴 ∩ (𝐺‘(𝑗 + 1)))
197 inss1 4036 . . . . . . . . . . . . . 14 (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝐴
198196, 197sstri 3814 . . . . . . . . . . . . 13 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) ⊆ 𝐴
199198a1i 11 . . . . . . . . . . . 12 (𝜑 → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) ⊆ 𝐴)
20040, 41, 42, 43, 199omessre 41207 . . . . . . . . . . 11 (𝜑 → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) ∈ ℝ)
201200adantr 468 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) ∈ ℝ)
20240adantr 468 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝑂 ∈ OutMeas)
20342adantr 468 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝐴𝑋)
20443adantr 468 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂𝐴) ∈ ℝ)
205 difss 3943 . . . . . . . . . . . . 13 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) ⊆ (𝐴 ∩ (𝐺‘(𝑗 + 1)))
206205, 197sstri 3814 . . . . . . . . . . . 12 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) ⊆ 𝐴
207206a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) ⊆ 𝐴)
208202, 41, 203, 204, 207omessre 41207 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))) ∈ ℝ)
209 rexadd 12284 . . . . . . . . . 10 (((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) ∈ ℝ ∧ (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))) ∈ ℝ) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
210201, 208, 209syl2anc 575 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
211210eqcomd 2819 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
212 carageniuncllem1.s . . . . . . . . 9 𝑆 = (CaraGen‘𝑂)
213137adantl 469 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐺𝑗) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
214 nfv 2005 . . . . . . . . . . . 12 𝑖𝜑
215 fzfid 12999 . . . . . . . . . . . 12 (𝜑 → (𝑀...𝑗) ∈ Fin)
216 carageniuncllem1.e . . . . . . . . . . . . . 14 (𝜑𝐸:𝑍𝑆)
217216adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀...𝑗)) → 𝐸:𝑍𝑆)
218 elfzuz 12564 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑗) → 𝑖 ∈ (ℤ𝑀))
219143a1i 11 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑗) → (ℤ𝑀) = 𝑍)
220218, 219eleqtrd 2894 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀...𝑗) → 𝑖𝑍)
221220adantl 469 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀...𝑗)) → 𝑖𝑍)
222217, 221ffvelrnd 6585 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝑀...𝑗)) → (𝐸𝑖) ∈ 𝑆)
223214, 40, 212, 215, 222caragenfiiuncl 41212 . . . . . . . . . . 11 (𝜑 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ 𝑆)
224223adantr 468 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ 𝑆)
225213, 224eqeltrd 2892 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐺𝑗) ∈ 𝑆)
22642ssinss1d 39708 . . . . . . . . . 10 (𝜑 → (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝑋)
227226adantr 468 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝑋)
228202, 212, 41, 225, 227caragensplit 41197 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
229195, 211, 2283eqtrd 2851 . . . . . . 7 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
2302293adant3 1155 . . . . . 6 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
231122, 124, 2303eqtrd 2851 . . . . 5 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
232103, 104, 107, 231syl3anc 1483 . . . 4 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
2332323exp 1141 . . 3 (𝑗 ∈ (𝑀..^𝐾) → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → (𝜑 → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))))
23413, 20, 27, 34, 102, 233fzind2 12813 . 2 (𝐾 ∈ (𝑀...𝐾) → (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾)))))
2355, 6, 234sylc 65 1 (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wcel 2157  Vcvv 3398  cdif 3773  cun 3774  cin 3775  wss 3776  c0 4123  {csn 4377   cuni 4637   ciun 4719  cmpt 4930  dom cdm 5318  wf 6100  cfv 6104  (class class class)co 6877  cc 10222  cr 10223  1c1 10225   + caddc 10227  cz 11646  cuz 11907   +𝑒 cxad 12163  ...cfz 12552  ..^cfzo 12692  Σcsu 14642  OutMeascome 41186  CaraGenccaragen 41188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301  ax-pre-sup 10302
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-se 5278  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-isom 6113  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-oadd 7803  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-sup 8590  df-oi 8657  df-card 9051  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-div 10973  df-nn 11309  df-2 11367  df-3 11368  df-n0 11563  df-z 11647  df-uz 11908  df-rp 12050  df-xadd 12166  df-ico 12402  df-icc 12403  df-fz 12553  df-fzo 12693  df-seq 13028  df-exp 13087  df-hash 13341  df-cj 14065  df-re 14066  df-im 14067  df-sqrt 14201  df-abs 14202  df-clim 14445  df-sum 14643  df-ome 41187  df-caragen 41189
This theorem is referenced by:  carageniuncllem2  41219
  Copyright terms: Public domain W3C validator