Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ovncvr2 Structured version   Visualization version   GIF version

Theorem ovncvr2 41465
Description: 𝐵 and 𝑇 are the left and right side of a cover of 𝐴. This cover is made of n-dimensional half-open intervals and approximates the n-dimensional Lebesgue outer volume of 𝐴. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
Hypotheses
Ref Expression
ovncvr2.x (𝜑𝑋 ∈ Fin)
ovncvr2.a (𝜑𝐴 ⊆ (ℝ ↑𝑚 𝑋))
ovncvr2.e (𝜑𝐸 ∈ ℝ+)
ovncvr2.c 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
ovncvr2.l 𝐿 = ( ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ )‘𝑘)))
ovncvr2.d 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)}))
ovncvr2.i (𝜑𝐼 ∈ ((𝐷𝐴)‘𝐸))
ovncvr2.b 𝐵 = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))))
ovncvr2.t 𝑇 = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))))
Assertion
Ref Expression
ovncvr2 (𝜑 → (((𝐵:ℕ⟶(ℝ ↑𝑚 𝑋) ∧ 𝑇:ℕ⟶(ℝ ↑𝑚 𝑋)) ∧ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))
Distinct variable groups:   𝐴,𝑎,𝑖,𝑟   𝐴,𝑙,𝑎   𝐵,   𝐶,𝑎,𝑖,𝑟   𝑖,𝐸,𝑟   ,𝐼,𝑗,𝑘   𝑖,𝐼,𝑗   𝐼,𝑙,𝑗,𝑘   𝐿,𝑎,𝑖,𝑟   𝑇,   𝑋,𝑎,𝑖,𝑗,𝑟   ,𝑋,𝑘   𝑋,𝑙   𝑘,𝑎,𝜑,𝑗   𝜑,   𝜑,𝑟
Allowed substitution hints:   𝜑(𝑖,𝑙)   𝐴(,𝑗,𝑘)   𝐵(𝑖,𝑗,𝑘,𝑟,𝑎,𝑙)   𝐶(,𝑗,𝑘,𝑙)   𝐷(,𝑖,𝑗,𝑘,𝑟,𝑎,𝑙)   𝑇(𝑖,𝑗,𝑘,𝑟,𝑎,𝑙)   𝐸(,𝑗,𝑘,𝑎,𝑙)   𝐼(𝑟,𝑎)   𝐿(,𝑗,𝑘,𝑙)

Proof of Theorem ovncvr2
StepHypRef Expression
1 ovncvr2.c . . . . . . . . . . . . . . . . 17 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
21a1i 11 . . . . . . . . . . . . . . . 16 (𝜑𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)}))
3 sseq1 3786 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝐴 → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘) ↔ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)))
43rabbidv 3338 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝐴 → {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} = {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
54adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑎 = 𝐴) → {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} = {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
6 ovncvr2.a . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ⊆ (ℝ ↑𝑚 𝑋))
7 ovexd 6876 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℝ ↑𝑚 𝑋) ∈ V)
87, 6ssexd 4966 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ V)
9 elpwg 4323 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ V → (𝐴 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↔ 𝐴 ⊆ (ℝ ↑𝑚 𝑋)))
108, 9syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↔ 𝐴 ⊆ (ℝ ↑𝑚 𝑋)))
116, 10mpbird 248 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ 𝒫 (ℝ ↑𝑚 𝑋))
12 ovex 6874 . . . . . . . . . . . . . . . . . 18 (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∈ V
1312rabex 4973 . . . . . . . . . . . . . . . . 17 {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} ∈ V
1413a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} ∈ V)
152, 5, 11, 14fvmptd 6477 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝐴) = {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
16 ssrab2 3847 . . . . . . . . . . . . . . . 16 {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
1716a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
1815, 17eqsstrd 3799 . . . . . . . . . . . . . 14 (𝜑 → (𝐶𝐴) ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
19 ovncvr2.i . . . . . . . . . . . . . . . . 17 (𝜑𝐼 ∈ ((𝐷𝐴)‘𝐸))
20 ovncvr2.d . . . . . . . . . . . . . . . . . . . 20 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)}))
2120a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)})))
22 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝐴 → (𝐶𝑎) = (𝐶𝐴))
2322eleq2d 2830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝐴 → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶𝐴)))
24 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝐴 → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘𝐴))
2524oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝐴 → (((voln*‘𝑋)‘𝑎) +𝑒 𝑟) = (((voln*‘𝑋)‘𝐴) +𝑒 𝑟))
2625breq2d 4821 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝐴 → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)))
2723, 26anbi12d 624 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝐴 → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)) ↔ (𝑖 ∈ (𝐶𝐴) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟))))
2827rabbidva2 3335 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝐴 → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)} = {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)})
2928mpteq2dv 4904 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝐴 → (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)}) = (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)}))
3029adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎 = 𝐴) → (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)}) = (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)}))
31 rpex 40200 . . . . . . . . . . . . . . . . . . . . 21 + ∈ V
3231mptex 6679 . . . . . . . . . . . . . . . . . . . 20 (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)}) ∈ V
3332a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)}) ∈ V)
3421, 30, 11, 33fvmptd 6477 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷𝐴) = (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)}))
35 oveq2 6850 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝐸 → (((voln*‘𝑋)‘𝐴) +𝑒 𝑟) = (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))
3635breq2d 4821 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = 𝐸 → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))
3736rabbidv 3338 . . . . . . . . . . . . . . . . . . 19 (𝑟 = 𝐸 → {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)} = {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)})
3837adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 = 𝐸) → {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)} = {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)})
39 ovncvr2.e . . . . . . . . . . . . . . . . . 18 (𝜑𝐸 ∈ ℝ+)
40 fvex 6388 . . . . . . . . . . . . . . . . . . . 20 (𝐶𝐴) ∈ V
4140rabex 4973 . . . . . . . . . . . . . . . . . . 19 {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ∈ V
4241a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ∈ V)
4334, 38, 39, 42fvmptd 6477 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷𝐴)‘𝐸) = {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)})
4419, 43eleqtrd 2846 . . . . . . . . . . . . . . . 16 (𝜑𝐼 ∈ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)})
45 fveq1 6374 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝐼 → (𝑖𝑗) = (𝐼𝑗))
4645fveq2d 6379 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝐼 → (𝐿‘(𝑖𝑗)) = (𝐿‘(𝐼𝑗)))
4746mpteq2dv 4904 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗))))
4847fveq2d 6379 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝐼 → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))))
4948breq1d 4819 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝐼 → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))
5049elrab 3519 . . . . . . . . . . . . . . . 16 (𝐼 ∈ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ↔ (𝐼 ∈ (𝐶𝐴) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))
5144, 50sylib 209 . . . . . . . . . . . . . . 15 (𝜑 → (𝐼 ∈ (𝐶𝐴) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))
5251simpld 488 . . . . . . . . . . . . . 14 (𝜑𝐼 ∈ (𝐶𝐴))
5318, 52sseldd 3762 . . . . . . . . . . . . 13 (𝜑𝐼 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
54 elmapi 8082 . . . . . . . . . . . . 13 (𝐼 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → 𝐼:ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
5553, 54syl 17 . . . . . . . . . . . 12 (𝜑𝐼:ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
5655adantr 472 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝐼:ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
57 simpr 477 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
5856, 57ffvelrnd 6550 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝐼𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
59 elmapi 8082 . . . . . . . . . 10 ((𝐼𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋) → (𝐼𝑗):𝑋⟶(ℝ × ℝ))
6058, 59syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐼𝑗):𝑋⟶(ℝ × ℝ))
6160ffvelrnda 6549 . . . . . . . 8 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐼𝑗)‘𝑘) ∈ (ℝ × ℝ))
62 xp1st 7398 . . . . . . . 8 (((𝐼𝑗)‘𝑘) ∈ (ℝ × ℝ) → (1st ‘((𝐼𝑗)‘𝑘)) ∈ ℝ)
6361, 62syl 17 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (1st ‘((𝐼𝑗)‘𝑘)) ∈ ℝ)
6463fmpttd 6575 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ)
65 reex 10280 . . . . . . . . 9 ℝ ∈ V
6665a1i 11 . . . . . . . 8 (𝜑 → ℝ ∈ V)
67 ovncvr2.x . . . . . . . 8 (𝜑𝑋 ∈ Fin)
68 elmapg 8073 . . . . . . . 8 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → ((𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
6966, 67, 68syl2anc 579 . . . . . . 7 (𝜑 → ((𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
7069adantr 472 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
7164, 70mpbird 248 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋))
7271fmpttd 6575 . . . 4 (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘)))):ℕ⟶(ℝ ↑𝑚 𝑋))
73 ovncvr2.b . . . . . 6 𝐵 = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))))
7473a1i 11 . . . . 5 (𝜑𝐵 = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘)))))
7574feq1d 6208 . . . 4 (𝜑 → (𝐵:ℕ⟶(ℝ ↑𝑚 𝑋) ↔ (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘)))):ℕ⟶(ℝ ↑𝑚 𝑋)))
7672, 75mpbird 248 . . 3 (𝜑𝐵:ℕ⟶(ℝ ↑𝑚 𝑋))
77 xp2nd 7399 . . . . . . . 8 (((𝐼𝑗)‘𝑘) ∈ (ℝ × ℝ) → (2nd ‘((𝐼𝑗)‘𝑘)) ∈ ℝ)
7861, 77syl 17 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (2nd ‘((𝐼𝑗)‘𝑘)) ∈ ℝ)
7978fmpttd 6575 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ)
80 elmapg 8073 . . . . . . . 8 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → ((𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
8166, 67, 80syl2anc 579 . . . . . . 7 (𝜑 → ((𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
8281adantr 472 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
8379, 82mpbird 248 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋))
8483fmpttd 6575 . . . 4 (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘)))):ℕ⟶(ℝ ↑𝑚 𝑋))
85 ovncvr2.t . . . . . 6 𝑇 = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))))
8685a1i 11 . . . . 5 (𝜑𝑇 = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘)))))
8786feq1d 6208 . . . 4 (𝜑 → (𝑇:ℕ⟶(ℝ ↑𝑚 𝑋) ↔ (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘)))):ℕ⟶(ℝ ↑𝑚 𝑋)))
8884, 87mpbird 248 . . 3 (𝜑𝑇:ℕ⟶(ℝ ↑𝑚 𝑋))
8976, 88jca 507 . 2 (𝜑 → (𝐵:ℕ⟶(ℝ ↑𝑚 𝑋) ∧ 𝑇:ℕ⟶(ℝ ↑𝑚 𝑋)))
9015idi 2 . . . . . 6 (𝜑 → (𝐶𝐴) = {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
9152, 90eleqtrd 2846 . . . . 5 (𝜑𝐼 ∈ {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
92 fveq1 6374 . . . . . . . . . . . 12 (𝑙 = 𝐼 → (𝑙𝑗) = (𝐼𝑗))
9392coeq2d 5453 . . . . . . . . . . 11 (𝑙 = 𝐼 → ([,) ∘ (𝑙𝑗)) = ([,) ∘ (𝐼𝑗)))
9493fveq1d 6377 . . . . . . . . . 10 (𝑙 = 𝐼 → (([,) ∘ (𝑙𝑗))‘𝑘) = (([,) ∘ (𝐼𝑗))‘𝑘))
9594ixpeq2dv 8129 . . . . . . . . 9 (𝑙 = 𝐼X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘))
9695adantr 472 . . . . . . . 8 ((𝑙 = 𝐼𝑗 ∈ ℕ) → X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘))
9796iuneq2dv 4698 . . . . . . 7 (𝑙 = 𝐼 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘) = 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘))
9897sseq2d 3793 . . . . . 6 (𝑙 = 𝐼 → (𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘) ↔ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘)))
9998elrab 3519 . . . . 5 (𝐼 ∈ {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} ↔ (𝐼 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘)))
10091, 99sylib 209 . . . 4 (𝜑 → (𝐼 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘)))
101100simprd 489 . . 3 (𝜑𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘))
10260adantr 472 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (𝐼𝑗):𝑋⟶(ℝ × ℝ))
103 simpr 477 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → 𝑘𝑋)
104102, 103fvovco 40028 . . . . . 6 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (([,) ∘ (𝐼𝑗))‘𝑘) = ((1st ‘((𝐼𝑗)‘𝑘))[,)(2nd ‘((𝐼𝑗)‘𝑘))))
105 mptexg 6677 . . . . . . . . . . . 12 (𝑋 ∈ Fin → (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ V)
10667, 105syl 17 . . . . . . . . . . 11 (𝜑 → (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ V)
107106adantr 472 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ V)
10874, 107fvmpt2d 6482 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐵𝑗) = (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))))
109 fvexd 6390 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (1st ‘((𝐼𝑗)‘𝑘)) ∈ V)
110108, 109fvmpt2d 6482 . . . . . . . 8 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐵𝑗)‘𝑘) = (1st ‘((𝐼𝑗)‘𝑘)))
111110eqcomd 2771 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (1st ‘((𝐼𝑗)‘𝑘)) = ((𝐵𝑗)‘𝑘))
112 mptexg 6677 . . . . . . . . . . . 12 (𝑋 ∈ Fin → (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ V)
11367, 112syl 17 . . . . . . . . . . 11 (𝜑 → (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ V)
114113adantr 472 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ V)
11586, 114fvmpt2d 6482 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) = (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))))
116 fvexd 6390 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (2nd ‘((𝐼𝑗)‘𝑘)) ∈ V)
117115, 116fvmpt2d 6482 . . . . . . . 8 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝑇𝑗)‘𝑘) = (2nd ‘((𝐼𝑗)‘𝑘)))
118117eqcomd 2771 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (2nd ‘((𝐼𝑗)‘𝑘)) = ((𝑇𝑗)‘𝑘))
119111, 118oveq12d 6860 . . . . . 6 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((1st ‘((𝐼𝑗)‘𝑘))[,)(2nd ‘((𝐼𝑗)‘𝑘))) = (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
120104, 119eqtrd 2799 . . . . 5 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (([,) ∘ (𝐼𝑗))‘𝑘) = (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
121120ixpeq2dva 8128 . . . 4 ((𝜑𝑗 ∈ ℕ) → X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘) = X𝑘𝑋 (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
122121iuneq2dv 4698 . . 3 (𝜑 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
123101, 122sseqtrd 3801 . 2 (𝜑𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
124 ovncvr2.l . . . . . . . 8 𝐿 = ( ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ )‘𝑘)))
125124a1i 11 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝐿 = ( ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ )‘𝑘))))
126 coeq2 5449 . . . . . . . . . . . . 13 ( = (𝐼𝑗) → ([,) ∘ ) = ([,) ∘ (𝐼𝑗)))
127126fveq1d 6377 . . . . . . . . . . . 12 ( = (𝐼𝑗) → (([,) ∘ )‘𝑘) = (([,) ∘ (𝐼𝑗))‘𝑘))
128127ad2antlr 718 . . . . . . . . . . 11 (((𝜑 = (𝐼𝑗)) ∧ 𝑘𝑋) → (([,) ∘ )‘𝑘) = (([,) ∘ (𝐼𝑗))‘𝑘))
129128adantllr 710 . . . . . . . . . 10 ((((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) ∧ 𝑘𝑋) → (([,) ∘ )‘𝑘) = (([,) ∘ (𝐼𝑗))‘𝑘))
130104adantlr 706 . . . . . . . . . 10 ((((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) ∧ 𝑘𝑋) → (([,) ∘ (𝐼𝑗))‘𝑘) = ((1st ‘((𝐼𝑗)‘𝑘))[,)(2nd ‘((𝐼𝑗)‘𝑘))))
131119adantlr 706 . . . . . . . . . 10 ((((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) ∧ 𝑘𝑋) → ((1st ‘((𝐼𝑗)‘𝑘))[,)(2nd ‘((𝐼𝑗)‘𝑘))) = (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
132129, 130, 1313eqtrd 2803 . . . . . . . . 9 ((((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) ∧ 𝑘𝑋) → (([,) ∘ )‘𝑘) = (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
133132fveq2d 6379 . . . . . . . 8 ((((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) ∧ 𝑘𝑋) → (vol‘(([,) ∘ )‘𝑘)) = (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))
134133prodeq2dv 14936 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) → ∏𝑘𝑋 (vol‘(([,) ∘ )‘𝑘)) = ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))
13567adantr 472 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
13673fvmpt2 6480 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℕ ∧ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ V) → (𝐵𝑗) = (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))))
13757, 107, 136syl2anc 579 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐵𝑗) = (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))))
138137feq1d 6208 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((𝐵𝑗):𝑋⟶ℝ ↔ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
13964, 138mpbird 248 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝐵𝑗):𝑋⟶ℝ)
140139adantr 472 . . . . . . . . . 10 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (𝐵𝑗):𝑋⟶ℝ)
141140, 103ffvelrnd 6550 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐵𝑗)‘𝑘) ∈ ℝ)
14285fvmpt2 6480 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℕ ∧ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ V) → (𝑇𝑗) = (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))))
14357, 114, 142syl2anc 579 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) = (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))))
144143feq1d 6208 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑗):𝑋⟶ℝ ↔ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
14579, 144mpbird 248 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗):𝑋⟶ℝ)
146145adantr 472 . . . . . . . . . 10 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (𝑇𝑗):𝑋⟶ℝ)
147146, 103ffvelrnd 6550 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝑇𝑗)‘𝑘) ∈ ℝ)
148 volicore 41435 . . . . . . . . 9 ((((𝐵𝑗)‘𝑘) ∈ ℝ ∧ ((𝑇𝑗)‘𝑘) ∈ ℝ) → (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))) ∈ ℝ)
149141, 147, 148syl2anc 579 . . . . . . . 8 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))) ∈ ℝ)
150135, 149fprodrecl 14966 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))) ∈ ℝ)
151125, 134, 58, 150fvmptd 6477 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐿‘(𝐼𝑗)) = ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))
152151eqcomd 2771 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))) = (𝐿‘(𝐼𝑗)))
153152mpteq2dva 4903 . . . 4 (𝜑 → (𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))) = (𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗))))
154153fveq2d 6379 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))))
15551simprd 489 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))
156154, 155eqbrtrd 4831 . 2 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))
15789, 123, 156jca31 510 1 (𝜑 → (((𝐵:ℕ⟶(ℝ ↑𝑚 𝑋) ∧ 𝑇:ℕ⟶(ℝ ↑𝑚 𝑋)) ∧ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  {crab 3059  Vcvv 3350  wss 3732  𝒫 cpw 4315   ciun 4676   class class class wbr 4809  cmpt 4888   × cxp 5275  ccom 5281  wf 6064  cfv 6068  (class class class)co 6842  1st c1st 7364  2nd c2nd 7365  𝑚 cmap 8060  Xcixp 8113  Fincfn 8160  cr 10188  cle 10329  cn 11274  +crp 12028   +𝑒 cxad 12144  [,)cico 12379  cprod 14918  volcvol 23521  Σ^csumge0 41216  voln*covoln 41390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-tpos 7555  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-clim 14504  df-rlim 14505  df-sum 14702  df-prod 14919  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-plusg 16227  df-mulr 16228  df-starv 16229  df-tset 16233  df-ple 16234  df-ds 16236  df-unif 16237  df-rest 16349  df-0g 16368  df-topgen 16370  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-grp 17692  df-minusg 17693  df-subg 17855  df-cmn 18461  df-abl 18462  df-mgp 18757  df-ur 18769  df-ring 18816  df-cring 18817  df-oppr 18890  df-dvdsr 18908  df-unit 18909  df-invr 18939  df-dvr 18950  df-drng 19018  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-cnfld 20020  df-top 20978  df-topon 20995  df-bases 21030  df-cmp 21470  df-ovol 23522  df-vol 23523
This theorem is referenced by:  hspmbllem3  41482
  Copyright terms: Public domain W3C validator