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

Theorem uniioombllem4 25621
Description: Lemma for uniioombl 25624. (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 4237 . . 3 (𝐾𝐴) ⊆ 𝐾
2 uniioombl.k . . . . 5 𝐾 = (((,) ∘ 𝐺) “ (1...𝑀))
3 imassrn 6089 . . . . . 6 (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ran ((,) ∘ 𝐺)
43unissi 4916 . . . . 5 (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ran ((,) ∘ 𝐺)
52, 4eqsstri 4030 . . . 4 𝐾 ran ((,) ∘ 𝐺)
6 uniioombl.g . . . . . . 7 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
76uniiccdif 25613 . . . . . 6 (𝜑 → ( ran ((,) ∘ 𝐺) ⊆ ran ([,] ∘ 𝐺) ∧ (vol*‘( ran ([,] ∘ 𝐺) ∖ ran ((,) ∘ 𝐺))) = 0))
87simpld 494 . . . . 5 (𝜑 ran ((,) ∘ 𝐺) ⊆ ran ([,] ∘ 𝐺))
9 ovolficcss 25504 . . . . . 6 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐺) ⊆ ℝ)
106, 9syl 17 . . . . 5 (𝜑 ran ([,] ∘ 𝐺) ⊆ ℝ)
118, 10sstrd 3994 . . . 4 (𝜑 ran ((,) ∘ 𝐺) ⊆ ℝ)
125, 11sstrid 3995 . . 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 25616 . . . . 5 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
23 ssid 4006 . . . . . 6 ran ((,) ∘ 𝐺) ⊆ ran ((,) ∘ 𝐺)
2420ovollb 25514 . . . . . 6 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ran ((,) ∘ 𝐺) ⊆ ran ((,) ∘ 𝐺)) → (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
256, 23, 24sylancl 586 . . . . 5 (𝜑 → (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
26 ovollecl 25518 . . . . 5 (( ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ ∧ (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < )) → (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ)
2711, 22, 25, 26syl3anc 1373 . . . 4 (𝜑 → (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ)
28 ovolsscl 25521 . . . 4 ((𝐾 ran ((,) ∘ 𝐺) ∧ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘𝐾) ∈ ℝ)
295, 11, 27, 28mp3an2i 1468 . . 3 (𝜑 → (vol*‘𝐾) ∈ ℝ)
30 ovolsscl 25521 . . 3 (((𝐾𝐴) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘(𝐾𝐴)) ∈ ℝ)
311, 12, 29, 30mp3an2i 1468 . 2 (𝜑 → (vol*‘(𝐾𝐴)) ∈ ℝ)
32 inss1 4237 . . . 4 (𝐾𝐿) ⊆ 𝐾
33 ovolsscl 25521 . . . 4 (((𝐾𝐿) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘(𝐾𝐿)) ∈ ℝ)
3432, 12, 29, 33mp3an2i 1468 . . 3 (𝜑 → (vol*‘(𝐾𝐿)) ∈ ℝ)
35 ssun2 4179 . . . . . 6 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
36 nnuz 12921 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
37 uniioombl.n . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℕ)
3837peano2nnd 12283 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ ℕ)
3938, 36eleqtrdi 2851 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
40 uzsplit 13636 . . . . . . . . . . . . . . 15 ((𝑁 + 1) ∈ (ℤ‘1) → (ℤ‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
4139, 40syl 17 . . . . . . . . . . . . . 14 (𝜑 → (ℤ‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
4236, 41eqtrid 2789 . . . . . . . . . . . . 13 (𝜑 → ℕ = ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
4337nncnd 12282 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℂ)
44 ax-1cn 11213 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
45 pncan 11514 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
4643, 44, 45sylancl 586 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
4746oveq2d 7447 . . . . . . . . . . . . . 14 (𝜑 → (1...((𝑁 + 1) − 1)) = (1...𝑁))
4847uneq1d 4167 . . . . . . . . . . . . 13 (𝜑 → ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))) = ((1...𝑁) ∪ (ℤ‘(𝑁 + 1))))
4942, 48eqtrd 2777 . . . . . . . . . . . 12 (𝜑 → ℕ = ((1...𝑁) ∪ (ℤ‘(𝑁 + 1))))
5049iuneq1d 5019 . . . . . . . . . . 11 (𝜑 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) = 𝑖 ∈ ((1...𝑁) ∪ (ℤ‘(𝑁 + 1)))((,)‘(𝐹𝑖)))
51 iunxun 5094 . . . . . . . . . . 11 𝑖 ∈ ((1...𝑁) ∪ (ℤ‘(𝑁 + 1)))((,)‘(𝐹𝑖)) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∪ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
5250, 51eqtrdi 2793 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∪ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
53 ioof 13487 . . . . . . . . . . . . . 14 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
54 inss2 4238 . . . . . . . . . . . . . . . 16 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
55 rexpssxrxp 11306 . . . . . . . . . . . . . . . 16 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
5654, 55sstri 3993 . . . . . . . . . . . . . . 15 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
57 fss 6752 . . . . . . . . . . . . . . 15 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* × ℝ*))
5813, 56, 57sylancl 586 . . . . . . . . . . . . . 14 (𝜑𝐹:ℕ⟶(ℝ* × ℝ*))
59 fco 6760 . . . . . . . . . . . . . 14 (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
6053, 58, 59sylancr 587 . . . . . . . . . . . . 13 (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
61 ffn 6736 . . . . . . . . . . . . 13 (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → ((,) ∘ 𝐹) Fn ℕ)
62 fniunfv 7267 . . . . . . . . . . . . 13 (((,) ∘ 𝐹) Fn ℕ → 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ran ((,) ∘ 𝐹))
6360, 61, 623syl 18 . . . . . . . . . . . 12 (𝜑 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ran ((,) ∘ 𝐹))
64 fvco3 7008 . . . . . . . . . . . . . 14 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹𝑖)))
6513, 64sylan 580 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹𝑖)))
6665iuneq2dv 5016 . . . . . . . . . . . 12 (𝜑 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
6763, 66eqtr3d 2779 . . . . . . . . . . 11 (𝜑 ran ((,) ∘ 𝐹) = 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
6816, 67eqtrid 2789 . . . . . . . . . 10 (𝜑𝐴 = 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
69 uniioombl.l . . . . . . . . . . . 12 𝐿 = (((,) ∘ 𝐹) “ (1...𝑁))
70 ffun 6739 . . . . . . . . . . . . . 14 (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐹))
71 funiunfv 7268 . . . . . . . . . . . . . 14 (Fun ((,) ∘ 𝐹) → 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = (((,) ∘ 𝐹) “ (1...𝑁)))
7260, 70, 713syl 18 . . . . . . . . . . . . 13 (𝜑 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = (((,) ∘ 𝐹) “ (1...𝑁)))
73 elfznn 13593 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑁) → 𝑖 ∈ ℕ)
7413, 73, 64syl2an 596 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹𝑖)))
7574iuneq2dv 5016 . . . . . . . . . . . . 13 (𝜑 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
7672, 75eqtr3d 2779 . . . . . . . . . . . 12 (𝜑 (((,) ∘ 𝐹) “ (1...𝑁)) = 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
7769, 76eqtrid 2789 . . . . . . . . . . 11 (𝜑𝐿 = 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
7877uneq1d 4167 . . . . . . . . . 10 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∪ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
7952, 68, 783eqtr4d 2787 . . . . . . . . 9 (𝜑𝐴 = (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
8079ineq2d 4220 . . . . . . . 8 (𝜑 → (𝐾𝐴) = (𝐾 ∩ (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))))
81 indi 4284 . . . . . . . 8 (𝐾 ∩ (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))) = ((𝐾𝐿) ∪ (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
8280, 81eqtrdi 2793 . . . . . . 7 (𝜑 → (𝐾𝐴) = ((𝐾𝐿) ∪ (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))))
83 fss 6752 . . . . . . . . . . . . . . 15 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* × ℝ*))
846, 56, 83sylancl 586 . . . . . . . . . . . . . 14 (𝜑𝐺:ℕ⟶(ℝ* × ℝ*))
85 fco 6760 . . . . . . . . . . . . . 14 (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
8653, 84, 85sylancr 587 . . . . . . . . . . . . 13 (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
87 ffun 6739 . . . . . . . . . . . . 13 (((,) ∘ 𝐺):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐺))
88 funiunfv 7268 . . . . . . . . . . . . 13 (Fun ((,) ∘ 𝐺) → 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = (((,) ∘ 𝐺) “ (1...𝑀)))
8986, 87, 883syl 18 . . . . . . . . . . . 12 (𝜑 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = (((,) ∘ 𝐺) “ (1...𝑀)))
90 elfznn 13593 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
91 fvco3 7008 . . . . . . . . . . . . . 14 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺𝑗)))
926, 90, 91syl2an 596 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺𝑗)))
9392iuneq2dv 5016 . . . . . . . . . . . 12 (𝜑 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
9489, 93eqtr3d 2779 . . . . . . . . . . 11 (𝜑 (((,) ∘ 𝐺) “ (1...𝑀)) = 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
952, 94eqtrid 2789 . . . . . . . . . 10 (𝜑𝐾 = 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
9695ineq2d 4220 . . . . . . . . 9 (𝜑 → ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝐾) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗))))
97 incom 4209 . . . . . . . . 9 (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝐾)
98 iunin2 5071 . . . . . . . . . . . . 13 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
99 incom 4209 . . . . . . . . . . . . . . 15 (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖)))
10099a1i 11 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ‘(𝑁 + 1)) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))))
101100iuneq2i 5013 . . . . . . . . . . . . 13 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖)))
102 incom 4209 . . . . . . . . . . . . 13 ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
10398, 101, 1023eqtr4ri 2776 . . . . . . . . . . . 12 ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))
104103a1i 11 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑀) → ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
105104iuneq2i 5013 . . . . . . . . . 10 𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))
106 iunin2 5071 . . . . . . . . . 10 𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
107105, 106eqtr3i 2767 . . . . . . . . 9 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
10896, 97, 1073eqtr4g 2802 . . . . . . . 8 (𝜑 → (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
109108uneq2d 4168 . . . . . . 7 (𝜑 → ((𝐾𝐿) ∪ (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))) = ((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
11082, 109eqtrd 2777 . . . . . 6 (𝜑 → (𝐾𝐴) = ((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
11135, 110sseqtrrid 4027 . . . . 5 (𝜑 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ (𝐾𝐴))
112111, 1sstrdi 3996 . . . 4 (𝜑 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
113 ovolsscl 25521 . . . 4 (( 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
114112, 12, 29, 113syl3anc 1373 . . 3 (𝜑 → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
11534, 114readdcld 11290 . 2 (𝜑 → ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ∈ ℝ)
11618rpred 13077 . . 3 (𝜑𝐶 ∈ ℝ)
11734, 116readdcld 11290 . 2 (𝜑 → ((vol*‘(𝐾𝐿)) + 𝐶) ∈ ℝ)
118110fveq2d 6910 . . 3 (𝜑 → (vol*‘(𝐾𝐴)) = (vol*‘((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
11932, 12sstrid 3995 . . . 4 (𝜑 → (𝐾𝐿) ⊆ ℝ)
120112, 12sstrd 3994 . . . 4 (𝜑 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ)
121 ovolun 25534 . . . 4 ((((𝐾𝐿) ⊆ ℝ ∧ (vol*‘(𝐾𝐿)) ∈ ℝ) ∧ ( 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)) → (vol*‘((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
122119, 34, 120, 114, 121syl22anc 839 . . 3 (𝜑 → (vol*‘((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
123118, 122eqbrtrd 5165 . 2 (𝜑 → (vol*‘(𝐾𝐴)) ≤ ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
124 fzfid 14014 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
125 iunss 5045 . . . . . . . 8 ( 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾 ↔ ∀𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
126112, 125sylib 218 . . . . . . 7 (𝜑 → ∀𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
127126r19.21bi 3251 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
12812adantr 480 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → 𝐾 ⊆ ℝ)
12929adantr 480 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘𝐾) ∈ ℝ)
130 ovolsscl 25521 . . . . . 6 (( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
131127, 128, 129, 130syl3anc 1373 . . . . 5 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
132124, 131fsumrecl 15770 . . . 4 (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
133127, 128sstrd 3994 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ)
134133, 131jca 511 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → ( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
135134ralrimiva 3146 . . . . 5 (𝜑 → ∀𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
136 ovolfiniun 25536 . . . . 5 (((1...𝑀) ∈ Fin ∧ ∀𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)) → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
137124, 135, 136syl2anc 584 . . . 4 (𝜑 → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
138 uniioombl.m . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
139116, 138nndivred 12320 . . . . . . 7 (𝜑 → (𝐶 / 𝑀) ∈ ℝ)
140139adantr 480 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐶 / 𝑀) ∈ ℝ)
14177ineq2d 4220 . . . . . . . . . . . . 13 (𝜑 → (((,)‘(𝐺𝑗)) ∩ 𝐿) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖))))
142141adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖))))
14399a1i 11 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑁) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))))
144143iuneq2i 5013 . . . . . . . . . . . . 13 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (1...𝑁)(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖)))
145 iunin2 5071 . . . . . . . . . . . . 13 𝑖 ∈ (1...𝑁)(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
146144, 145eqtri 2765 . . . . . . . . . . . 12 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
147142, 146eqtr4di 2795 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) = 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
148 fzfid 14014 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (1...𝑁) ∈ Fin)
149 ffvelcdm 7101 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (𝐹𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
15013, 73, 149syl2an 596 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...𝑁)) → (𝐹𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
151150elin2d 4205 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (1...𝑁)) → (𝐹𝑖) ∈ (ℝ × ℝ))
152 1st2nd2 8053 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑖) ∈ (ℝ × ℝ) → (𝐹𝑖) = ⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩)
153151, 152syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...𝑁)) → (𝐹𝑖) = ⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩)
154153fveq2d 6910 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) = ((,)‘⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩))
155 df-ov 7434 . . . . . . . . . . . . . . . . 17 ((1st ‘(𝐹𝑖))(,)(2nd ‘(𝐹𝑖))) = ((,)‘⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩)
156154, 155eqtr4di 2795 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) = ((1st ‘(𝐹𝑖))(,)(2nd ‘(𝐹𝑖))))
157 ioombl 25600 . . . . . . . . . . . . . . . 16 ((1st ‘(𝐹𝑖))(,)(2nd ‘(𝐹𝑖))) ∈ dom vol
158156, 157eqeltrdi 2849 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) ∈ dom vol)
159158adantlr 715 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) ∈ dom vol)
160 ffvelcdm 7101 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
1616, 90, 160syl2an 596 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
162161elin2d 4205 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) ∈ (ℝ × ℝ))
163 1st2nd2 8053 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑗) ∈ (ℝ × ℝ) → (𝐺𝑗) = ⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
164162, 163syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) = ⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
165164fveq2d 6910 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) = ((,)‘⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩))
166 df-ov 7434 . . . . . . . . . . . . . . . . 17 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) = ((,)‘⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
167165, 166eqtr4di 2795 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) = ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))))
168 ioombl 25600 . . . . . . . . . . . . . . . 16 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) ∈ dom vol
169167, 168eqeltrdi 2849 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) ∈ dom vol)
170169adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺𝑗)) ∈ dom vol)
171 inmbl 25577 . . . . . . . . . . . . . 14 ((((,)‘(𝐹𝑖)) ∈ dom vol ∧ ((,)‘(𝐺𝑗)) ∈ dom vol) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
172159, 170, 171syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
173172ralrimiva 3146 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
174 finiunmbl 25579 . . . . . . . . . . . 12 (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol) → 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
175148, 173, 174syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
176147, 175eqeltrd 2841 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) ∈ dom vol)
177 inss2 4238 . . . . . . . . . . 11 (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ 𝐴
17813uniiccdif 25613 . . . . . . . . . . . . . . 15 (𝜑 → ( ran ((,) ∘ 𝐹) ⊆ ran ([,] ∘ 𝐹) ∧ (vol*‘( ran ([,] ∘ 𝐹) ∖ ran ((,) ∘ 𝐹))) = 0))
179178simpld 494 . . . . . . . . . . . . . 14 (𝜑 ran ((,) ∘ 𝐹) ⊆ ran ([,] ∘ 𝐹))
180 ovolficcss 25504 . . . . . . . . . . . . . . 15 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐹) ⊆ ℝ)
18113, 180syl 17 . . . . . . . . . . . . . 14 (𝜑 ran ([,] ∘ 𝐹) ⊆ ℝ)
182179, 181sstrd 3994 . . . . . . . . . . . . 13 (𝜑 ran ((,) ∘ 𝐹) ⊆ ℝ)
18316, 182eqsstrid 4022 . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ)
184183adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → 𝐴 ⊆ ℝ)
185177, 184sstrid 3995 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ℝ)
186 inss1 4237 . . . . . . . . . . 11 (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺𝑗))
187 ioossre 13448 . . . . . . . . . . . 12 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) ⊆ ℝ
188167, 187eqsstrdi 4028 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) ⊆ ℝ)
189167fveq2d 6910 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺𝑗))) = (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))))
190 ovolfcl 25501 . . . . . . . . . . . . . . 15 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
1916, 90, 190syl2an 596 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
192 ovolioo 25603 . . . . . . . . . . . . . 14 (((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))) → (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
193191, 192syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
194189, 193eqtrd 2777 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺𝑗))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
195191simp2d 1144 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺𝑗)) ∈ ℝ)
196191simp1d 1143 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺𝑗)) ∈ ℝ)
197195, 196resubcld 11691 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) ∈ ℝ)
198194, 197eqeltrd 2841 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ)
199 ovolsscl 25521 . . . . . . . . . . 11 (((((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺𝑗)) ∧ ((,)‘(𝐺𝑗)) ⊆ ℝ ∧ (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ∈ ℝ)
200186, 188, 198, 199mp3an2i 1468 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ∈ ℝ)
201 mblsplit 25567 . . . . . . . . . 10 (((((,)‘(𝐺𝑗)) ∩ 𝐿) ∈ dom vol ∧ (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ∈ ℝ) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) = ((vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)))))
202176, 185, 200, 201syl3anc 1373 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) = ((vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)))))
203 imassrn 6089 . . . . . . . . . . . . . . 15 (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ran ((,) ∘ 𝐹)
204203unissi 4916 . . . . . . . . . . . . . 14 (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ran ((,) ∘ 𝐹)
205204, 69, 163sstr4i 4035 . . . . . . . . . . . . 13 𝐿𝐴
206 sslin 4243 . . . . . . . . . . . . 13 (𝐿𝐴 → (((,)‘(𝐺𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺𝑗)) ∩ 𝐴))
207205, 206mp1i 13 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺𝑗)) ∩ 𝐴))
208 sseqin2 4223 . . . . . . . . . . . 12 ((((,)‘(𝐺𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺𝑗)) ∩ 𝐴) ↔ ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿)) = (((,)‘(𝐺𝑗)) ∩ 𝐿))
209207, 208sylib 218 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿)) = (((,)‘(𝐺𝑗)) ∩ 𝐿))
210209fveq2d 6910 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) = (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)))
211 indifdir 4295 . . . . . . . . . . . . 13 ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = ((𝐴 ∩ ((,)‘(𝐺𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺𝑗))))
212 incom 4209 . . . . . . . . . . . . . 14 (𝐴 ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝐴)
213 incom 4209 . . . . . . . . . . . . . 14 (𝐿 ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝐿)
214212, 213difeq12i 4124 . . . . . . . . . . . . 13 ((𝐴 ∩ ((,)‘(𝐺𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺𝑗)))) = ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿))
215211, 214eqtri 2765 . . . . . . . . . . . 12 ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿))
21679eqcomd 2743 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝐴)
21777ineq1d 4219 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
218 2fveq3 6911 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑖 → ((,)‘(𝐹𝑥)) = ((,)‘(𝐹𝑖)))
219218cbvdisjv 5121 . . . . . . . . . . . . . . . . . . . 20 (Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)) ↔ Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
22014, 219sylib 218 . . . . . . . . . . . . . . . . . . 19 (𝜑Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
221 fz1ssnn 13595 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ⊆ ℕ
222221a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...𝑁) ⊆ ℕ)
223 uzss 12901 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 + 1) ∈ (ℤ‘1) → (ℤ‘(𝑁 + 1)) ⊆ (ℤ‘1))
22439, 223syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ℤ‘(𝑁 + 1)) ⊆ (ℤ‘1))
225224, 36sseqtrrdi 4025 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℤ‘(𝑁 + 1)) ⊆ ℕ)
22647ineq1d 4219 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...((𝑁 + 1) − 1)) ∩ (ℤ‘(𝑁 + 1))) = ((1...𝑁) ∩ (ℤ‘(𝑁 + 1))))
227 uzdisj 13637 . . . . . . . . . . . . . . . . . . . 20 ((1...((𝑁 + 1) − 1)) ∩ (ℤ‘(𝑁 + 1))) = ∅
228226, 227eqtr3di 2792 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅)
229 disjiun 5131 . . . . . . . . . . . . . . . . . . 19 ((Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) ∧ ((1...𝑁) ⊆ ℕ ∧ (ℤ‘(𝑁 + 1)) ⊆ ℕ ∧ ((1...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅)) → ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅)
230220, 222, 225, 228, 229syl13anc 1374 . . . . . . . . . . . . . . . . . 18 (𝜑 → ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅)
231217, 230eqtrd 2777 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅)
232 uneqdifeq 4493 . . . . . . . . . . . . . . . . 17 ((𝐿𝐴 ∧ (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅) → ((𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝐴 ↔ (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
233205, 231, 232sylancr 587 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝐴 ↔ (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
234216, 233mpbid 232 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
235234adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
236235ineq2d 4220 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ (𝐴𝐿)) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
237 incom 4209 . . . . . . . . . . . . 13 ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ (𝐴𝐿))
238101, 98eqtri 2765 . . . . . . . . . . . . 13 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
239236, 237, 2383eqtr4g 2802 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
240215, 239eqtr3id 2791 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
241240fveq2d 6910 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿))) = (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
242210, 241oveq12d 7449 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)))) = ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
243202, 242eqtrd 2777 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) = ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
244200, 140resubcld 11691 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ∈ ℝ)
245 inss2 4238 . . . . . . . . . . . . 13 (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐺𝑗))
246188adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺𝑗)) ⊆ ℝ)
247198adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ)
248 ovolsscl 25521 . . . . . . . . . . . . 13 (((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐺𝑗)) ∧ ((,)‘(𝐺𝑗)) ⊆ ℝ ∧ (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ) → (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
249245, 246, 247, 248mp3an2i 1468 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
250148, 249fsumrecl 15770 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
251 uniioombl.n2 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
252251r19.21bi 3251 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
253250, 200, 140absdifltd 15472 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → ((abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀) ↔ (((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) < ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀)))))
254252, 253mpbid 232 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) < ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀))))
255254simpld 494 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
256244, 250, 255ltled 11409 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
257147fveq2d 6910 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) = (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
258 mblvol 25565 . . . . . . . . . . . . . . . . 17 ((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol → (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
259172, 258syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
260259, 249eqeltrd 2841 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
261172, 260jca 511 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
262261ralrimiva 3146 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
263 inss1 4237 . . . . . . . . . . . . . . . 16 (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐹𝑖))
264263rgenw 3065 . . . . . . . . . . . . . . 15 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐹𝑖))
265220adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
266 disjss2 5113 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐹𝑖)) → (Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
267264, 265, 266mpsyl 68 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
268 disjss1 5116 . . . . . . . . . . . . . 14 ((1...𝑁) ⊆ ℕ → (Disj 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
269221, 267, 268mpsyl 68 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
270 volfiniun 25582 . . . . . . . . . . . . 13 (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ) ∧ Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
271148, 262, 269, 270syl3anc 1373 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
272 mblvol 25565 . . . . . . . . . . . . 13 ( 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
273175, 272syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
274259sumeq2dv 15738 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
275271, 273, 2743eqtr3d 2785 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
276257, 275eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
277256, 276breqtrrd 5171 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)))
278276, 250eqeltrd 2841 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) ∈ ℝ)
279200, 140, 278lesubaddd 11860 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → (((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) ↔ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
280277, 279mpbid 232 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
281243, 280eqbrtrrd 5167 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
282131, 140, 278leadd2d 11858 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ (𝐶 / 𝑀) ↔ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
283281, 282mpbird 257 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ (𝐶 / 𝑀))
284124, 131, 140, 283fsumle 15835 . . . . 5 (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀))
285139recnd 11289 . . . . . . 7 (𝜑 → (𝐶 / 𝑀) ∈ ℂ)
286 fsumconst 15826 . . . . . . 7 (((1...𝑀) ∈ Fin ∧ (𝐶 / 𝑀) ∈ ℂ) → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
287124, 285, 286syl2anc 584 . . . . . 6 (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
288 nnnn0 12533 . . . . . . . 8 (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
289 hashfz1 14385 . . . . . . . 8 (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
290138, 288, 2893syl 18 . . . . . . 7 (𝜑 → (♯‘(1...𝑀)) = 𝑀)
291290oveq1d 7446 . . . . . 6 (𝜑 → ((♯‘(1...𝑀)) · (𝐶 / 𝑀)) = (𝑀 · (𝐶 / 𝑀)))
292116recnd 11289 . . . . . . 7 (𝜑𝐶 ∈ ℂ)
293138nncnd 12282 . . . . . . 7 (𝜑𝑀 ∈ ℂ)
294138nnne0d 12316 . . . . . . 7 (𝜑𝑀 ≠ 0)
295292, 293, 294divcan2d 12045 . . . . . 6 (𝜑 → (𝑀 · (𝐶 / 𝑀)) = 𝐶)
296287, 291, 2953eqtrd 2781 . . . . 5 (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = 𝐶)
297284, 296breqtrd 5169 . . . 4 (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ 𝐶)
298114, 132, 116, 137, 297letrd 11418 . . 3 (𝜑 → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ 𝐶)
299114, 116, 34, 298leadd2dd 11878 . 2 (𝜑 → ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(𝐾𝐿)) + 𝐶))
30031, 115, 117, 123, 299letrd 11418 1 (𝜑 → (vol*‘(𝐾𝐴)) ≤ ((vol*‘(𝐾𝐿)) + 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061  cdif 3948  cun 3949  cin 3950  wss 3951  c0 4333  𝒫 cpw 4600  cop 4632   cuni 4907   ciun 4991  Disj wdisj 5110   class class class wbr 5143   × cxp 5683  dom cdm 5685  ran crn 5686  cima 5688  ccom 5689  Fun wfun 6555   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  1st c1st 8012  2nd c2nd 8013  Fincfn 8985  supcsup 9480  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  *cxr 11294   < clt 11295  cle 11296  cmin 11492   / cdiv 11920  cn 12266  0cn0 12526  cuz 12878  +crp 13034  (,)cioo 13387  [,]cicc 13390  ...cfz 13547  seqcseq 14042  chash 14369  abscabs 15273  Σcsu 15722  vol*covol 25497  volcvol 25498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-acn 9982  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-rlim 15525  df-sum 15723  df-rest 17467  df-topgen 17488  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-top 22900  df-topon 22917  df-bases 22953  df-cmp 23395  df-ovol 25499  df-vol 25500
This theorem is referenced by:  uniioombllem5  25622
  Copyright terms: Public domain W3C validator