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 40498
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 2709 . . 3 (𝜑𝐾 ∈ (ℤ𝑀))
4 eluzfz2 12334 . . 3 (𝐾 ∈ (ℤ𝑀) → 𝐾 ∈ (𝑀...𝐾))
53, 4syl 17 . 2 (𝜑𝐾 ∈ (𝑀...𝐾))
6 id 22 . 2 (𝜑𝜑)
7 oveq2 6643 . . . . . 6 (𝑘 = 𝑀 → (𝑀...𝑘) = (𝑀...𝑀))
87sumeq1d 14412 . . . . 5 (𝑘 = 𝑀 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))))
9 fveq2 6178 . . . . . . 7 (𝑘 = 𝑀 → (𝐺𝑘) = (𝐺𝑀))
109ineq2d 3806 . . . . . 6 (𝑘 = 𝑀 → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺𝑀)))
1110fveq2d 6182 . . . . 5 (𝑘 = 𝑀 → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))
128, 11eqeq12d 2635 . . . 4 (𝑘 = 𝑀 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀)))))
1312imbi2d 330 . . 3 (𝑘 = 𝑀 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))))
14 oveq2 6643 . . . . . 6 (𝑘 = 𝑗 → (𝑀...𝑘) = (𝑀...𝑗))
1514sumeq1d 14412 . . . . 5 (𝑘 = 𝑗 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))))
16 fveq2 6178 . . . . . . 7 (𝑘 = 𝑗 → (𝐺𝑘) = (𝐺𝑗))
1716ineq2d 3806 . . . . . 6 (𝑘 = 𝑗 → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺𝑗)))
1817fveq2d 6182 . . . . 5 (𝑘 = 𝑗 → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
1915, 18eqeq12d 2635 . . . 4 (𝑘 = 𝑗 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))))
2019imbi2d 330 . . 3 (𝑘 = 𝑗 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))))
21 oveq2 6643 . . . . . 6 (𝑘 = (𝑗 + 1) → (𝑀...𝑘) = (𝑀...(𝑗 + 1)))
2221sumeq1d 14412 . . . . 5 (𝑘 = (𝑗 + 1) → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))))
23 fveq2 6178 . . . . . . 7 (𝑘 = (𝑗 + 1) → (𝐺𝑘) = (𝐺‘(𝑗 + 1)))
2423ineq2d 3806 . . . . . 6 (𝑘 = (𝑗 + 1) → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺‘(𝑗 + 1))))
2524fveq2d 6182 . . . . 5 (𝑘 = (𝑗 + 1) → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
2622, 25eqeq12d 2635 . . . 4 (𝑘 = (𝑗 + 1) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1))))))
2726imbi2d 330 . . 3 (𝑘 = (𝑗 + 1) → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))))
28 oveq2 6643 . . . . . 6 (𝑘 = 𝐾 → (𝑀...𝑘) = (𝑀...𝐾))
2928sumeq1d 14412 . . . . 5 (𝑘 = 𝐾 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))))
30 fveq2 6178 . . . . . . 7 (𝑘 = 𝐾 → (𝐺𝑘) = (𝐺𝐾))
3130ineq2d 3806 . . . . . 6 (𝑘 = 𝐾 → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺𝐾)))
3231fveq2d 6182 . . . . 5 (𝑘 = 𝐾 → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺𝐾))))
3329, 32eqeq12d 2635 . . . 4 (𝑘 = 𝐾 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾)))))
3433imbi2d 330 . . 3 (𝑘 = 𝐾 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾))))))
35 eluzel2 11677 . . . . . . . 8 (𝐾 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
363, 35syl 17 . . . . . . 7 (𝜑𝑀 ∈ ℤ)
37 fzsn 12368 . . . . . . 7 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
3836, 37syl 17 . . . . . 6 (𝜑 → (𝑀...𝑀) = {𝑀})
3938sumeq1d 14412 . . . . 5 (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹𝑛))))
40 carageniuncllem1.o . . . . . . . 8 (𝜑𝑂 ∈ OutMeas)
41 carageniuncllem1.x . . . . . . . 8 𝑋 = dom 𝑂
42 carageniuncllem1.a . . . . . . . 8 (𝜑𝐴𝑋)
43 carageniuncllem1.re . . . . . . . 8 (𝜑 → (𝑂𝐴) ∈ ℝ)
44 inss1 3825 . . . . . . . . 9 (𝐴 ∩ (𝐹𝑀)) ⊆ 𝐴
4544a1i 11 . . . . . . . 8 (𝜑 → (𝐴 ∩ (𝐹𝑀)) ⊆ 𝐴)
4640, 41, 42, 43, 45omessre 40487 . . . . . . 7 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) ∈ ℝ)
4746recnd 10053 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) ∈ ℂ)
48 fveq2 6178 . . . . . . . . 9 (𝑛 = 𝑀 → (𝐹𝑛) = (𝐹𝑀))
4948ineq2d 3806 . . . . . . . 8 (𝑛 = 𝑀 → (𝐴 ∩ (𝐹𝑛)) = (𝐴 ∩ (𝐹𝑀)))
5049fveq2d 6182 . . . . . . 7 (𝑛 = 𝑀 → (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹𝑀))))
5150sumsn 14456 . . . . . 6 ((𝑀 ∈ ℤ ∧ (𝑂‘(𝐴 ∩ (𝐹𝑀))) ∈ ℂ) → Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹𝑀))))
5236, 47, 51syl2anc 692 . . . . 5 (𝜑 → Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹𝑀))))
53 eqidd 2621 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐸𝑀))) = (𝑂‘(𝐴 ∩ (𝐸𝑀))))
54 carageniuncllem1.f . . . . . . . . . . 11 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)))
5554a1i 11 . . . . . . . . . 10 (𝜑𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖))))
56 fveq2 6178 . . . . . . . . . . . 12 (𝑛 = 𝑀 → (𝐸𝑛) = (𝐸𝑀))
57 oveq2 6643 . . . . . . . . . . . . 13 (𝑛 = 𝑀 → (𝑀..^𝑛) = (𝑀..^𝑀))
5857iuneq1d 4536 . . . . . . . . . . . 12 (𝑛 = 𝑀 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖))
5956, 58difeq12d 3721 . . . . . . . . . . 11 (𝑛 = 𝑀 → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)))
6059adantl 482 . . . . . . . . . 10 ((𝜑𝑛 = 𝑀) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)))
61 uzid 11687 . . . . . . . . . . . 12 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
6236, 61syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ (ℤ𝑀))
632a1i 11 . . . . . . . . . . . 12 (𝜑𝑍 = (ℤ𝑀))
6463eqcomd 2626 . . . . . . . . . . 11 (𝜑 → (ℤ𝑀) = 𝑍)
6562, 64eleqtrd 2701 . . . . . . . . . 10 (𝜑𝑀𝑍)
66 fvex 6188 . . . . . . . . . . . 12 (𝐸𝑀) ∈ V
67 difexg 4799 . . . . . . . . . . . 12 ((𝐸𝑀) ∈ V → ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) ∈ V)
6866, 67ax-mp 5 . . . . . . . . . . 11 ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) ∈ V
6968a1i 11 . . . . . . . . . 10 (𝜑 → ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) ∈ V)
7055, 60, 65, 69fvmptd 6275 . . . . . . . . 9 (𝜑 → (𝐹𝑀) = ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)))
71 fzo0 12476 . . . . . . . . . . . . 13 (𝑀..^𝑀) = ∅
72 iuneq1 4525 . . . . . . . . . . . . 13 ((𝑀..^𝑀) = ∅ → 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖) = 𝑖 ∈ ∅ (𝐸𝑖))
7371, 72ax-mp 5 . . . . . . . . . . . 12 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖) = 𝑖 ∈ ∅ (𝐸𝑖)
74 0iun 4568 . . . . . . . . . . . 12 𝑖 ∈ ∅ (𝐸𝑖) = ∅
7573, 74eqtri 2642 . . . . . . . . . . 11 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖) = ∅
7675difeq2i 3717 . . . . . . . . . 10 ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) = ((𝐸𝑀) ∖ ∅)
7776a1i 11 . . . . . . . . 9 (𝜑 → ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) = ((𝐸𝑀) ∖ ∅))
78 dif0 3941 . . . . . . . . . 10 ((𝐸𝑀) ∖ ∅) = (𝐸𝑀)
7978a1i 11 . . . . . . . . 9 (𝜑 → ((𝐸𝑀) ∖ ∅) = (𝐸𝑀))
8070, 77, 793eqtrd 2658 . . . . . . . 8 (𝜑 → (𝐹𝑀) = (𝐸𝑀))
8180ineq2d 3806 . . . . . . 7 (𝜑 → (𝐴 ∩ (𝐹𝑀)) = (𝐴 ∩ (𝐸𝑀)))
8281fveq2d 6182 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) = (𝑂‘(𝐴 ∩ (𝐸𝑀))))
83 carageniuncllem1.g . . . . . . . . . . 11 𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖))
8483a1i 11 . . . . . . . . . 10 (𝜑𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖)))
85 oveq2 6643 . . . . . . . . . . . 12 (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
8685iuneq1d 4536 . . . . . . . . . . 11 (𝑛 = 𝑀 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
8786adantl 482 . . . . . . . . . 10 ((𝜑𝑛 = 𝑀) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
88 ovex 6663 . . . . . . . . . . . 12 (𝑀...𝑀) ∈ V
89 fvex 6188 . . . . . . . . . . . 12 (𝐸𝑖) ∈ V
9088, 89iunex 7132 . . . . . . . . . . 11 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) ∈ V
9190a1i 11 . . . . . . . . . 10 (𝜑 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) ∈ V)
9284, 87, 65, 91fvmptd 6275 . . . . . . . . 9 (𝜑 → (𝐺𝑀) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
9338iuneq1d 4536 . . . . . . . . 9 (𝜑 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) = 𝑖 ∈ {𝑀} (𝐸𝑖))
94 fveq2 6178 . . . . . . . . . . 11 (𝑖 = 𝑀 → (𝐸𝑖) = (𝐸𝑀))
9594iunxsng 4593 . . . . . . . . . 10 (𝑀 ∈ ℤ → 𝑖 ∈ {𝑀} (𝐸𝑖) = (𝐸𝑀))
9636, 95syl 17 . . . . . . . . 9 (𝜑 𝑖 ∈ {𝑀} (𝐸𝑖) = (𝐸𝑀))
9792, 93, 963eqtrd 2658 . . . . . . . 8 (𝜑 → (𝐺𝑀) = (𝐸𝑀))
9897ineq2d 3806 . . . . . . 7 (𝜑 → (𝐴 ∩ (𝐺𝑀)) = (𝐴 ∩ (𝐸𝑀)))
9998fveq2d 6182 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐺𝑀))) = (𝑂‘(𝐴 ∩ (𝐸𝑀))))
10053, 82, 993eqtr4d 2664 . . . . 5 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))
10139, 52, 1003eqtrd 2658 . . . 4 (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))
102101a1i 11 . . 3 (𝐾 ∈ (ℤ𝑀) → (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀)))))
103 simp3 1061 . . . . 5 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → 𝜑)
104 simp1 1059 . . . . 5 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → 𝑗 ∈ (𝑀..^𝐾))
105 id 22 . . . . . . 7 ((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))))
106105imp 445 . . . . . 6 (((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
1071063adant1 1077 . . . . 5 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
108 elfzouz 12458 . . . . . . . . 9 (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ (ℤ𝑀))
109108adantl 482 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝑗 ∈ (ℤ𝑀))
11040adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → 𝑂 ∈ OutMeas)
11142adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → 𝐴𝑋)
11243adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂𝐴) ∈ ℝ)
113 inss1 3825 . . . . . . . . . . . 12 (𝐴 ∩ (𝐹𝑛)) ⊆ 𝐴
114113a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝐴 ∩ (𝐹𝑛)) ⊆ 𝐴)
115110, 41, 111, 112, 114omessre 40487 . . . . . . . . . 10 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
116115recnd 10053 . . . . . . . . 9 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℂ)
117116adantlr 750 . . . . . . . 8 (((𝜑𝑗 ∈ (𝑀..^𝐾)) ∧ 𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℂ)
118 fveq2 6178 . . . . . . . . . 10 (𝑛 = (𝑗 + 1) → (𝐹𝑛) = (𝐹‘(𝑗 + 1)))
119118ineq2d 3806 . . . . . . . . 9 (𝑛 = (𝑗 + 1) → (𝐴 ∩ (𝐹𝑛)) = (𝐴 ∩ (𝐹‘(𝑗 + 1))))
120119fveq2d 6182 . . . . . . . 8 (𝑛 = (𝑗 + 1) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1)))))
121109, 117, 120fsump1 14468 . . . . . . 7 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
1221213adant3 1079 . . . . . 6 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
123 oveq1 6642 . . . . . . 7 𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))) → (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
1241233ad2ant3 1082 . . . . . 6 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
125 fzssp1 12369 . . . . . . . . . . . . . . . 16 (𝑀...𝑗) ⊆ (𝑀...(𝑗 + 1))
126 iunss1 4523 . . . . . . . . . . . . . . . 16 ((𝑀...𝑗) ⊆ (𝑀...(𝑗 + 1)) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
127125, 126ax-mp 5 . . . . . . . . . . . . . . 15 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖)
128127a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
12983a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖)))
130 oveq2 6643 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑗 → (𝑀...𝑛) = (𝑀...𝑗))
131130iuneq1d 4536 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
132131adantl 482 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = 𝑗) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
133108, 2syl6eleqr 2710 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝑗𝑍)
134 ovex 6663 . . . . . . . . . . . . . . . . . 18 (𝑀...𝑗) ∈ V
135134, 89iunex 7132 . . . . . . . . . . . . . . . . 17 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ V
136135a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ V)
137129, 132, 133, 136fvmptd 6275 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → (𝐺𝑗) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
138 oveq2 6643 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑗 + 1) → (𝑀...𝑛) = (𝑀...(𝑗 + 1)))
139138iuneq1d 4536 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑗 + 1) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
140139adantl 482 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = (𝑗 + 1)) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
141 peano2uz 11726 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (ℤ𝑀) → (𝑗 + 1) ∈ (ℤ𝑀))
142108, 141syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝐾) → (𝑗 + 1) ∈ (ℤ𝑀))
1432eqcomi 2629 . . . . . . . . . . . . . . . . 17 (ℤ𝑀) = 𝑍
144142, 143syl6eleq 2709 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → (𝑗 + 1) ∈ 𝑍)
145 ovex 6663 . . . . . . . . . . . . . . . . . 18 (𝑀...(𝑗 + 1)) ∈ V
146145, 89iunex 7132 . . . . . . . . . . . . . . . . 17 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖) ∈ V
147146a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖) ∈ V)
148129, 140, 144, 147fvmptd 6275 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → (𝐺‘(𝑗 + 1)) = 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
149137, 148sseq12d 3626 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → ((𝐺𝑗) ⊆ (𝐺‘(𝑗 + 1)) ↔ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖)))
150128, 149mpbird 247 . . . . . . . . . . . . 13 (𝑗 ∈ (𝑀..^𝐾) → (𝐺𝑗) ⊆ (𝐺‘(𝑗 + 1)))
151 inabs3 39044 . . . . . . . . . . . . 13 ((𝐺𝑗) ⊆ (𝐺‘(𝑗 + 1)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) = (𝐴 ∩ (𝐺𝑗)))
152150, 151syl 17 . . . . . . . . . . . 12 (𝑗 ∈ (𝑀..^𝐾) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) = (𝐴 ∩ (𝐺𝑗)))
153152fveq2d 6182 . . . . . . . . . . 11 (𝑗 ∈ (𝑀..^𝐾) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
154153eqcomd 2626 . . . . . . . . . 10 (𝑗 ∈ (𝑀..^𝐾) → (𝑂‘(𝐴 ∩ (𝐺𝑗))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))))
155154adantl 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘(𝐴 ∩ (𝐺𝑗))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))))
156 elfzoelz 12454 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ ℤ)
157 fzval3 12520 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℤ → (𝑀...𝑗) = (𝑀..^(𝑗 + 1)))
158156, 157syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝐾) → (𝑀...𝑗) = (𝑀..^(𝑗 + 1)))
159158eqcomd 2626 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → (𝑀..^(𝑗 + 1)) = (𝑀...𝑗))
160159iuneq1d 4536 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
161160difeq2d 3720 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
162161adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
16354a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖))))
164 fveq2 6178 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑗 + 1) → (𝐸𝑛) = (𝐸‘(𝑗 + 1)))
165 oveq2 6643 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑗 + 1) → (𝑀..^𝑛) = (𝑀..^(𝑗 + 1)))
166165iuneq1d 4536 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑗 + 1) → 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖))
167164, 166difeq12d 3721 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑗 + 1) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
168167adantl 482 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = (𝑗 + 1)) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
169 fvex 6188 . . . . . . . . . . . . . . . . 17 (𝐸‘(𝑗 + 1)) ∈ V
170 difexg 4799 . . . . . . . . . . . . . . . . 17 ((𝐸‘(𝑗 + 1)) ∈ V → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) ∈ V)
171169, 170ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) ∈ V
172171a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) ∈ V)
173163, 168, 144, 172fvmptd 6275 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → (𝐹‘(𝑗 + 1)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
174173adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐹‘(𝑗 + 1)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
175 nfcv 2762 . . . . . . . . . . . . . . . . . 18 𝑖(𝐸‘(𝑗 + 1))
176 fveq2 6178 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 + 1) → (𝐸𝑖) = (𝐸‘(𝑗 + 1)))
177175, 108, 176iunp1 39055 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖) = ( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))))
178148, 177eqtrd 2654 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → (𝐺‘(𝑗 + 1)) = ( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))))
179178, 137difeq12d 3721 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)) = (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
180 difundir 3872 . . . . . . . . . . . . . . . . 17 (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
181 difid 3939 . . . . . . . . . . . . . . . . . 18 ( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = ∅
182181uneq1i 3755 . . . . . . . . . . . . . . . . 17 (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))) = (∅ ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
183 0un 39035 . . . . . . . . . . . . . . . . 17 (∅ ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
184180, 182, 1833eqtri 2646 . . . . . . . . . . . . . . . 16 (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
185184a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
186179, 185eqtrd 2654 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
187186adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
188162, 174, 1873eqtr4d 2664 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐹‘(𝑗 + 1)) = ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)))
189188ineq2d 3806 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐹‘(𝑗 + 1))) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗))))
190 indif2 3862 . . . . . . . . . . . . 13 (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗))) = ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))
191190eqcomi 2629 . . . . . . . . . . . 12 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)))
192191a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗))))
193189, 192eqtr4d 2657 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐹‘(𝑗 + 1))) = ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))
194193fveq2d 6182 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1)))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))))
195155, 194oveq12d 6653 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
196 inss1 3825 . . . . . . . . . . . . . 14 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) ⊆ (𝐴 ∩ (𝐺‘(𝑗 + 1)))
197 inss1 3825 . . . . . . . . . . . . . 14 (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝐴
198196, 197sstri 3604 . . . . . . . . . . . . 13 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) ⊆ 𝐴
199198a1i 11 . . . . . . . . . . . 12 (𝜑 → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) ⊆ 𝐴)
20040, 41, 42, 43, 199omessre 40487 . . . . . . . . . . 11 (𝜑 → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) ∈ ℝ)
201200adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) ∈ ℝ)
20240adantr 481 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝑂 ∈ OutMeas)
20342adantr 481 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝐴𝑋)
20443adantr 481 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂𝐴) ∈ ℝ)
205 difss 3729 . . . . . . . . . . . . 13 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) ⊆ (𝐴 ∩ (𝐺‘(𝑗 + 1)))
206205, 197sstri 3604 . . . . . . . . . . . 12 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) ⊆ 𝐴
207206a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) ⊆ 𝐴)
208202, 41, 203, 204, 207omessre 40487 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))) ∈ ℝ)
209 rexadd 12048 . . . . . . . . . 10 (((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) ∈ ℝ ∧ (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))) ∈ ℝ) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
210201, 208, 209syl2anc 692 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
211210eqcomd 2626 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
212 carageniuncllem1.s . . . . . . . . 9 𝑆 = (CaraGen‘𝑂)
213137adantl 482 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐺𝑗) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
214 nfv 1841 . . . . . . . . . . . 12 𝑖𝜑
215 fzfid 12755 . . . . . . . . . . . 12 (𝜑 → (𝑀...𝑗) ∈ Fin)
216 carageniuncllem1.e . . . . . . . . . . . . . 14 (𝜑𝐸:𝑍𝑆)
217216adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀...𝑗)) → 𝐸:𝑍𝑆)
218 elfzuz 12323 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑗) → 𝑖 ∈ (ℤ𝑀))
219143a1i 11 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑗) → (ℤ𝑀) = 𝑍)
220218, 219eleqtrd 2701 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀...𝑗) → 𝑖𝑍)
221220adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀...𝑗)) → 𝑖𝑍)
222217, 221ffvelrnd 6346 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝑀...𝑗)) → (𝐸𝑖) ∈ 𝑆)
223214, 40, 212, 215, 222caragenfiiuncl 40492 . . . . . . . . . . 11 (𝜑 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ 𝑆)
224223adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ 𝑆)
225213, 224eqeltrd 2699 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐺𝑗) ∈ 𝑆)
22642ssinss1d 39034 . . . . . . . . . 10 (𝜑 → (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝑋)
227226adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝑋)
228202, 212, 41, 225, 227caragensplit 40477 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
229195, 211, 2283eqtrd 2658 . . . . . . 7 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
2302293adant3 1079 . . . . . 6 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
231122, 124, 2303eqtrd 2658 . . . . 5 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
232103, 104, 107, 231syl3anc 1324 . . . 4 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
2332323exp 1262 . . 3 (𝑗 ∈ (𝑀..^𝐾) → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → (𝜑 → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))))
23413, 20, 27, 34, 102, 233fzind2 12569 . 2 (𝐾 ∈ (𝑀...𝐾) → (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾)))))
2355, 6, 234sylc 65 1 (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1481  wcel 1988  Vcvv 3195  cdif 3564  cun 3565  cin 3566  wss 3567  c0 3907  {csn 4168   cuni 4427   ciun 4511  cmpt 4720  dom cdm 5104  wf 5872  cfv 5876  (class class class)co 6635  cc 9919  cr 9920  1c1 9922   + caddc 9924  cz 11362  cuz 11672   +𝑒 cxad 11929  ...cfz 12311  ..^cfzo 12449  Σcsu 14397  OutMeascome 40466  CaraGenccaragen 40468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-sup 8333  df-oi 8400  df-card 8750  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-n0 11278  df-z 11363  df-uz 11673  df-rp 11818  df-xadd 11932  df-ico 12166  df-icc 12167  df-fz 12312  df-fzo 12450  df-seq 12785  df-exp 12844  df-hash 13101  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-clim 14200  df-sum 14398  df-ome 40467  df-caragen 40469
This theorem is referenced by:  carageniuncllem2  40499
  Copyright terms: Public domain W3C validator