Metamath Proof Explorer


Theorem uniioombllem3a

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 8-May-2015)

Ref Expression
Hypotheses uniioombl.1 ( 𝜑𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.2 ( 𝜑Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹𝑥 ) ) )
uniioombl.3 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
uniioombl.a 𝐴 = ran ( (,) ∘ 𝐹 )
uniioombl.e ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
uniioombl.c ( 𝜑𝐶 ∈ ℝ+ )
uniioombl.g ( 𝜑𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.s ( 𝜑𝐸 ran ( (,) ∘ 𝐺 ) )
uniioombl.t 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
uniioombl.v ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
uniioombl.m ( 𝜑𝑀 ∈ ℕ )
uniioombl.m2 ( 𝜑 → ( abs ‘ ( ( 𝑇𝑀 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
uniioombl.k 𝐾 = ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) )
Assertion uniioombllem3a ( 𝜑 → ( 𝐾 = 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) )

Proof

Step Hyp Ref Expression
1 uniioombl.1 ( 𝜑𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2 uniioombl.2 ( 𝜑Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹𝑥 ) ) )
3 uniioombl.3 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4 uniioombl.a 𝐴 = ran ( (,) ∘ 𝐹 )
5 uniioombl.e ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
6 uniioombl.c ( 𝜑𝐶 ∈ ℝ+ )
7 uniioombl.g ( 𝜑𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8 uniioombl.s ( 𝜑𝐸 ran ( (,) ∘ 𝐺 ) )
9 uniioombl.t 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
10 uniioombl.v ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
11 uniioombl.m ( 𝜑𝑀 ∈ ℕ )
12 uniioombl.m2 ( 𝜑 → ( abs ‘ ( ( 𝑇𝑀 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
13 uniioombl.k 𝐾 = ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) )
14 ioof (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
15 inss2 ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
16 rexpssxrxp ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
17 15 16 sstri ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
18 fss ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) )
19 7 17 18 sylancl ( 𝜑𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) )
20 fco ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ )
21 14 19 20 sylancr ( 𝜑 → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ )
22 ffun ( ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ → Fun ( (,) ∘ 𝐺 ) )
23 funiunfv ( Fun ( (,) ∘ 𝐺 ) → 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) )
24 21 22 23 3syl ( 𝜑 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) )
25 elfznn ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℕ )
26 fvco3 ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ( (,) ‘ ( 𝐺𝑗 ) ) )
27 7 25 26 syl2an ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ( (,) ‘ ( 𝐺𝑗 ) ) )
28 27 iuneq2dv ( 𝜑 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) )
29 24 28 eqtr3d ( 𝜑 ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) = 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) )
30 13 29 syl5eq ( 𝜑𝐾 = 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) )
31 ffvelrn ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝐺𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
32 7 25 31 syl2an ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
33 32 elin2d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺𝑗 ) ∈ ( ℝ × ℝ ) )
34 1st2nd2 ( ( 𝐺𝑗 ) ∈ ( ℝ × ℝ ) → ( 𝐺𝑗 ) = ⟨ ( 1st ‘ ( 𝐺𝑗 ) ) , ( 2nd ‘ ( 𝐺𝑗 ) ) ⟩ )
35 33 34 syl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺𝑗 ) = ⟨ ( 1st ‘ ( 𝐺𝑗 ) ) , ( 2nd ‘ ( 𝐺𝑗 ) ) ⟩ )
36 35 fveq2d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺𝑗 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺𝑗 ) ) , ( 2nd ‘ ( 𝐺𝑗 ) ) ⟩ ) )
37 df-ov ( ( 1st ‘ ( 𝐺𝑗 ) ) (,) ( 2nd ‘ ( 𝐺𝑗 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐺𝑗 ) ) , ( 2nd ‘ ( 𝐺𝑗 ) ) ⟩ )
38 36 37 eqtr4di ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺𝑗 ) ) = ( ( 1st ‘ ( 𝐺𝑗 ) ) (,) ( 2nd ‘ ( 𝐺𝑗 ) ) ) )
39 ioossre ( ( 1st ‘ ( 𝐺𝑗 ) ) (,) ( 2nd ‘ ( 𝐺𝑗 ) ) ) ⊆ ℝ
40 38 39 eqsstrdi ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺𝑗 ) ) ⊆ ℝ )
41 40 ralrimiva ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) ⊆ ℝ )
42 iunss ( 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) ⊆ ℝ ↔ ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) ⊆ ℝ )
43 41 42 sylibr ( 𝜑 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) ⊆ ℝ )
44 30 43 eqsstrd ( 𝜑𝐾 ⊆ ℝ )
45 fzfid ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
46 38 fveq2d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) = ( vol* ‘ ( ( 1st ‘ ( 𝐺𝑗 ) ) (,) ( 2nd ‘ ( 𝐺𝑗 ) ) ) ) )
47 ovolfcl ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺𝑗 ) ) ) )
48 7 25 47 syl2an ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 1st ‘ ( 𝐺𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺𝑗 ) ) ) )
49 ovolioo ( ( ( 1st ‘ ( 𝐺𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺𝑗 ) ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺𝑗 ) ) (,) ( 2nd ‘ ( 𝐺𝑗 ) ) ) ) = ( ( 2nd ‘ ( 𝐺𝑗 ) ) − ( 1st ‘ ( 𝐺𝑗 ) ) ) )
50 48 49 syl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺𝑗 ) ) (,) ( 2nd ‘ ( 𝐺𝑗 ) ) ) ) = ( ( 2nd ‘ ( 𝐺𝑗 ) ) − ( 1st ‘ ( 𝐺𝑗 ) ) ) )
51 46 50 eqtrd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) = ( ( 2nd ‘ ( 𝐺𝑗 ) ) − ( 1st ‘ ( 𝐺𝑗 ) ) ) )
52 48 simp2d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 2nd ‘ ( 𝐺𝑗 ) ) ∈ ℝ )
53 48 simp1d ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 1st ‘ ( 𝐺𝑗 ) ) ∈ ℝ )
54 52 53 resubcld ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 2nd ‘ ( 𝐺𝑗 ) ) − ( 1st ‘ ( 𝐺𝑗 ) ) ) ∈ ℝ )
55 51 54 eqeltrd ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) ∈ ℝ )
56 45 55 fsumrecl ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) ∈ ℝ )
57 30 fveq2d ( 𝜑 → ( vol* ‘ 𝐾 ) = ( vol* ‘ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) ) )
58 40 55 jca ( ( 𝜑𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ‘ ( 𝐺𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) ∈ ℝ ) )
59 58 ralrimiva ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ‘ ( 𝐺𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) ∈ ℝ ) )
60 ovolfiniun ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ‘ ( 𝐺𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) ∈ ℝ ) ) → ( vol* ‘ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) )
61 45 59 60 syl2anc ( 𝜑 → ( vol* ‘ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) )
62 57 61 eqbrtrd ( 𝜑 → ( vol* ‘ 𝐾 ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) )
63 ovollecl ( ( 𝐾 ⊆ ℝ ∧ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) ∈ ℝ ∧ ( vol* ‘ 𝐾 ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺𝑗 ) ) ) ) → ( vol* ‘ 𝐾 ) ∈ ℝ )
64 44 56 62 63 syl3anc ( 𝜑 → ( vol* ‘ 𝐾 ) ∈ ℝ )
65 30 64 jca ( 𝜑 → ( 𝐾 = 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺𝑗 ) ) ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) )