MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniioombllem4 Structured version   Visualization version   GIF version

Theorem uniioombllem4 25606
Description: Lemma for uniioombl 25609. (Contributed by Mario Carneiro, 26-Mar-2015.)
Hypotheses
Ref Expression
uniioombl.1 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.2 (𝜑Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
uniioombl.3 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
uniioombl.a 𝐴 = ran ((,) ∘ 𝐹)
uniioombl.e (𝜑 → (vol*‘𝐸) ∈ ℝ)
uniioombl.c (𝜑𝐶 ∈ ℝ+)
uniioombl.g (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.s (𝜑𝐸 ran ((,) ∘ 𝐺))
uniioombl.t 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
uniioombl.v (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
uniioombl.m (𝜑𝑀 ∈ ℕ)
uniioombl.m2 (𝜑 → (abs‘((𝑇𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)
uniioombl.k 𝐾 = (((,) ∘ 𝐺) “ (1...𝑀))
uniioombl.n (𝜑𝑁 ∈ ℕ)
uniioombl.n2 (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
uniioombl.l 𝐿 = (((,) ∘ 𝐹) “ (1...𝑁))
Assertion
Ref Expression
uniioombllem4 (𝜑 → (vol*‘(𝐾𝐴)) ≤ ((vol*‘(𝐾𝐿)) + 𝐶))
Distinct variable groups:   𝑖,𝑗,𝑥,𝐹   𝑖,𝐺,𝑗,𝑥   𝑗,𝐾,𝑥   𝐴,𝑗,𝑥   𝐶,𝑖,𝑗,𝑥   𝑖,𝑀,𝑗,𝑥   𝑖,𝑁,𝑗   𝜑,𝑖,𝑗,𝑥   𝑇,𝑖,𝑗,𝑥
Allowed substitution hints:   𝐴(𝑖)   𝑆(𝑥,𝑖,𝑗)   𝐸(𝑥,𝑖,𝑗)   𝐾(𝑖)   𝐿(𝑥,𝑖,𝑗)   𝑁(𝑥)

Proof of Theorem uniioombllem4
StepHypRef Expression
1 inss1 4230 . . 3 (𝐾𝐴) ⊆ 𝐾
2 uniioombl.k . . . . 5 𝐾 = (((,) ∘ 𝐺) “ (1...𝑀))
3 imassrn 6080 . . . . . 6 (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ran ((,) ∘ 𝐺)
43unissi 4922 . . . . 5 (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ran ((,) ∘ 𝐺)
52, 4eqsstri 4014 . . . 4 𝐾 ran ((,) ∘ 𝐺)
6 uniioombl.g . . . . . . 7 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
76uniiccdif 25598 . . . . . 6 (𝜑 → ( ran ((,) ∘ 𝐺) ⊆ ran ([,] ∘ 𝐺) ∧ (vol*‘( ran ([,] ∘ 𝐺) ∖ ran ((,) ∘ 𝐺))) = 0))
87simpld 493 . . . . 5 (𝜑 ran ((,) ∘ 𝐺) ⊆ ran ([,] ∘ 𝐺))
9 ovolficcss 25489 . . . . . 6 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐺) ⊆ ℝ)
106, 9syl 17 . . . . 5 (𝜑 ran ([,] ∘ 𝐺) ⊆ ℝ)
118, 10sstrd 3990 . . . 4 (𝜑 ran ((,) ∘ 𝐺) ⊆ ℝ)
125, 11sstrid 3991 . . 3 (𝜑𝐾 ⊆ ℝ)
13 uniioombl.1 . . . . . 6 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
14 uniioombl.2 . . . . . 6 (𝜑Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
15 uniioombl.3 . . . . . 6 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
16 uniioombl.a . . . . . 6 𝐴 = ran ((,) ∘ 𝐹)
17 uniioombl.e . . . . . 6 (𝜑 → (vol*‘𝐸) ∈ ℝ)
18 uniioombl.c . . . . . 6 (𝜑𝐶 ∈ ℝ+)
19 uniioombl.s . . . . . 6 (𝜑𝐸 ran ((,) ∘ 𝐺))
20 uniioombl.t . . . . . 6 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
21 uniioombl.v . . . . . 6 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
2213, 14, 15, 16, 17, 18, 6, 19, 20, 21uniioombllem1 25601 . . . . 5 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
23 ssid 4002 . . . . . 6 ran ((,) ∘ 𝐺) ⊆ ran ((,) ∘ 𝐺)
2420ovollb 25499 . . . . . 6 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ran ((,) ∘ 𝐺) ⊆ ran ((,) ∘ 𝐺)) → (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
256, 23, 24sylancl 584 . . . . 5 (𝜑 → (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
26 ovollecl 25503 . . . . 5 (( ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ ∧ (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < )) → (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ)
2711, 22, 25, 26syl3anc 1368 . . . 4 (𝜑 → (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ)
28 ovolsscl 25506 . . . 4 ((𝐾 ran ((,) ∘ 𝐺) ∧ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘𝐾) ∈ ℝ)
295, 11, 27, 28mp3an2i 1463 . . 3 (𝜑 → (vol*‘𝐾) ∈ ℝ)
30 ovolsscl 25506 . . 3 (((𝐾𝐴) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘(𝐾𝐴)) ∈ ℝ)
311, 12, 29, 30mp3an2i 1463 . 2 (𝜑 → (vol*‘(𝐾𝐴)) ∈ ℝ)
32 inss1 4230 . . . 4 (𝐾𝐿) ⊆ 𝐾
33 ovolsscl 25506 . . . 4 (((𝐾𝐿) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘(𝐾𝐿)) ∈ ℝ)
3432, 12, 29, 33mp3an2i 1463 . . 3 (𝜑 → (vol*‘(𝐾𝐿)) ∈ ℝ)
35 ssun2 4174 . . . . . 6 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
36 nnuz 12917 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
37 uniioombl.n . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℕ)
3837peano2nnd 12281 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ ℕ)
3938, 36eleqtrdi 2836 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
40 uzsplit 13627 . . . . . . . . . . . . . . 15 ((𝑁 + 1) ∈ (ℤ‘1) → (ℤ‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
4139, 40syl 17 . . . . . . . . . . . . . 14 (𝜑 → (ℤ‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
4236, 41eqtrid 2778 . . . . . . . . . . . . 13 (𝜑 → ℕ = ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
4337nncnd 12280 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℂ)
44 ax-1cn 11216 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
45 pncan 11516 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
4643, 44, 45sylancl 584 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
4746oveq2d 7440 . . . . . . . . . . . . . 14 (𝜑 → (1...((𝑁 + 1) − 1)) = (1...𝑁))
4847uneq1d 4162 . . . . . . . . . . . . 13 (𝜑 → ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))) = ((1...𝑁) ∪ (ℤ‘(𝑁 + 1))))
4942, 48eqtrd 2766 . . . . . . . . . . . 12 (𝜑 → ℕ = ((1...𝑁) ∪ (ℤ‘(𝑁 + 1))))
5049iuneq1d 5028 . . . . . . . . . . 11 (𝜑 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) = 𝑖 ∈ ((1...𝑁) ∪ (ℤ‘(𝑁 + 1)))((,)‘(𝐹𝑖)))
51 iunxun 5102 . . . . . . . . . . 11 𝑖 ∈ ((1...𝑁) ∪ (ℤ‘(𝑁 + 1)))((,)‘(𝐹𝑖)) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∪ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
5250, 51eqtrdi 2782 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∪ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
53 ioof 13478 . . . . . . . . . . . . . 14 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
54 inss2 4231 . . . . . . . . . . . . . . . 16 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
55 rexpssxrxp 11309 . . . . . . . . . . . . . . . 16 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
5654, 55sstri 3989 . . . . . . . . . . . . . . 15 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
57 fss 6744 . . . . . . . . . . . . . . 15 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* × ℝ*))
5813, 56, 57sylancl 584 . . . . . . . . . . . . . 14 (𝜑𝐹:ℕ⟶(ℝ* × ℝ*))
59 fco 6752 . . . . . . . . . . . . . 14 (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
6053, 58, 59sylancr 585 . . . . . . . . . . . . 13 (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
61 ffn 6728 . . . . . . . . . . . . 13 (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → ((,) ∘ 𝐹) Fn ℕ)
62 fniunfv 7262 . . . . . . . . . . . . 13 (((,) ∘ 𝐹) Fn ℕ → 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ran ((,) ∘ 𝐹))
6360, 61, 623syl 18 . . . . . . . . . . . 12 (𝜑 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ran ((,) ∘ 𝐹))
64 fvco3 7001 . . . . . . . . . . . . . 14 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹𝑖)))
6513, 64sylan 578 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹𝑖)))
6665iuneq2dv 5025 . . . . . . . . . . . 12 (𝜑 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
6763, 66eqtr3d 2768 . . . . . . . . . . 11 (𝜑 ran ((,) ∘ 𝐹) = 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
6816, 67eqtrid 2778 . . . . . . . . . 10 (𝜑𝐴 = 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
69 uniioombl.l . . . . . . . . . . . 12 𝐿 = (((,) ∘ 𝐹) “ (1...𝑁))
70 ffun 6731 . . . . . . . . . . . . . 14 (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐹))
71 funiunfv 7263 . . . . . . . . . . . . . 14 (Fun ((,) ∘ 𝐹) → 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = (((,) ∘ 𝐹) “ (1...𝑁)))
7260, 70, 713syl 18 . . . . . . . . . . . . 13 (𝜑 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = (((,) ∘ 𝐹) “ (1...𝑁)))
73 elfznn 13584 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑁) → 𝑖 ∈ ℕ)
7413, 73, 64syl2an 594 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹𝑖)))
7574iuneq2dv 5025 . . . . . . . . . . . . 13 (𝜑 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
7672, 75eqtr3d 2768 . . . . . . . . . . . 12 (𝜑 (((,) ∘ 𝐹) “ (1...𝑁)) = 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
7769, 76eqtrid 2778 . . . . . . . . . . 11 (𝜑𝐿 = 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
7877uneq1d 4162 . . . . . . . . . 10 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∪ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
7952, 68, 783eqtr4d 2776 . . . . . . . . 9 (𝜑𝐴 = (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
8079ineq2d 4213 . . . . . . . 8 (𝜑 → (𝐾𝐴) = (𝐾 ∩ (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))))
81 indi 4275 . . . . . . . 8 (𝐾 ∩ (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))) = ((𝐾𝐿) ∪ (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
8280, 81eqtrdi 2782 . . . . . . 7 (𝜑 → (𝐾𝐴) = ((𝐾𝐿) ∪ (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))))
83 fss 6744 . . . . . . . . . . . . . . 15 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* × ℝ*))
846, 56, 83sylancl 584 . . . . . . . . . . . . . 14 (𝜑𝐺:ℕ⟶(ℝ* × ℝ*))
85 fco 6752 . . . . . . . . . . . . . 14 (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
8653, 84, 85sylancr 585 . . . . . . . . . . . . 13 (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
87 ffun 6731 . . . . . . . . . . . . 13 (((,) ∘ 𝐺):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐺))
88 funiunfv 7263 . . . . . . . . . . . . 13 (Fun ((,) ∘ 𝐺) → 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = (((,) ∘ 𝐺) “ (1...𝑀)))
8986, 87, 883syl 18 . . . . . . . . . . . 12 (𝜑 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = (((,) ∘ 𝐺) “ (1...𝑀)))
90 elfznn 13584 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
91 fvco3 7001 . . . . . . . . . . . . . 14 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺𝑗)))
926, 90, 91syl2an 594 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺𝑗)))
9392iuneq2dv 5025 . . . . . . . . . . . 12 (𝜑 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
9489, 93eqtr3d 2768 . . . . . . . . . . 11 (𝜑 (((,) ∘ 𝐺) “ (1...𝑀)) = 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
952, 94eqtrid 2778 . . . . . . . . . 10 (𝜑𝐾 = 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
9695ineq2d 4213 . . . . . . . . 9 (𝜑 → ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝐾) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗))))
97 incom 4202 . . . . . . . . 9 (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝐾)
98 iunin2 5079 . . . . . . . . . . . . 13 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
99 incom 4202 . . . . . . . . . . . . . . 15 (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖)))
10099a1i 11 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ‘(𝑁 + 1)) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))))
101100iuneq2i 5022 . . . . . . . . . . . . 13 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖)))
102 incom 4202 . . . . . . . . . . . . 13 ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
10398, 101, 1023eqtr4ri 2765 . . . . . . . . . . . 12 ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))
104103a1i 11 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑀) → ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
105104iuneq2i 5022 . . . . . . . . . 10 𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))
106 iunin2 5079 . . . . . . . . . 10 𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
107105, 106eqtr3i 2756 . . . . . . . . 9 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
10896, 97, 1073eqtr4g 2791 . . . . . . . 8 (𝜑 → (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
109108uneq2d 4163 . . . . . . 7 (𝜑 → ((𝐾𝐿) ∪ (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))) = ((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
11082, 109eqtrd 2766 . . . . . 6 (𝜑 → (𝐾𝐴) = ((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
11135, 110sseqtrrid 4033 . . . . 5 (𝜑 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ (𝐾𝐴))
112111, 1sstrdi 3992 . . . 4 (𝜑 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
113 ovolsscl 25506 . . . 4 (( 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
114112, 12, 29, 113syl3anc 1368 . . 3 (𝜑 → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
11534, 114readdcld 11293 . 2 (𝜑 → ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ∈ ℝ)
11618rpred 13070 . . 3 (𝜑𝐶 ∈ ℝ)
11734, 116readdcld 11293 . 2 (𝜑 → ((vol*‘(𝐾𝐿)) + 𝐶) ∈ ℝ)
118110fveq2d 6905 . . 3 (𝜑 → (vol*‘(𝐾𝐴)) = (vol*‘((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
11932, 12sstrid 3991 . . . 4 (𝜑 → (𝐾𝐿) ⊆ ℝ)
120112, 12sstrd 3990 . . . 4 (𝜑 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ)
121 ovolun 25519 . . . 4 ((((𝐾𝐿) ⊆ ℝ ∧ (vol*‘(𝐾𝐿)) ∈ ℝ) ∧ ( 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)) → (vol*‘((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
122119, 34, 120, 114, 121syl22anc 837 . . 3 (𝜑 → (vol*‘((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
123118, 122eqbrtrd 5175 . 2 (𝜑 → (vol*‘(𝐾𝐴)) ≤ ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
124 fzfid 13993 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
125 iunss 5053 . . . . . . . 8 ( 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾 ↔ ∀𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
126112, 125sylib 217 . . . . . . 7 (𝜑 → ∀𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
127126r19.21bi 3239 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
12812adantr 479 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → 𝐾 ⊆ ℝ)
12929adantr 479 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘𝐾) ∈ ℝ)
130 ovolsscl 25506 . . . . . 6 (( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
131127, 128, 129, 130syl3anc 1368 . . . . 5 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
132124, 131fsumrecl 15738 . . . 4 (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
133127, 128sstrd 3990 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ)
134133, 131jca 510 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → ( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
135134ralrimiva 3136 . . . . 5 (𝜑 → ∀𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
136 ovolfiniun 25521 . . . . 5 (((1...𝑀) ∈ Fin ∧ ∀𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)) → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
137124, 135, 136syl2anc 582 . . . 4 (𝜑 → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
138 uniioombl.m . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
139116, 138nndivred 12318 . . . . . . 7 (𝜑 → (𝐶 / 𝑀) ∈ ℝ)
140139adantr 479 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐶 / 𝑀) ∈ ℝ)
14177ineq2d 4213 . . . . . . . . . . . . 13 (𝜑 → (((,)‘(𝐺𝑗)) ∩ 𝐿) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖))))
142141adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖))))
14399a1i 11 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑁) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))))
144143iuneq2i 5022 . . . . . . . . . . . . 13 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (1...𝑁)(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖)))
145 iunin2 5079 . . . . . . . . . . . . 13 𝑖 ∈ (1...𝑁)(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
146144, 145eqtri 2754 . . . . . . . . . . . 12 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
147142, 146eqtr4di 2784 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) = 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
148 fzfid 13993 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (1...𝑁) ∈ Fin)
149 ffvelcdm 7095 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (𝐹𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
15013, 73, 149syl2an 594 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...𝑁)) → (𝐹𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
151150elin2d 4200 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (1...𝑁)) → (𝐹𝑖) ∈ (ℝ × ℝ))
152 1st2nd2 8042 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑖) ∈ (ℝ × ℝ) → (𝐹𝑖) = ⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩)
153151, 152syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...𝑁)) → (𝐹𝑖) = ⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩)
154153fveq2d 6905 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) = ((,)‘⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩))
155 df-ov 7427 . . . . . . . . . . . . . . . . 17 ((1st ‘(𝐹𝑖))(,)(2nd ‘(𝐹𝑖))) = ((,)‘⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩)
156154, 155eqtr4di 2784 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) = ((1st ‘(𝐹𝑖))(,)(2nd ‘(𝐹𝑖))))
157 ioombl 25585 . . . . . . . . . . . . . . . 16 ((1st ‘(𝐹𝑖))(,)(2nd ‘(𝐹𝑖))) ∈ dom vol
158156, 157eqeltrdi 2834 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) ∈ dom vol)
159158adantlr 713 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) ∈ dom vol)
160 ffvelcdm 7095 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
1616, 90, 160syl2an 594 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
162161elin2d 4200 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) ∈ (ℝ × ℝ))
163 1st2nd2 8042 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑗) ∈ (ℝ × ℝ) → (𝐺𝑗) = ⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
164162, 163syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) = ⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
165164fveq2d 6905 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) = ((,)‘⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩))
166 df-ov 7427 . . . . . . . . . . . . . . . . 17 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) = ((,)‘⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
167165, 166eqtr4di 2784 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) = ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))))
168 ioombl 25585 . . . . . . . . . . . . . . . 16 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) ∈ dom vol
169167, 168eqeltrdi 2834 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) ∈ dom vol)
170169adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺𝑗)) ∈ dom vol)
171 inmbl 25562 . . . . . . . . . . . . . 14 ((((,)‘(𝐹𝑖)) ∈ dom vol ∧ ((,)‘(𝐺𝑗)) ∈ dom vol) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
172159, 170, 171syl2anc 582 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
173172ralrimiva 3136 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
174 finiunmbl 25564 . . . . . . . . . . . 12 (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol) → 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
175148, 173, 174syl2anc 582 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
176147, 175eqeltrd 2826 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) ∈ dom vol)
177 inss2 4231 . . . . . . . . . . 11 (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ 𝐴
17813uniiccdif 25598 . . . . . . . . . . . . . . 15 (𝜑 → ( ran ((,) ∘ 𝐹) ⊆ ran ([,] ∘ 𝐹) ∧ (vol*‘( ran ([,] ∘ 𝐹) ∖ ran ((,) ∘ 𝐹))) = 0))
179178simpld 493 . . . . . . . . . . . . . 14 (𝜑 ran ((,) ∘ 𝐹) ⊆ ran ([,] ∘ 𝐹))
180 ovolficcss 25489 . . . . . . . . . . . . . . 15 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐹) ⊆ ℝ)
18113, 180syl 17 . . . . . . . . . . . . . 14 (𝜑 ran ([,] ∘ 𝐹) ⊆ ℝ)
182179, 181sstrd 3990 . . . . . . . . . . . . 13 (𝜑 ran ((,) ∘ 𝐹) ⊆ ℝ)
18316, 182eqsstrid 4028 . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ)
184183adantr 479 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → 𝐴 ⊆ ℝ)
185177, 184sstrid 3991 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ℝ)
186 inss1 4230 . . . . . . . . . . 11 (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺𝑗))
187 ioossre 13439 . . . . . . . . . . . 12 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) ⊆ ℝ
188167, 187eqsstrdi 4034 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) ⊆ ℝ)
189167fveq2d 6905 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺𝑗))) = (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))))
190 ovolfcl 25486 . . . . . . . . . . . . . . 15 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
1916, 90, 190syl2an 594 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
192 ovolioo 25588 . . . . . . . . . . . . . 14 (((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))) → (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
193191, 192syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
194189, 193eqtrd 2766 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺𝑗))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
195191simp2d 1140 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺𝑗)) ∈ ℝ)
196191simp1d 1139 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺𝑗)) ∈ ℝ)
197195, 196resubcld 11692 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) ∈ ℝ)
198194, 197eqeltrd 2826 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ)
199 ovolsscl 25506 . . . . . . . . . . 11 (((((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺𝑗)) ∧ ((,)‘(𝐺𝑗)) ⊆ ℝ ∧ (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ∈ ℝ)
200186, 188, 198, 199mp3an2i 1463 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ∈ ℝ)
201 mblsplit 25552 . . . . . . . . . 10 (((((,)‘(𝐺𝑗)) ∩ 𝐿) ∈ dom vol ∧ (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ∈ ℝ) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) = ((vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)))))
202176, 185, 200, 201syl3anc 1368 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) = ((vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)))))
203 imassrn 6080 . . . . . . . . . . . . . . 15 (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ran ((,) ∘ 𝐹)
204203unissi 4922 . . . . . . . . . . . . . 14 (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ran ((,) ∘ 𝐹)
205204, 69, 163sstr4i 4023 . . . . . . . . . . . . 13 𝐿𝐴
206 sslin 4236 . . . . . . . . . . . . 13 (𝐿𝐴 → (((,)‘(𝐺𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺𝑗)) ∩ 𝐴))
207205, 206mp1i 13 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺𝑗)) ∩ 𝐴))
208 sseqin2 4216 . . . . . . . . . . . 12 ((((,)‘(𝐺𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺𝑗)) ∩ 𝐴) ↔ ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿)) = (((,)‘(𝐺𝑗)) ∩ 𝐿))
209207, 208sylib 217 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿)) = (((,)‘(𝐺𝑗)) ∩ 𝐿))
210209fveq2d 6905 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) = (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)))
211 indifdir 4286 . . . . . . . . . . . . 13 ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = ((𝐴 ∩ ((,)‘(𝐺𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺𝑗))))
212 incom 4202 . . . . . . . . . . . . . 14 (𝐴 ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝐴)
213 incom 4202 . . . . . . . . . . . . . 14 (𝐿 ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝐿)
214212, 213difeq12i 4119 . . . . . . . . . . . . 13 ((𝐴 ∩ ((,)‘(𝐺𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺𝑗)))) = ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿))
215211, 214eqtri 2754 . . . . . . . . . . . 12 ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿))
21679eqcomd 2732 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝐴)
21777ineq1d 4212 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
218 2fveq3 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑖 → ((,)‘(𝐹𝑥)) = ((,)‘(𝐹𝑖)))
219218cbvdisjv 5129 . . . . . . . . . . . . . . . . . . . 20 (Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)) ↔ Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
22014, 219sylib 217 . . . . . . . . . . . . . . . . . . 19 (𝜑Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
221 fz1ssnn 13586 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ⊆ ℕ
222221a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...𝑁) ⊆ ℕ)
223 uzss 12897 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 + 1) ∈ (ℤ‘1) → (ℤ‘(𝑁 + 1)) ⊆ (ℤ‘1))
22439, 223syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ℤ‘(𝑁 + 1)) ⊆ (ℤ‘1))
225224, 36sseqtrrdi 4031 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℤ‘(𝑁 + 1)) ⊆ ℕ)
22647ineq1d 4212 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...((𝑁 + 1) − 1)) ∩ (ℤ‘(𝑁 + 1))) = ((1...𝑁) ∩ (ℤ‘(𝑁 + 1))))
227 uzdisj 13628 . . . . . . . . . . . . . . . . . . . 20 ((1...((𝑁 + 1) − 1)) ∩ (ℤ‘(𝑁 + 1))) = ∅
228226, 227eqtr3di 2781 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅)
229 disjiun 5140 . . . . . . . . . . . . . . . . . . 19 ((Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) ∧ ((1...𝑁) ⊆ ℕ ∧ (ℤ‘(𝑁 + 1)) ⊆ ℕ ∧ ((1...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅)) → ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅)
230220, 222, 225, 228, 229syl13anc 1369 . . . . . . . . . . . . . . . . . 18 (𝜑 → ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅)
231217, 230eqtrd 2766 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅)
232 uneqdifeq 4497 . . . . . . . . . . . . . . . . 17 ((𝐿𝐴 ∧ (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅) → ((𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝐴 ↔ (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
233205, 231, 232sylancr 585 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝐴 ↔ (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
234216, 233mpbid 231 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
235234adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
236235ineq2d 4213 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ (𝐴𝐿)) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
237 incom 4202 . . . . . . . . . . . . 13 ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ (𝐴𝐿))
238101, 98eqtri 2754 . . . . . . . . . . . . 13 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
239236, 237, 2383eqtr4g 2791 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
240215, 239eqtr3id 2780 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
241240fveq2d 6905 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿))) = (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
242210, 241oveq12d 7442 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)))) = ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
243202, 242eqtrd 2766 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) = ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
244200, 140resubcld 11692 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ∈ ℝ)
245 inss2 4231 . . . . . . . . . . . . 13 (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐺𝑗))
246188adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺𝑗)) ⊆ ℝ)
247198adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ)
248 ovolsscl 25506 . . . . . . . . . . . . 13 (((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐺𝑗)) ∧ ((,)‘(𝐺𝑗)) ⊆ ℝ ∧ (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ) → (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
249245, 246, 247, 248mp3an2i 1463 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
250148, 249fsumrecl 15738 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
251 uniioombl.n2 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
252251r19.21bi 3239 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
253250, 200, 140absdifltd 15438 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → ((abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀) ↔ (((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) < ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀)))))
254252, 253mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) < ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀))))
255254simpld 493 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
256244, 250, 255ltled 11412 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
257147fveq2d 6905 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) = (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
258 mblvol 25550 . . . . . . . . . . . . . . . . 17 ((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol → (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
259172, 258syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
260259, 249eqeltrd 2826 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
261172, 260jca 510 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
262261ralrimiva 3136 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
263 inss1 4230 . . . . . . . . . . . . . . . 16 (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐹𝑖))
264263rgenw 3055 . . . . . . . . . . . . . . 15 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐹𝑖))
265220adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
266 disjss2 5121 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐹𝑖)) → (Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
267264, 265, 266mpsyl 68 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
268 disjss1 5124 . . . . . . . . . . . . . 14 ((1...𝑁) ⊆ ℕ → (Disj 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
269221, 267, 268mpsyl 68 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
270 volfiniun 25567 . . . . . . . . . . . . 13 (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ) ∧ Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
271148, 262, 269, 270syl3anc 1368 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
272 mblvol 25550 . . . . . . . . . . . . 13 ( 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
273175, 272syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
274259sumeq2dv 15707 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
275271, 273, 2743eqtr3d 2774 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
276257, 275eqtrd 2766 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
277256, 276breqtrrd 5181 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)))
278276, 250eqeltrd 2826 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) ∈ ℝ)
279200, 140, 278lesubaddd 11861 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → (((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) ↔ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
280277, 279mpbid 231 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
281243, 280eqbrtrrd 5177 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
282131, 140, 278leadd2d 11859 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ (𝐶 / 𝑀) ↔ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
283281, 282mpbird 256 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ (𝐶 / 𝑀))
284124, 131, 140, 283fsumle 15803 . . . . 5 (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀))
285139recnd 11292 . . . . . . 7 (𝜑 → (𝐶 / 𝑀) ∈ ℂ)
286 fsumconst 15794 . . . . . . 7 (((1...𝑀) ∈ Fin ∧ (𝐶 / 𝑀) ∈ ℂ) → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
287124, 285, 286syl2anc 582 . . . . . 6 (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
288 nnnn0 12531 . . . . . . . 8 (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
289 hashfz1 14363 . . . . . . . 8 (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
290138, 288, 2893syl 18 . . . . . . 7 (𝜑 → (♯‘(1...𝑀)) = 𝑀)
291290oveq1d 7439 . . . . . 6 (𝜑 → ((♯‘(1...𝑀)) · (𝐶 / 𝑀)) = (𝑀 · (𝐶 / 𝑀)))
292116recnd 11292 . . . . . . 7 (𝜑𝐶 ∈ ℂ)
293138nncnd 12280 . . . . . . 7 (𝜑𝑀 ∈ ℂ)
294138nnne0d 12314 . . . . . . 7 (𝜑𝑀 ≠ 0)
295292, 293, 294divcan2d 12043 . . . . . 6 (𝜑 → (𝑀 · (𝐶 / 𝑀)) = 𝐶)
296287, 291, 2953eqtrd 2770 . . . . 5 (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = 𝐶)
297284, 296breqtrd 5179 . . . 4 (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ 𝐶)
298114, 132, 116, 137, 297letrd 11421 . . 3 (𝜑 → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ 𝐶)
299114, 116, 34, 298leadd2dd 11879 . 2 (𝜑 → ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(𝐾𝐿)) + 𝐶))
30031, 115, 117, 123, 299letrd 11421 1 (𝜑 → (vol*‘(𝐾𝐴)) ≤ ((vol*‘(𝐾𝐿)) + 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wral 3051  cdif 3944  cun 3945  cin 3946  wss 3947  c0 4325  𝒫 cpw 4607  cop 4639   cuni 4913   ciun 5001  Disj wdisj 5118   class class class wbr 5153   × cxp 5680  dom cdm 5682  ran crn 5683  cima 5685  ccom 5686  Fun wfun 6548   Fn wfn 6549  wf 6550  cfv 6554  (class class class)co 7424  1st c1st 8001  2nd c2nd 8002  Fincfn 8974  supcsup 9483  cc 11156  cr 11157  0cc0 11158  1c1 11159   + caddc 11161   · cmul 11163  *cxr 11297   < clt 11298  cle 11299  cmin 11494   / cdiv 11921  cn 12264  0cn0 12524  cuz 12874  +crp 13028  (,)cioo 13378  [,]cicc 13381  ...cfz 13538  seqcseq 14021  chash 14347  abscabs 15239  Σcsu 15690  vol*covol 25482  volcvol 25483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9684  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235  ax-pre-sup 11236
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-disj 5119  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-isom 6563  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7690  df-om 7877  df-1st 8003  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-2o 8497  df-er 8734  df-map 8857  df-pm 8858  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-fi 9454  df-sup 9485  df-inf 9486  df-oi 9553  df-dju 9944  df-card 9982  df-acn 9985  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-div 11922  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12611  df-uz 12875  df-q 12985  df-rp 13029  df-xneg 13146  df-xadd 13147  df-xmul 13148  df-ioo 13382  df-ico 13384  df-icc 13385  df-fz 13539  df-fzo 13682  df-fl 13812  df-seq 14022  df-exp 14082  df-hash 14348  df-cj 15104  df-re 15105  df-im 15106  df-sqrt 15240  df-abs 15241  df-clim 15490  df-rlim 15491  df-sum 15691  df-rest 17437  df-topgen 17458  df-psmet 21335  df-xmet 21336  df-met 21337  df-bl 21338  df-mopn 21339  df-top 22887  df-topon 22904  df-bases 22940  df-cmp 23382  df-ovol 25484  df-vol 25485
This theorem is referenced by:  uniioombllem5  25607
  Copyright terms: Public domain W3C validator