Metamath Proof Explorer

Theorem ovnhoi

Description: The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses ovnhoi.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
ovnhoi.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
ovnhoi.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
ovnhoi.c ⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
ovnhoi.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
Assertion ovnhoi ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ovnhoi.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 ovnhoi.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
3 ovnhoi.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
4 ovnhoi.c ⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
5 ovnhoi.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
6 4 a1i ⊢ ( 𝜑 → 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
7 nfv ⊢ Ⅎ 𝑘 𝜑
8 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
9 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
10 9 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ* )
11 7 8 10 hoissrrn2 ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
12 6 11 eqsstrd ⊢ ( 𝜑 → 𝐼 ⊆ ( ℝ ↑m 𝑋 ) )
13 1 12 ovnxrcl ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) ∈ ℝ* )
14 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
15 5 1 2 3 hoidmvcl ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ( 0 [,) +∞ ) )
16 14 15 sselid ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ℝ* )
17 fveq2 ⊢ ( 𝑋 = ∅ → ( voln* ‘ 𝑋 ) = ( voln* ‘ ∅ ) )
18 17 fveq1d ⊢ ( 𝑋 = ∅ → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) = ( ( voln* ‘ ∅ ) ‘ 𝐼 ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) = ( ( voln* ‘ ∅ ) ‘ 𝐼 ) )
20 ixpeq1 ⊢ ( 𝑋 = ∅ → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = X 𝑘 ∈ ∅ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
21 ixp0x ⊢ X 𝑘 ∈ ∅ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = { ∅ }
22 21 a1i ⊢ ( 𝑋 = ∅ → X 𝑘 ∈ ∅ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = { ∅ } )
23 20 22 eqtrd ⊢ ( 𝑋 = ∅ → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = { ∅ } )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = { ∅ } )
25 4 a1i ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
26 reex ⊢ ℝ ∈ V
27 mapdm0 ⊢ ( ℝ ∈ V → ( ℝ ↑m ∅ ) = { ∅ } )
28 26 27 ax-mp ⊢ ( ℝ ↑m ∅ ) = { ∅ }
29 28 a1i ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ℝ ↑m ∅ ) = { ∅ } )
30 24 25 29 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐼 = ( ℝ ↑m ∅ ) )
31 eqimss ⊢ ( 𝐼 = ( ℝ ↑m ∅ ) → 𝐼 ⊆ ( ℝ ↑m ∅ ) )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐼 ⊆ ( ℝ ↑m ∅ ) )
33 32 ovn0val ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ ∅ ) ‘ 𝐼 ) = 0 )
34 19 33 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) = 0 )
35 0red ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 0 ∈ ℝ )
36 34 35 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) ∈ ℝ )
37 eqidd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 0 = 0 )
38 fveq2 ⊢ ( 𝑋 = ∅ → ( 𝐿 ‘ 𝑋 ) = ( 𝐿 ‘ ∅ ) )
39 38 oveqd ⊢ ( 𝑋 = ∅ → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐵 ) )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐵 ) )
41 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 : 𝑋 ⟶ ℝ )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝑋 = ∅ )
43 42 feq2d ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 : 𝑋 ⟶ ℝ ↔ 𝐴 : ∅ ⟶ ℝ ) )
44 41 43 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 : ∅ ⟶ ℝ )
45 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐵 : 𝑋 ⟶ ℝ )
46 42 feq2d ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐵 : 𝑋 ⟶ ℝ ↔ 𝐵 : ∅ ⟶ ℝ ) )
47 45 46 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐵 : ∅ ⟶ ℝ )
48 5 44 47 hoidmv0val ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐵 ) = 0 )
49 40 48 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = 0 )
50 37 34 49 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
51 36 50 eqled ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) ≤ ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
52 eqid ⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
53 eqeq1 ⊢ ( 𝑛 = 𝑗 → ( 𝑛 = 1 ↔ 𝑗 = 1 ) )
54 53 ifbid ⊢ ( 𝑛 = 𝑗 → if ( 𝑛 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) = if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) )
55 54 mpteq2dv ⊢ ( 𝑛 = 𝑗 → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑛 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) = ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) )
56 55 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑛 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑗 = 1 , ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ , ⟨ 0 , 0 ⟩ ) ) )
57 1 2 3 4 52 56 ovnhoilem1 ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
58 57 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) ≤ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
59 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ∈ Fin )
60 neqne ⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
61 60 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
62 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝐴 : 𝑋 ⟶ ℝ )
63 3 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝐵 : 𝑋 ⟶ ℝ )
64 5 59 61 62 63 hoidmvn0val ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
65 64 eqcomd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
66 58 65 breqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) ≤ ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
67 51 66 pm2.61dan ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) ≤ ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
68 49 35 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ∈ ℝ )
69 50 eqcomd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) )
70 68 69 eqled ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) )
71 fveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ‘ 𝑘 ) = ( 𝑐 ‘ 𝑘 ) )
72 71 fvoveq1d ⊢ ( 𝑎 = 𝑐 → ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) )
73 72 prodeq2ad ⊢ ( 𝑎 = 𝑐 → ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) )
74 73 ifeq2d ⊢ ( 𝑎 = 𝑐 → if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) = if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) )
75 fveq1 ⊢ ( 𝑏 = 𝑑 → ( 𝑏 ‘ 𝑘 ) = ( 𝑑 ‘ 𝑘 ) )
76 75 oveq2d ⊢ ( 𝑏 = 𝑑 → ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) = ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) )
77 76 fveq2d ⊢ ( 𝑏 = 𝑑 → ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) )
78 77 prodeq2ad ⊢ ( 𝑏 = 𝑑 → ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) )
79 78 ifeq2d ⊢ ( 𝑏 = 𝑑 → if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) = if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) ) )
80 74 79 cbvmpov ⊢ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑥 ) , 𝑑 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) ) )
81 80 a1i ⊢ ( 𝑥 = 𝑦 → ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑥 ) , 𝑑 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) ) ) )
82 oveq2 ⊢ ( 𝑥 = 𝑦 → ( ℝ ↑m 𝑥 ) = ( ℝ ↑m 𝑦 ) )
83 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ∅ ↔ 𝑦 = ∅ ) )
84 prodeq1 ⊢ ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑦 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) )
85 83 84 ifbieq2d ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) ) = if ( 𝑦 = ∅ , 0 , ∏ 𝑘 ∈ 𝑦 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) ) )
86 82 82 85 mpoeq123dv ⊢ ( 𝑥 = 𝑦 → ( 𝑐 ∈ ( ℝ ↑m 𝑥 ) , 𝑑 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑦 ) , 𝑑 ∈ ( ℝ ↑m 𝑦 ) ↦ if ( 𝑦 = ∅ , 0 , ∏ 𝑘 ∈ 𝑦 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) ) ) )
87 81 86 eqtrd ⊢ ( 𝑥 = 𝑦 → ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑦 ) , 𝑑 ∈ ( ℝ ↑m 𝑦 ) ↦ if ( 𝑦 = ∅ , 0 , ∏ 𝑘 ∈ 𝑦 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) ) ) )
88 87 cbvmptv ⊢ ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) = ( 𝑦 ∈ Fin ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑦 ) , 𝑑 ∈ ( ℝ ↑m 𝑦 ) ↦ if ( 𝑦 = ∅ , 0 , ∏ 𝑘 ∈ 𝑦 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) ) ) )
89 5 88 eqtri ⊢ 𝐿 = ( 𝑦 ∈ Fin ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑦 ) , 𝑑 ∈ ( ℝ ↑m 𝑦 ) ↦ if ( 𝑦 = ∅ , 0 , ∏ 𝑘 ∈ 𝑦 ( vol ‘ ( ( 𝑐 ‘ 𝑘 ) [,) ( 𝑑 ‘ 𝑘 ) ) ) ) ) )
90 eqeq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
91 90 anbi2d ⊢ ( 𝑤 = 𝑧 → ( ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑤 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
92 91 rexbidv ⊢ ( 𝑤 = 𝑧 → ( ∃ ℎ ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑤 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ∃ ℎ ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
93 simpl ⊢ ( ( ℎ = 𝑖 ∧ 𝑗 ∈ ℕ ) → ℎ = 𝑖 )
94 93 fveq1d ⊢ ( ( ℎ = 𝑖 ∧ 𝑗 ∈ ℕ ) → ( ℎ ‘ 𝑗 ) = ( 𝑖 ‘ 𝑗 ) )
95 94 coeq2d ⊢ ( ( ℎ = 𝑖 ∧ 𝑗 ∈ ℕ ) → ( [,) ∘ ( ℎ ‘ 𝑗 ) ) = ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) )
96 95 fveq1d ⊢ ( ( ℎ = 𝑖 ∧ 𝑗 ∈ ℕ ) → ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
97 96 ixpeq2dv ⊢ ( ( ℎ = 𝑖 ∧ 𝑗 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
98 97 iuneq2dv ⊢ ( ℎ = 𝑖 → ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) = ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
99 98 sseq2d ⊢ ( ℎ = 𝑖 → ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
100 simpl ⊢ ( ( ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋 ) → ℎ = 𝑖 )
101 100 fveq1d ⊢ ( ( ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋 ) → ( ℎ ‘ 𝑗 ) = ( 𝑖 ‘ 𝑗 ) )
102 101 coeq2d ⊢ ( ( ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋 ) → ( [,) ∘ ( ℎ ‘ 𝑗 ) ) = ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) )
103 102 fveq1d ⊢ ( ( ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) = ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
104 103 fveq2d ⊢ ( ( ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
105 104 prodeq2dv ⊢ ( ℎ = 𝑖 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
106 105 mpteq2dv ⊢ ( ℎ = 𝑖 → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
107 106 fveq2d ⊢ ( ℎ = 𝑖 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
108 107 eqeq2d ⊢ ( ℎ = 𝑖 → ( 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ↔ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
109 99 108 anbi12d ⊢ ( ℎ = 𝑖 → ( ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
110 109 cbvrexvw ⊢ ( ∃ ℎ ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
111 110 a1i ⊢ ( 𝑤 = 𝑧 → ( ∃ ℎ ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
112 92 111 bitrd ⊢ ( 𝑤 = 𝑧 → ( ∃ ℎ ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑤 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
113 112 cbvrabv ⊢ { 𝑤 ∈ ℝ* ∣ ∃ ℎ ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑤 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( ℎ ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐼 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
114 simpl ⊢ ( ( 𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋 ) → 𝑗 = 𝑛 )
115 114 fveq2d ⊢ ( ( 𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋 ) → ( 𝑖 ‘ 𝑗 ) = ( 𝑖 ‘ 𝑛 ) )
116 115 fveq1d ⊢ ( ( 𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋 ) → ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) = ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) )
117 116 fveq2d ⊢ ( ( 𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋 ) → ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) = ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) )
118 117 mpteq2dva ⊢ ( 𝑗 = 𝑛 → ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
119 118 cbvmptv ⊢ ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
120 119 mpteq2i ⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↦ ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ) ) = ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
121 116 fveq2d ⊢ ( ( 𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋 ) → ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) = ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) )
122 121 mpteq2dva ⊢ ( 𝑗 = 𝑛 → ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) = ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
123 122 cbvmptv ⊢ ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) )
124 123 mpteq2i ⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↦ ( 𝑗 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑙 ) ) ) ) ) = ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ↦ ( 𝑛 ∈ ℕ ↦ ( 𝑙 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑛 ) ‘ 𝑙 ) ) ) ) )
125 59 61 62 63 4 89 113 120 124 ovnhoilem2 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) )
126 70 125 pm2.61dan ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) )
127 13 16 67 126 xrletrid ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )