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 39298
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 3588 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝐴 → (𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘) ↔ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)))
43rabbidv 3163 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝐴 → {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} = {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
54adantl 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑎 = 𝐴) → {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} = {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
6 ovncvr2.a . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ⊆ (ℝ ↑𝑚 𝑋))
7 ovex 6555 . . . . . . . . . . . . . . . . . . . 20 (ℝ ↑𝑚 𝑋) ∈ V
87a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℝ ↑𝑚 𝑋) ∈ V)
98, 6ssexd 4728 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ V)
10 elpwg 4115 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ V → (𝐴 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↔ 𝐴 ⊆ (ℝ ↑𝑚 𝑋)))
119, 10syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↔ 𝐴 ⊆ (ℝ ↑𝑚 𝑋)))
126, 11mpbird 245 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ 𝒫 (ℝ ↑𝑚 𝑋))
13 ovex 6555 . . . . . . . . . . . . . . . . . 18 (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∈ V
1413rabex 4735 . . . . . . . . . . . . . . . . 17 {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} ∈ V
1514a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} ∈ V)
162, 5, 12, 15fvmptd 6182 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝐴) = {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
17 ssrab2 3649 . . . . . . . . . . . . . . . 16 {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
1817a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
1916, 18eqsstrd 3601 . . . . . . . . . . . . . 14 (𝜑 → (𝐶𝐴) ⊆ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
20 ovncvr2.i . . . . . . . . . . . . . . . . 17 (𝜑𝐼 ∈ ((𝐷𝐴)‘𝐸))
21 ovncvr2.d . . . . . . . . . . . . . . . . . . . 20 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)}))
2221a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)})))
23 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝐴 → (𝐶𝑎) = (𝐶𝐴))
2423eleq2d 2672 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝐴 → (𝑖 ∈ (𝐶𝑎) ↔ 𝑖 ∈ (𝐶𝐴)))
25 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝐴 → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘𝐴))
2625oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝐴 → (((voln*‘𝑋)‘𝑎) +𝑒 𝑟) = (((voln*‘𝑋)‘𝐴) +𝑒 𝑟))
2726breq2d 4589 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 𝐴 → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)))
2824, 27anbi12d 742 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝐴 → ((𝑖 ∈ (𝐶𝑎) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)) ↔ (𝑖 ∈ (𝐶𝐴) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟))))
2928rabbidva2 3161 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝐴 → {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)} = {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)})
3029mpteq2dv 4667 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝐴 → (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)}) = (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)}))
3130adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎 = 𝐴) → (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)}) = (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)}))
32 rpex 38300 . . . . . . . . . . . . . . . . . . . . 21 + ∈ V
3332mptex 6368 . . . . . . . . . . . . . . . . . . . 20 (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)}) ∈ V
3433a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)}) ∈ V)
3522, 31, 12, 34fvmptd 6182 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷𝐴) = (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)}))
36 oveq2 6535 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝐸 → (((voln*‘𝑋)‘𝐴) +𝑒 𝑟) = (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))
3736breq2d 4589 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = 𝐸 → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))
3837rabbidv 3163 . . . . . . . . . . . . . . . . . . 19 (𝑟 = 𝐸 → {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)} = {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)})
3938adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟 = 𝐸) → {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑟)} = {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)})
40 ovncvr2.e . . . . . . . . . . . . . . . . . 18 (𝜑𝐸 ∈ ℝ+)
41 fvex 6098 . . . . . . . . . . . . . . . . . . . 20 (𝐶𝐴) ∈ V
4241rabex 4735 . . . . . . . . . . . . . . . . . . 19 {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ∈ V
4342a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ∈ V)
4435, 39, 40, 43fvmptd 6182 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷𝐴)‘𝐸) = {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)})
4520, 44eleqtrd 2689 . . . . . . . . . . . . . . . 16 (𝜑𝐼 ∈ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)})
46 fveq1 6087 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝐼 → (𝑖𝑗) = (𝐼𝑗))
4746fveq2d 6092 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝐼 → (𝐿‘(𝑖𝑗)) = (𝐿‘(𝐼𝑗)))
4847mpteq2dv 4667 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗))))
4948fveq2d 6092 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝐼 → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) = (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))))
5049breq1d 4587 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝐼 → ((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) ↔ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))
5150elrab 3330 . . . . . . . . . . . . . . . 16 (𝐼 ∈ {𝑖 ∈ (𝐶𝐴) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ↔ (𝐼 ∈ (𝐶𝐴) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))
5245, 51sylib 206 . . . . . . . . . . . . . . 15 (𝜑 → (𝐼 ∈ (𝐶𝐴) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))
5352simpld 473 . . . . . . . . . . . . . 14 (𝜑𝐼 ∈ (𝐶𝐴))
5419, 53sseldd 3568 . . . . . . . . . . . . 13 (𝜑𝐼 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ))
55 elmapi 7742 . . . . . . . . . . . . 13 (𝐼 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) → 𝐼:ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
5654, 55syl 17 . . . . . . . . . . . 12 (𝜑𝐼:ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
5756adantr 479 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝐼:ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋))
58 simpr 475 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
5957, 58ffvelrnd 6253 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝐼𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
60 elmapi 7742 . . . . . . . . . 10 ((𝐼𝑗) ∈ ((ℝ × ℝ) ↑𝑚 𝑋) → (𝐼𝑗):𝑋⟶(ℝ × ℝ))
6159, 60syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐼𝑗):𝑋⟶(ℝ × ℝ))
6261ffvelrnda 6252 . . . . . . . 8 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐼𝑗)‘𝑘) ∈ (ℝ × ℝ))
63 xp1st 7066 . . . . . . . 8 (((𝐼𝑗)‘𝑘) ∈ (ℝ × ℝ) → (1st ‘((𝐼𝑗)‘𝑘)) ∈ ℝ)
6462, 63syl 17 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (1st ‘((𝐼𝑗)‘𝑘)) ∈ ℝ)
65 eqid 2609 . . . . . . 7 (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) = (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘)))
6664, 65fmptd 6277 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ)
67 reex 9883 . . . . . . . . 9 ℝ ∈ V
6867a1i 11 . . . . . . . 8 (𝜑 → ℝ ∈ V)
69 ovncvr2.x . . . . . . . 8 (𝜑𝑋 ∈ Fin)
70 elmapg 7734 . . . . . . . 8 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → ((𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
7168, 69, 70syl2anc 690 . . . . . . 7 (𝜑 → ((𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
7271adantr 479 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
7366, 72mpbird 245 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋))
74 eqid 2609 . . . . 5 (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘)))) = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))))
7573, 74fmptd 6277 . . . 4 (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘)))):ℕ⟶(ℝ ↑𝑚 𝑋))
76 ovncvr2.b . . . . . 6 𝐵 = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))))
7776a1i 11 . . . . 5 (𝜑𝐵 = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘)))))
7877feq1d 5929 . . . 4 (𝜑 → (𝐵:ℕ⟶(ℝ ↑𝑚 𝑋) ↔ (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘)))):ℕ⟶(ℝ ↑𝑚 𝑋)))
7975, 78mpbird 245 . . 3 (𝜑𝐵:ℕ⟶(ℝ ↑𝑚 𝑋))
80 xp2nd 7067 . . . . . . . 8 (((𝐼𝑗)‘𝑘) ∈ (ℝ × ℝ) → (2nd ‘((𝐼𝑗)‘𝑘)) ∈ ℝ)
8162, 80syl 17 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (2nd ‘((𝐼𝑗)‘𝑘)) ∈ ℝ)
82 eqid 2609 . . . . . . 7 (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) = (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘)))
8381, 82fmptd 6277 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ)
84 elmapg 7734 . . . . . . . 8 ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → ((𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
8568, 69, 84syl2anc 690 . . . . . . 7 (𝜑 → ((𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
8685adantr 479 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋) ↔ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
8783, 86mpbird 245 . . . . 5 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ (ℝ ↑𝑚 𝑋))
88 eqid 2609 . . . . 5 (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘)))) = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))))
8987, 88fmptd 6277 . . . 4 (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘)))):ℕ⟶(ℝ ↑𝑚 𝑋))
90 ovncvr2.t . . . . . 6 𝑇 = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))))
9190a1i 11 . . . . 5 (𝜑𝑇 = (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘)))))
9291feq1d 5929 . . . 4 (𝜑 → (𝑇:ℕ⟶(ℝ ↑𝑚 𝑋) ↔ (𝑗 ∈ ℕ ↦ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘)))):ℕ⟶(ℝ ↑𝑚 𝑋)))
9389, 92mpbird 245 . . 3 (𝜑𝑇:ℕ⟶(ℝ ↑𝑚 𝑋))
9479, 93jca 552 . 2 (𝜑 → (𝐵:ℕ⟶(ℝ ↑𝑚 𝑋) ∧ 𝑇:ℕ⟶(ℝ ↑𝑚 𝑋)))
9516idi 2 . . . . . 6 (𝜑 → (𝐶𝐴) = {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
9653, 95eleqtrd 2689 . . . . 5 (𝜑𝐼 ∈ {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
97 fveq1 6087 . . . . . . . . . . . 12 (𝑙 = 𝐼 → (𝑙𝑗) = (𝐼𝑗))
9897coeq2d 5194 . . . . . . . . . . 11 (𝑙 = 𝐼 → ([,) ∘ (𝑙𝑗)) = ([,) ∘ (𝐼𝑗)))
9998fveq1d 6090 . . . . . . . . . 10 (𝑙 = 𝐼 → (([,) ∘ (𝑙𝑗))‘𝑘) = (([,) ∘ (𝐼𝑗))‘𝑘))
10099ixpeq2dv 7787 . . . . . . . . 9 (𝑙 = 𝐼X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘))
101100adantr 479 . . . . . . . 8 ((𝑙 = 𝐼𝑗 ∈ ℕ) → X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘) = X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘))
102101iuneq2dv 4472 . . . . . . 7 (𝑙 = 𝐼 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘) = 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘))
103102sseq2d 3595 . . . . . 6 (𝑙 = 𝐼 → (𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘) ↔ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘)))
104103elrab 3330 . . . . 5 (𝐼 ∈ {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)} ↔ (𝐼 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘)))
10596, 104sylib 206 . . . 4 (𝜑 → (𝐼 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘)))
106105simprd 477 . . 3 (𝜑𝐴 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘))
10761adantr 479 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (𝐼𝑗):𝑋⟶(ℝ × ℝ))
108 simpr 475 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → 𝑘𝑋)
109107, 108fvovco 38172 . . . . . 6 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (([,) ∘ (𝐼𝑗))‘𝑘) = ((1st ‘((𝐼𝑗)‘𝑘))[,)(2nd ‘((𝐼𝑗)‘𝑘))))
110 mptexg 6367 . . . . . . . . . . . 12 (𝑋 ∈ Fin → (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ V)
11169, 110syl 17 . . . . . . . . . . 11 (𝜑 → (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ V)
112111adantr 479 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ V)
11377, 112fvmpt2d 6187 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐵𝑗) = (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))))
114 fvex 6098 . . . . . . . . . 10 (1st ‘((𝐼𝑗)‘𝑘)) ∈ V
115114a1i 11 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (1st ‘((𝐼𝑗)‘𝑘)) ∈ V)
116113, 115fvmpt2d 6187 . . . . . . . 8 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐵𝑗)‘𝑘) = (1st ‘((𝐼𝑗)‘𝑘)))
117116eqcomd 2615 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (1st ‘((𝐼𝑗)‘𝑘)) = ((𝐵𝑗)‘𝑘))
118 mptexg 6367 . . . . . . . . . . . 12 (𝑋 ∈ Fin → (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ V)
11969, 118syl 17 . . . . . . . . . . 11 (𝜑 → (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ V)
120119adantr 479 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ V)
12191, 120fvmpt2d 6187 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) = (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))))
122 fvex 6098 . . . . . . . . . 10 (2nd ‘((𝐼𝑗)‘𝑘)) ∈ V
123122a1i 11 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (2nd ‘((𝐼𝑗)‘𝑘)) ∈ V)
124121, 123fvmpt2d 6187 . . . . . . . 8 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝑇𝑗)‘𝑘) = (2nd ‘((𝐼𝑗)‘𝑘)))
125124eqcomd 2615 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (2nd ‘((𝐼𝑗)‘𝑘)) = ((𝑇𝑗)‘𝑘))
126117, 125oveq12d 6545 . . . . . 6 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((1st ‘((𝐼𝑗)‘𝑘))[,)(2nd ‘((𝐼𝑗)‘𝑘))) = (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
127109, 126eqtrd 2643 . . . . 5 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (([,) ∘ (𝐼𝑗))‘𝑘) = (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
128127ixpeq2dva 7786 . . . 4 ((𝜑𝑗 ∈ ℕ) → X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘) = X𝑘𝑋 (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
129128iuneq2dv 4472 . . 3 (𝜑 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝐼𝑗))‘𝑘) = 𝑗 ∈ ℕ X𝑘𝑋 (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
130106, 129sseqtrd 3603 . 2 (𝜑𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
131 ovncvr2.l . . . . . . . 8 𝐿 = ( ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ )‘𝑘)))
132131a1i 11 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝐿 = ( ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ )‘𝑘))))
133 coeq2 5190 . . . . . . . . . . . . 13 ( = (𝐼𝑗) → ([,) ∘ ) = ([,) ∘ (𝐼𝑗)))
134133fveq1d 6090 . . . . . . . . . . . 12 ( = (𝐼𝑗) → (([,) ∘ )‘𝑘) = (([,) ∘ (𝐼𝑗))‘𝑘))
135134ad2antlr 758 . . . . . . . . . . 11 (((𝜑 = (𝐼𝑗)) ∧ 𝑘𝑋) → (([,) ∘ )‘𝑘) = (([,) ∘ (𝐼𝑗))‘𝑘))
136135adantllr 750 . . . . . . . . . 10 ((((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) ∧ 𝑘𝑋) → (([,) ∘ )‘𝑘) = (([,) ∘ (𝐼𝑗))‘𝑘))
137109adantlr 746 . . . . . . . . . 10 ((((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) ∧ 𝑘𝑋) → (([,) ∘ (𝐼𝑗))‘𝑘) = ((1st ‘((𝐼𝑗)‘𝑘))[,)(2nd ‘((𝐼𝑗)‘𝑘))))
138126adantlr 746 . . . . . . . . . 10 ((((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) ∧ 𝑘𝑋) → ((1st ‘((𝐼𝑗)‘𝑘))[,)(2nd ‘((𝐼𝑗)‘𝑘))) = (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
139136, 137, 1383eqtrd 2647 . . . . . . . . 9 ((((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) ∧ 𝑘𝑋) → (([,) ∘ )‘𝑘) = (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))
140139fveq2d 6092 . . . . . . . 8 ((((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) ∧ 𝑘𝑋) → (vol‘(([,) ∘ )‘𝑘)) = (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))
141140prodeq2dv 14438 . . . . . . 7 (((𝜑𝑗 ∈ ℕ) ∧ = (𝐼𝑗)) → ∏𝑘𝑋 (vol‘(([,) ∘ )‘𝑘)) = ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))
14269adantr 479 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
14376fvmpt2 6185 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℕ ∧ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))) ∈ V) → (𝐵𝑗) = (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))))
14458, 112, 143syl2anc 690 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐵𝑗) = (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))))
145144feq1d 5929 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((𝐵𝑗):𝑋⟶ℝ ↔ (𝑘𝑋 ↦ (1st ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
14666, 145mpbird 245 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝐵𝑗):𝑋⟶ℝ)
147146adantr 479 . . . . . . . . . 10 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (𝐵𝑗):𝑋⟶ℝ)
148147, 108ffvelrnd 6253 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝐵𝑗)‘𝑘) ∈ ℝ)
14990fvmpt2 6185 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℕ ∧ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))) ∈ V) → (𝑇𝑗) = (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))))
15058, 120, 149syl2anc 690 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) = (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))))
151150feq1d 5929 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((𝑇𝑗):𝑋⟶ℝ ↔ (𝑘𝑋 ↦ (2nd ‘((𝐼𝑗)‘𝑘))):𝑋⟶ℝ))
15283, 151mpbird 245 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗):𝑋⟶ℝ)
153152adantr 479 . . . . . . . . . 10 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (𝑇𝑗):𝑋⟶ℝ)
154153, 108ffvelrnd 6253 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → ((𝑇𝑗)‘𝑘) ∈ ℝ)
155 volicore 39268 . . . . . . . . 9 ((((𝐵𝑗)‘𝑘) ∈ ℝ ∧ ((𝑇𝑗)‘𝑘) ∈ ℝ) → (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))) ∈ ℝ)
156148, 154, 155syl2anc 690 . . . . . . . 8 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘𝑋) → (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))) ∈ ℝ)
157142, 156fprodrecl 14468 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))) ∈ ℝ)
158132, 141, 59, 157fvmptd 6182 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (𝐿‘(𝐼𝑗)) = ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))
159158eqcomd 2615 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))) = (𝐿‘(𝐼𝑗)))
160159mpteq2dva 4666 . . . 4 (𝜑 → (𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘)))) = (𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗))))
161160fveq2d 6092 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))) = (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))))
16252simprd 477 . . 3 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))
163161, 162eqbrtrd 4599 . 2 (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))
16494, 130, 163jca31 554 1 (𝜑 → (((𝐵:ℕ⟶(ℝ ↑𝑚 𝑋) ∧ 𝑇:ℕ⟶(ℝ ↑𝑚 𝑋)) ∧ 𝐴 𝑗 ∈ ℕ X𝑘𝑋 (((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(((𝐵𝑗)‘𝑘)[,)((𝑇𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  {crab 2899  Vcvv 3172  wss 3539  𝒫 cpw 4107   ciun 4449   class class class wbr 4577  cmpt 4637   × cxp 5026  ccom 5032  wf 5786  cfv 5790  (class class class)co 6527  1st c1st 7034  2nd c2nd 7035  𝑚 cmap 7721  Xcixp 7771  Fincfn 7818  cr 9791  cle 9931  cn 10867  +crp 11664   +𝑒 cxad 11776  [,)cico 12004  cprod 14420  volcvol 22956  Σ^csumge0 39052  voln*covoln 39223
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-tpos 7216  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-dec 11326  df-uz 11520  df-q 11621  df-rp 11665  df-xneg 11778  df-xadd 11779  df-xmul 11780  df-ioo 12006  df-ico 12008  df-icc 12009  df-fz 12153  df-fzo 12290  df-fl 12410  df-seq 12619  df-exp 12678  df-hash 12935  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-clim 14013  df-rlim 14014  df-sum 14211  df-prod 14421  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-sets 15647  df-ress 15648  df-plusg 15727  df-mulr 15728  df-starv 15729  df-tset 15733  df-ple 15734  df-ds 15737  df-unif 15738  df-rest 15852  df-0g 15871  df-topgen 15873  df-mgm 17011  df-sgrp 17053  df-mnd 17064  df-grp 17194  df-minusg 17195  df-subg 17360  df-cmn 17964  df-abl 17965  df-mgp 18259  df-ur 18271  df-ring 18318  df-cring 18319  df-oppr 18392  df-dvdsr 18410  df-unit 18411  df-invr 18441  df-dvr 18452  df-drng 18518  df-psmet 19505  df-xmet 19506  df-met 19507  df-bl 19508  df-mopn 19509  df-cnfld 19514  df-top 20463  df-bases 20464  df-topon 20465  df-cmp 20942  df-ovol 22957  df-vol 22958
This theorem is referenced by:  hspmbllem3  39315
  Copyright terms: Public domain W3C validator