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 41056
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 2740 . . 3 (𝜑𝐾 ∈ (ℤ𝑀))
4 eluzfz2 12387 . . 3 (𝐾 ∈ (ℤ𝑀) → 𝐾 ∈ (𝑀...𝐾))
53, 4syl 17 . 2 (𝜑𝐾 ∈ (𝑀...𝐾))
6 id 22 . 2 (𝜑𝜑)
7 oveq2 6698 . . . . . 6 (𝑘 = 𝑀 → (𝑀...𝑘) = (𝑀...𝑀))
87sumeq1d 14475 . . . . 5 (𝑘 = 𝑀 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))))
9 fveq2 6229 . . . . . . 7 (𝑘 = 𝑀 → (𝐺𝑘) = (𝐺𝑀))
109ineq2d 3847 . . . . . 6 (𝑘 = 𝑀 → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺𝑀)))
1110fveq2d 6233 . . . . 5 (𝑘 = 𝑀 → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))
128, 11eqeq12d 2666 . . . 4 (𝑘 = 𝑀 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀)))))
1312imbi2d 329 . . 3 (𝑘 = 𝑀 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))))
14 oveq2 6698 . . . . . 6 (𝑘 = 𝑗 → (𝑀...𝑘) = (𝑀...𝑗))
1514sumeq1d 14475 . . . . 5 (𝑘 = 𝑗 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))))
16 fveq2 6229 . . . . . . 7 (𝑘 = 𝑗 → (𝐺𝑘) = (𝐺𝑗))
1716ineq2d 3847 . . . . . 6 (𝑘 = 𝑗 → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺𝑗)))
1817fveq2d 6233 . . . . 5 (𝑘 = 𝑗 → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
1915, 18eqeq12d 2666 . . . 4 (𝑘 = 𝑗 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))))
2019imbi2d 329 . . 3 (𝑘 = 𝑗 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))))
21 oveq2 6698 . . . . . 6 (𝑘 = (𝑗 + 1) → (𝑀...𝑘) = (𝑀...(𝑗 + 1)))
2221sumeq1d 14475 . . . . 5 (𝑘 = (𝑗 + 1) → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))))
23 fveq2 6229 . . . . . . 7 (𝑘 = (𝑗 + 1) → (𝐺𝑘) = (𝐺‘(𝑗 + 1)))
2423ineq2d 3847 . . . . . 6 (𝑘 = (𝑗 + 1) → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺‘(𝑗 + 1))))
2524fveq2d 6233 . . . . 5 (𝑘 = (𝑗 + 1) → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
2622, 25eqeq12d 2666 . . . 4 (𝑘 = (𝑗 + 1) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1))))))
2726imbi2d 329 . . 3 (𝑘 = (𝑗 + 1) → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))))
28 oveq2 6698 . . . . . 6 (𝑘 = 𝐾 → (𝑀...𝑘) = (𝑀...𝐾))
2928sumeq1d 14475 . . . . 5 (𝑘 = 𝐾 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))))
30 fveq2 6229 . . . . . . 7 (𝑘 = 𝐾 → (𝐺𝑘) = (𝐺𝐾))
3130ineq2d 3847 . . . . . 6 (𝑘 = 𝐾 → (𝐴 ∩ (𝐺𝑘)) = (𝐴 ∩ (𝐺𝐾)))
3231fveq2d 6233 . . . . 5 (𝑘 = 𝐾 → (𝑂‘(𝐴 ∩ (𝐺𝑘))) = (𝑂‘(𝐴 ∩ (𝐺𝐾))))
3329, 32eqeq12d 2666 . . . 4 (𝑘 = 𝐾 → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))) ↔ Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾)))))
3433imbi2d 329 . . 3 (𝑘 = 𝐾 → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘)))) ↔ (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾))))))
35 eluzel2 11730 . . . . . . . 8 (𝐾 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
363, 35syl 17 . . . . . . 7 (𝜑𝑀 ∈ ℤ)
37 fzsn 12421 . . . . . . 7 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
3836, 37syl 17 . . . . . 6 (𝜑 → (𝑀...𝑀) = {𝑀})
3938sumeq1d 14475 . . . . 5 (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹𝑛))))
40 carageniuncllem1.o . . . . . . . 8 (𝜑𝑂 ∈ OutMeas)
41 carageniuncllem1.x . . . . . . . 8 𝑋 = dom 𝑂
42 carageniuncllem1.a . . . . . . . 8 (𝜑𝐴𝑋)
43 carageniuncllem1.re . . . . . . . 8 (𝜑 → (𝑂𝐴) ∈ ℝ)
44 inss1 3866 . . . . . . . . 9 (𝐴 ∩ (𝐹𝑀)) ⊆ 𝐴
4544a1i 11 . . . . . . . 8 (𝜑 → (𝐴 ∩ (𝐹𝑀)) ⊆ 𝐴)
4640, 41, 42, 43, 45omessre 41045 . . . . . . 7 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) ∈ ℝ)
4746recnd 10106 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) ∈ ℂ)
48 fveq2 6229 . . . . . . . . 9 (𝑛 = 𝑀 → (𝐹𝑛) = (𝐹𝑀))
4948ineq2d 3847 . . . . . . . 8 (𝑛 = 𝑀 → (𝐴 ∩ (𝐹𝑛)) = (𝐴 ∩ (𝐹𝑀)))
5049fveq2d 6233 . . . . . . 7 (𝑛 = 𝑀 → (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹𝑀))))
5150sumsn 14519 . . . . . 6 ((𝑀 ∈ ℤ ∧ (𝑂‘(𝐴 ∩ (𝐹𝑀))) ∈ ℂ) → Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹𝑀))))
5236, 47, 51syl2anc 694 . . . . 5 (𝜑 → Σ𝑛 ∈ {𝑀} (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹𝑀))))
53 eqidd 2652 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐸𝑀))) = (𝑂‘(𝐴 ∩ (𝐸𝑀))))
54 carageniuncllem1.f . . . . . . . . . . 11 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)))
5554a1i 11 . . . . . . . . . 10 (𝜑𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖))))
56 fveq2 6229 . . . . . . . . . . . 12 (𝑛 = 𝑀 → (𝐸𝑛) = (𝐸𝑀))
57 oveq2 6698 . . . . . . . . . . . . 13 (𝑛 = 𝑀 → (𝑀..^𝑛) = (𝑀..^𝑀))
5857iuneq1d 4577 . . . . . . . . . . . 12 (𝑛 = 𝑀 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖))
5956, 58difeq12d 3762 . . . . . . . . . . 11 (𝑛 = 𝑀 → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)))
6059adantl 481 . . . . . . . . . 10 ((𝜑𝑛 = 𝑀) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)))
61 uzid 11740 . . . . . . . . . . . 12 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
6236, 61syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ (ℤ𝑀))
632a1i 11 . . . . . . . . . . . 12 (𝜑𝑍 = (ℤ𝑀))
6463eqcomd 2657 . . . . . . . . . . 11 (𝜑 → (ℤ𝑀) = 𝑍)
6562, 64eleqtrd 2732 . . . . . . . . . 10 (𝜑𝑀𝑍)
66 fvex 6239 . . . . . . . . . . . 12 (𝐸𝑀) ∈ V
67 difexg 4841 . . . . . . . . . . . 12 ((𝐸𝑀) ∈ V → ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) ∈ V)
6866, 67ax-mp 5 . . . . . . . . . . 11 ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) ∈ V
6968a1i 11 . . . . . . . . . 10 (𝜑 → ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) ∈ V)
7055, 60, 65, 69fvmptd 6327 . . . . . . . . 9 (𝜑 → (𝐹𝑀) = ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)))
71 fzo0 12531 . . . . . . . . . . . . 13 (𝑀..^𝑀) = ∅
72 iuneq1 4566 . . . . . . . . . . . . 13 ((𝑀..^𝑀) = ∅ → 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖) = 𝑖 ∈ ∅ (𝐸𝑖))
7371, 72ax-mp 5 . . . . . . . . . . . 12 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖) = 𝑖 ∈ ∅ (𝐸𝑖)
74 0iun 4609 . . . . . . . . . . . 12 𝑖 ∈ ∅ (𝐸𝑖) = ∅
7573, 74eqtri 2673 . . . . . . . . . . 11 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖) = ∅
7675difeq2i 3758 . . . . . . . . . 10 ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) = ((𝐸𝑀) ∖ ∅)
7776a1i 11 . . . . . . . . 9 (𝜑 → ((𝐸𝑀) ∖ 𝑖 ∈ (𝑀..^𝑀)(𝐸𝑖)) = ((𝐸𝑀) ∖ ∅))
78 dif0 3983 . . . . . . . . . 10 ((𝐸𝑀) ∖ ∅) = (𝐸𝑀)
7978a1i 11 . . . . . . . . 9 (𝜑 → ((𝐸𝑀) ∖ ∅) = (𝐸𝑀))
8070, 77, 793eqtrd 2689 . . . . . . . 8 (𝜑 → (𝐹𝑀) = (𝐸𝑀))
8180ineq2d 3847 . . . . . . 7 (𝜑 → (𝐴 ∩ (𝐹𝑀)) = (𝐴 ∩ (𝐸𝑀)))
8281fveq2d 6233 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) = (𝑂‘(𝐴 ∩ (𝐸𝑀))))
83 carageniuncllem1.g . . . . . . . . . . 11 𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖))
8483a1i 11 . . . . . . . . . 10 (𝜑𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖)))
85 oveq2 6698 . . . . . . . . . . . 12 (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
8685iuneq1d 4577 . . . . . . . . . . 11 (𝑛 = 𝑀 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
8786adantl 481 . . . . . . . . . 10 ((𝜑𝑛 = 𝑀) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
88 ovex 6718 . . . . . . . . . . . 12 (𝑀...𝑀) ∈ V
89 fvex 6239 . . . . . . . . . . . 12 (𝐸𝑖) ∈ V
9088, 89iunex 7189 . . . . . . . . . . 11 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) ∈ V
9190a1i 11 . . . . . . . . . 10 (𝜑 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) ∈ V)
9284, 87, 65, 91fvmptd 6327 . . . . . . . . 9 (𝜑 → (𝐺𝑀) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
9338iuneq1d 4577 . . . . . . . . 9 (𝜑 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) = 𝑖 ∈ {𝑀} (𝐸𝑖))
94 fveq2 6229 . . . . . . . . . . 11 (𝑖 = 𝑀 → (𝐸𝑖) = (𝐸𝑀))
9594iunxsng 4634 . . . . . . . . . 10 (𝑀 ∈ ℤ → 𝑖 ∈ {𝑀} (𝐸𝑖) = (𝐸𝑀))
9636, 95syl 17 . . . . . . . . 9 (𝜑 𝑖 ∈ {𝑀} (𝐸𝑖) = (𝐸𝑀))
9792, 93, 963eqtrd 2689 . . . . . . . 8 (𝜑 → (𝐺𝑀) = (𝐸𝑀))
9897ineq2d 3847 . . . . . . 7 (𝜑 → (𝐴 ∩ (𝐺𝑀)) = (𝐴 ∩ (𝐸𝑀)))
9998fveq2d 6233 . . . . . 6 (𝜑 → (𝑂‘(𝐴 ∩ (𝐺𝑀))) = (𝑂‘(𝐴 ∩ (𝐸𝑀))))
10053, 82, 993eqtr4d 2695 . . . . 5 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑀))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))
10139, 52, 1003eqtrd 2689 . . . 4 (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀))))
102101a1i 11 . . 3 (𝐾 ∈ (ℤ𝑀) → (𝜑 → Σ𝑛 ∈ (𝑀...𝑀)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑀)))))
103 simp3 1083 . . . . 5 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → 𝜑)
104 simp1 1081 . . . . 5 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → 𝑗 ∈ (𝑀..^𝐾))
105 id 22 . . . . . . 7 ((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))))
106105imp 444 . . . . . 6 (((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
1071063adant1 1099 . . . . 5 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
108 elfzouz 12513 . . . . . . . . 9 (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ (ℤ𝑀))
109108adantl 481 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝑗 ∈ (ℤ𝑀))
11040adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → 𝑂 ∈ OutMeas)
11142adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → 𝐴𝑋)
11243adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂𝐴) ∈ ℝ)
113 inss1 3866 . . . . . . . . . . . 12 (𝐴 ∩ (𝐹𝑛)) ⊆ 𝐴
114113a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝐴 ∩ (𝐹𝑛)) ⊆ 𝐴)
115110, 41, 111, 112, 114omessre 41045 . . . . . . . . . 10 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
116115recnd 10106 . . . . . . . . 9 ((𝜑𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℂ)
117116adantlr 751 . . . . . . . 8 (((𝜑𝑗 ∈ (𝑀..^𝐾)) ∧ 𝑛 ∈ (𝑀...(𝑗 + 1))) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℂ)
118 fveq2 6229 . . . . . . . . . 10 (𝑛 = (𝑗 + 1) → (𝐹𝑛) = (𝐹‘(𝑗 + 1)))
119118ineq2d 3847 . . . . . . . . 9 (𝑛 = (𝑗 + 1) → (𝐴 ∩ (𝐹𝑛)) = (𝐴 ∩ (𝐹‘(𝑗 + 1))))
120119fveq2d 6233 . . . . . . . 8 (𝑛 = (𝑗 + 1) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1)))))
121109, 117, 120fsump1 14531 . . . . . . 7 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
1221213adant3 1101 . . . . . 6 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
123 oveq1 6697 . . . . . . 7 𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))) → (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
1241233ad2ant3 1104 . . . . . 6 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → (Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))))
125 fzssp1 12422 . . . . . . . . . . . . . . . 16 (𝑀...𝑗) ⊆ (𝑀...(𝑗 + 1))
126 iunss1 4564 . . . . . . . . . . . . . . . 16 ((𝑀...𝑗) ⊆ (𝑀...(𝑗 + 1)) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
127125, 126ax-mp 5 . . . . . . . . . . . . . . 15 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖)
128127a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
12983a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖)))
130 oveq2 6698 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑗 → (𝑀...𝑛) = (𝑀...𝑗))
131130iuneq1d 4577 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
132131adantl 481 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = 𝑗) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
133108, 2syl6eleqr 2741 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝑗𝑍)
134 ovex 6718 . . . . . . . . . . . . . . . . . 18 (𝑀...𝑗) ∈ V
135134, 89iunex 7189 . . . . . . . . . . . . . . . . 17 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ V
136135a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ V)
137129, 132, 133, 136fvmptd 6327 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → (𝐺𝑗) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
138 oveq2 6698 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑗 + 1) → (𝑀...𝑛) = (𝑀...(𝑗 + 1)))
139138iuneq1d 4577 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑗 + 1) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
140139adantl 481 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = (𝑗 + 1)) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
141 peano2uz 11779 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (ℤ𝑀) → (𝑗 + 1) ∈ (ℤ𝑀))
142108, 141syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝐾) → (𝑗 + 1) ∈ (ℤ𝑀))
1432eqcomi 2660 . . . . . . . . . . . . . . . . 17 (ℤ𝑀) = 𝑍
144142, 143syl6eleq 2740 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → (𝑗 + 1) ∈ 𝑍)
145 ovex 6718 . . . . . . . . . . . . . . . . . 18 (𝑀...(𝑗 + 1)) ∈ V
146145, 89iunex 7189 . . . . . . . . . . . . . . . . 17 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖) ∈ V
147146a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖) ∈ V)
148129, 140, 144, 147fvmptd 6327 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → (𝐺‘(𝑗 + 1)) = 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖))
149137, 148sseq12d 3667 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → ((𝐺𝑗) ⊆ (𝐺‘(𝑗 + 1)) ↔ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ⊆ 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖)))
150128, 149mpbird 247 . . . . . . . . . . . . 13 (𝑗 ∈ (𝑀..^𝐾) → (𝐺𝑗) ⊆ (𝐺‘(𝑗 + 1)))
151 inabs3 39538 . . . . . . . . . . . . 13 ((𝐺𝑗) ⊆ (𝐺‘(𝑗 + 1)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) = (𝐴 ∩ (𝐺𝑗)))
152150, 151syl 17 . . . . . . . . . . . 12 (𝑗 ∈ (𝑀..^𝐾) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) = (𝐴 ∩ (𝐺𝑗)))
153152fveq2d 6233 . . . . . . . . . . 11 (𝑗 ∈ (𝑀..^𝐾) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) = (𝑂‘(𝐴 ∩ (𝐺𝑗))))
154153eqcomd 2657 . . . . . . . . . 10 (𝑗 ∈ (𝑀..^𝐾) → (𝑂‘(𝐴 ∩ (𝐺𝑗))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))))
155154adantl 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘(𝐴 ∩ (𝐺𝑗))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))))
156 elfzoelz 12509 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ ℤ)
157 fzval3 12576 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℤ → (𝑀...𝑗) = (𝑀..^(𝑗 + 1)))
158156, 157syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝐾) → (𝑀...𝑗) = (𝑀..^(𝑗 + 1)))
159158eqcomd 2657 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → (𝑀..^(𝑗 + 1)) = (𝑀...𝑗))
160159iuneq1d 4577 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
161160difeq2d 3761 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
162161adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
16354a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖))))
164 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑗 + 1) → (𝐸𝑛) = (𝐸‘(𝑗 + 1)))
165 oveq2 6698 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑗 + 1) → (𝑀..^𝑛) = (𝑀..^(𝑗 + 1)))
166165iuneq1d 4577 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑗 + 1) → 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖))
167164, 166difeq12d 3762 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑗 + 1) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
168167adantl 481 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (𝑀..^𝐾) ∧ 𝑛 = (𝑗 + 1)) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
169 fvex 6239 . . . . . . . . . . . . . . . . 17 (𝐸‘(𝑗 + 1)) ∈ V
170 difexg 4841 . . . . . . . . . . . . . . . . 17 ((𝐸‘(𝑗 + 1)) ∈ V → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) ∈ V)
171169, 170ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) ∈ V
172171a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)) ∈ V)
173163, 168, 144, 172fvmptd 6327 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → (𝐹‘(𝑗 + 1)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
174173adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐹‘(𝑗 + 1)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀..^(𝑗 + 1))(𝐸𝑖)))
175 nfcv 2793 . . . . . . . . . . . . . . . . . 18 𝑖(𝐸‘(𝑗 + 1))
176 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 + 1) → (𝐸𝑖) = (𝐸‘(𝑗 + 1)))
177175, 108, 176iunp1 39549 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝐾) → 𝑖 ∈ (𝑀...(𝑗 + 1))(𝐸𝑖) = ( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))))
178148, 177eqtrd 2685 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (𝑀..^𝐾) → (𝐺‘(𝑗 + 1)) = ( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))))
179178, 137difeq12d 3762 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)) = (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
180 difundir 3913 . . . . . . . . . . . . . . . . 17 (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
181 difid 3981 . . . . . . . . . . . . . . . . . 18 ( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = ∅
182181uneq1i 3796 . . . . . . . . . . . . . . . . 17 (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))) = (∅ ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
183 0un 39529 . . . . . . . . . . . . . . . . 17 (∅ ∪ ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
184180, 182, 1833eqtri 2677 . . . . . . . . . . . . . . . 16 (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
185184a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (𝑀..^𝐾) → (( 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∪ (𝐸‘(𝑗 + 1))) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
186179, 185eqtrd 2685 . . . . . . . . . . . . . 14 (𝑗 ∈ (𝑀..^𝐾) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
187186adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)) = ((𝐸‘(𝑗 + 1)) ∖ 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖)))
188162, 174, 1873eqtr4d 2695 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐹‘(𝑗 + 1)) = ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)))
189188ineq2d 3847 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐹‘(𝑗 + 1))) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗))))
190 indif2 3903 . . . . . . . . . . . . 13 (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗))) = ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))
191190eqcomi 2660 . . . . . . . . . . . 12 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗)))
192191a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) = (𝐴 ∩ ((𝐺‘(𝑗 + 1)) ∖ (𝐺𝑗))))
193189, 192eqtr4d 2688 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐹‘(𝑗 + 1))) = ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))
194193fveq2d 6233 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1)))) = (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))))
195155, 194oveq12d 6708 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
196 inss1 3866 . . . . . . . . . . . . . 14 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) ⊆ (𝐴 ∩ (𝐺‘(𝑗 + 1)))
197 inss1 3866 . . . . . . . . . . . . . 14 (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝐴
198196, 197sstri 3645 . . . . . . . . . . . . 13 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) ⊆ 𝐴
199198a1i 11 . . . . . . . . . . . 12 (𝜑 → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗)) ⊆ 𝐴)
20040, 41, 42, 43, 199omessre 41045 . . . . . . . . . . 11 (𝜑 → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) ∈ ℝ)
201200adantr 480 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) ∈ ℝ)
20240adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝑂 ∈ OutMeas)
20342adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝐴𝑋)
20443adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂𝐴) ∈ ℝ)
205 difss 3770 . . . . . . . . . . . . 13 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) ⊆ (𝐴 ∩ (𝐺‘(𝑗 + 1)))
206205, 197sstri 3645 . . . . . . . . . . . 12 ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) ⊆ 𝐴
207206a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)) ⊆ 𝐴)
208202, 41, 203, 204, 207omessre 41045 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))) ∈ ℝ)
209 rexadd 12101 . . . . . . . . . 10 (((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) ∈ ℝ ∧ (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗))) ∈ ℝ) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
210201, 208, 209syl2anc 694 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
211210eqcomd 2657 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) + (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))))
212 carageniuncllem1.s . . . . . . . . 9 𝑆 = (CaraGen‘𝑂)
213137adantl 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐺𝑗) = 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖))
214 nfv 1883 . . . . . . . . . . . 12 𝑖𝜑
215 fzfid 12812 . . . . . . . . . . . 12 (𝜑 → (𝑀...𝑗) ∈ Fin)
216 carageniuncllem1.e . . . . . . . . . . . . . 14 (𝜑𝐸:𝑍𝑆)
217216adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀...𝑗)) → 𝐸:𝑍𝑆)
218 elfzuz 12376 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑗) → 𝑖 ∈ (ℤ𝑀))
219143a1i 11 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑗) → (ℤ𝑀) = 𝑍)
220218, 219eleqtrd 2732 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀...𝑗) → 𝑖𝑍)
221220adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀...𝑗)) → 𝑖𝑍)
222217, 221ffvelrnd 6400 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝑀...𝑗)) → (𝐸𝑖) ∈ 𝑆)
223214, 40, 212, 215, 222caragenfiiuncl 41050 . . . . . . . . . . 11 (𝜑 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ 𝑆)
224223adantr 480 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → 𝑖 ∈ (𝑀...𝑗)(𝐸𝑖) ∈ 𝑆)
225213, 224eqeltrd 2730 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐺𝑗) ∈ 𝑆)
22642ssinss1d 39528 . . . . . . . . . 10 (𝜑 → (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝑋)
227226adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → (𝐴 ∩ (𝐺‘(𝑗 + 1))) ⊆ 𝑋)
228202, 212, 41, 225, 227caragensplit 41035 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∩ (𝐺𝑗))) +𝑒 (𝑂‘((𝐴 ∩ (𝐺‘(𝑗 + 1))) ∖ (𝐺𝑗)))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
229195, 211, 2283eqtrd 2689 . . . . . . 7 ((𝜑𝑗 ∈ (𝑀..^𝐾)) → ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
2302293adant3 1101 . . . . . 6 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → ((𝑂‘(𝐴 ∩ (𝐺𝑗))) + (𝑂‘(𝐴 ∩ (𝐹‘(𝑗 + 1))))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
231122, 124, 2303eqtrd 2689 . . . . 5 ((𝜑𝑗 ∈ (𝑀..^𝐾) ∧ Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
232103, 104, 107, 231syl3anc 1366 . . . 4 ((𝑗 ∈ (𝑀..^𝐾) ∧ (𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) ∧ 𝜑) → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))
2332323exp 1283 . . 3 (𝑗 ∈ (𝑀..^𝐾) → ((𝜑 → Σ𝑛 ∈ (𝑀...𝑗)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑗)))) → (𝜑 → Σ𝑛 ∈ (𝑀...(𝑗 + 1))(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘(𝑗 + 1)))))))
23413, 20, 27, 34, 102, 233fzind2 12626 . 2 (𝐾 ∈ (𝑀...𝐾) → (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾)))))
2355, 6, 234sylc 65 1 (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝐾))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054   = wceq 1523  wcel 2030  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  {csn 4210   cuni 4468   ciun 4552  cmpt 4762  dom cdm 5143  wf 5922  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  1c1 9975   + caddc 9977  cz 11415  cuz 11725   +𝑒 cxad 11982  ...cfz 12364  ..^cfzo 12504  Σcsu 14460  OutMeascome 41024  CaraGenccaragen 41026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-xadd 11985  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-ome 41025  df-caragen 41027
This theorem is referenced by:  carageniuncllem2  41057
  Copyright terms: Public domain W3C validator