| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovnhoi.x | . . 3
⊢ (𝜑 → 𝑋 ∈ Fin) | 
| 2 |  | ovnhoi.c | . . . . 5
⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) | 
| 3 | 2 | a1i 11 | . . . 4
⊢ (𝜑 → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) | 
| 4 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑘𝜑 | 
| 5 |  | ovnhoi.a | . . . . . 6
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) | 
| 6 | 5 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) | 
| 7 |  | ovnhoi.b | . . . . . . 7
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) | 
| 8 | 7 | ffvelcdmda 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) | 
| 9 | 8 | rexrd 11311 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈
ℝ*) | 
| 10 | 4, 6, 9 | hoissrrn2 46593 | . . . 4
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ (ℝ ↑m 𝑋)) | 
| 11 | 3, 10 | eqsstrd 4018 | . . 3
⊢ (𝜑 → 𝐼 ⊆ (ℝ ↑m 𝑋)) | 
| 12 | 1, 11 | ovnxrcl 46584 | . 2
⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) ∈
ℝ*) | 
| 13 |  | icossxr 13472 | . . 3
⊢
(0[,)+∞) ⊆ ℝ* | 
| 14 |  | ovnhoi.l | . . . 4
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) | 
| 15 | 14, 1, 5, 7 | hoidmvcl 46597 | . . 3
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ∈ (0[,)+∞)) | 
| 16 | 13, 15 | sselid 3981 | . 2
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ∈
ℝ*) | 
| 17 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑋 = ∅ →
(voln*‘𝑋) =
(voln*‘∅)) | 
| 18 | 17 | fveq1d 6908 | . . . . . . 7
⊢ (𝑋 = ∅ →
((voln*‘𝑋)‘𝐼) = ((voln*‘∅)‘𝐼)) | 
| 19 | 18 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) = ((voln*‘∅)‘𝐼)) | 
| 20 |  | ixpeq1 8948 | . . . . . . . . . . 11
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) | 
| 21 |  | ixp0x 8966 | . . . . . . . . . . . 12
⊢ X𝑘 ∈
∅ ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = {∅} | 
| 22 | 21 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑋 = ∅ → X𝑘 ∈
∅ ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = {∅}) | 
| 23 | 20, 22 | eqtrd 2777 | . . . . . . . . . 10
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = {∅}) | 
| 24 | 23 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = {∅}) | 
| 25 | 2 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) | 
| 26 |  | reex 11246 | . . . . . . . . . . 11
⊢ ℝ
∈ V | 
| 27 |  | mapdm0 8882 | . . . . . . . . . . 11
⊢ (ℝ
∈ V → (ℝ ↑m ∅) =
{∅}) | 
| 28 | 26, 27 | ax-mp 5 | . . . . . . . . . 10
⊢ (ℝ
↑m ∅) = {∅} | 
| 29 | 28 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → (ℝ
↑m ∅) = {∅}) | 
| 30 | 24, 25, 29 | 3eqtr4d 2787 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐼 = (ℝ ↑m
∅)) | 
| 31 |  | eqimss 4042 | . . . . . . . 8
⊢ (𝐼 = (ℝ ↑m
∅) → 𝐼 ⊆
(ℝ ↑m ∅)) | 
| 32 | 30, 31 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐼 ⊆ (ℝ ↑m
∅)) | 
| 33 | 32 | ovn0val 46565 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) →
((voln*‘∅)‘𝐼) = 0) | 
| 34 | 19, 33 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) = 0) | 
| 35 |  | 0red 11264 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 ∈
ℝ) | 
| 36 | 34, 35 | eqeltrd 2841 | . . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) ∈ ℝ) | 
| 37 |  | eqidd 2738 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 = 0) | 
| 38 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑋 = ∅ → (𝐿‘𝑋) = (𝐿‘∅)) | 
| 39 | 38 | oveqd 7448 | . . . . . . 7
⊢ (𝑋 = ∅ → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵)) | 
| 40 | 39 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵)) | 
| 41 | 5 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:𝑋⟶ℝ) | 
| 42 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝑋 = ∅) | 
| 43 | 42 | feq2d 6722 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ)) | 
| 44 | 41, 43 | mpbid 232 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:∅⟶ℝ) | 
| 45 | 7 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:𝑋⟶ℝ) | 
| 46 | 42 | feq2d 6722 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ)) | 
| 47 | 45, 46 | mpbid 232 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:∅⟶ℝ) | 
| 48 | 14, 44, 47 | hoidmv0val 46598 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘∅)𝐵) = 0) | 
| 49 | 40, 48 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = 0) | 
| 50 | 37, 34, 49 | 3eqtr4d 2787 | . . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) | 
| 51 | 36, 50 | eqled 11364 | . . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) ≤ (𝐴(𝐿‘𝑋)𝐵)) | 
| 52 |  | eqid 2737 | . . . . . 6
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} | 
| 53 |  | eqeq1 2741 | . . . . . . . . 9
⊢ (𝑛 = 𝑗 → (𝑛 = 1 ↔ 𝑗 = 1)) | 
| 54 | 53 | ifbid 4549 | . . . . . . . 8
⊢ (𝑛 = 𝑗 → if(𝑛 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉) = if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) | 
| 55 | 54 | mpteq2dv 5244 | . . . . . . 7
⊢ (𝑛 = 𝑗 → (𝑘 ∈ 𝑋 ↦ if(𝑛 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) = (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) | 
| 56 | 55 | cbvmptv 5255 | . . . . . 6
⊢ (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ if(𝑛 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) | 
| 57 | 1, 5, 7, 2, 52, 56 | ovnhoilem1 46616 | . . . . 5
⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) ≤ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | 
| 58 | 57 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) ≤ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | 
| 59 | 1 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ∈ Fin) | 
| 60 |  | neqne 2948 | . . . . . . 7
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) | 
| 61 | 60 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) | 
| 62 | 5 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝐴:𝑋⟶ℝ) | 
| 63 | 7 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝐵:𝑋⟶ℝ) | 
| 64 | 14, 59, 61, 62, 63 | hoidmvn0val 46599 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | 
| 65 | 64 | eqcomd 2743 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (𝐴(𝐿‘𝑋)𝐵)) | 
| 66 | 58, 65 | breqtrd 5169 | . . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) ≤ (𝐴(𝐿‘𝑋)𝐵)) | 
| 67 | 51, 66 | pm2.61dan 813 | . 2
⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) ≤ (𝐴(𝐿‘𝑋)𝐵)) | 
| 68 | 49, 35 | eqeltrd 2841 | . . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) ∈ ℝ) | 
| 69 | 50 | eqcomd 2743 | . . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = ((voln*‘𝑋)‘𝐼)) | 
| 70 | 68, 69 | eqled 11364 | . . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) ≤ ((voln*‘𝑋)‘𝐼)) | 
| 71 |  | fveq1 6905 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝑐 → (𝑎‘𝑘) = (𝑐‘𝑘)) | 
| 72 | 71 | fvoveq1d 7453 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑐 → (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘)))) | 
| 73 | 72 | prodeq2ad 45607 | . . . . . . . . . 10
⊢ (𝑎 = 𝑐 → ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘)))) | 
| 74 | 73 | ifeq2d 4546 | . . . . . . . . 9
⊢ (𝑎 = 𝑐 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘))))) | 
| 75 |  | fveq1 6905 | . . . . . . . . . . . . 13
⊢ (𝑏 = 𝑑 → (𝑏‘𝑘) = (𝑑‘𝑘)) | 
| 76 | 75 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑏 = 𝑑 → ((𝑐‘𝑘)[,)(𝑏‘𝑘)) = ((𝑐‘𝑘)[,)(𝑑‘𝑘))) | 
| 77 | 76 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (𝑏 = 𝑑 → (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘))) = (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))) | 
| 78 | 77 | prodeq2ad 45607 | . . . . . . . . . 10
⊢ (𝑏 = 𝑑 → ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))) | 
| 79 | 78 | ifeq2d 4546 | . . . . . . . . 9
⊢ (𝑏 = 𝑑 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘))))) | 
| 80 | 74, 79 | cbvmpov 7528 | . . . . . . . 8
⊢ (𝑎 ∈ (ℝ
↑m 𝑥),
𝑏 ∈ (ℝ
↑m 𝑥)
↦ if(𝑥 = ∅, 0,
∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑐 ∈ (ℝ ↑m 𝑥), 𝑑 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘))))) | 
| 81 | 80 | a1i 11 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑐 ∈ (ℝ ↑m 𝑥), 𝑑 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))))) | 
| 82 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (ℝ ↑m 𝑥) = (ℝ ↑m
𝑦)) | 
| 83 |  | eqeq1 2741 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅)) | 
| 84 |  | prodeq1 15943 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘))) = ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))) | 
| 85 | 83, 84 | ifbieq2d 4552 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘))))) | 
| 86 | 82, 82, 85 | mpoeq123dv 7508 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑐 ∈ (ℝ ↑m 𝑥), 𝑑 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘))))) = (𝑐 ∈ (ℝ ↑m 𝑦), 𝑑 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))))) | 
| 87 | 81, 86 | eqtrd 2777 | . . . . . 6
⊢ (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑐 ∈ (ℝ ↑m 𝑦), 𝑑 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))))) | 
| 88 | 87 | cbvmptv 5255 | . . . . 5
⊢ (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ
↑m 𝑥),
𝑏 ∈ (ℝ
↑m 𝑥)
↦ if(𝑥 = ∅, 0,
∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑐 ∈ (ℝ ↑m 𝑦), 𝑑 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))))) | 
| 89 | 14, 88 | eqtri 2765 | . . . 4
⊢ 𝐿 = (𝑦 ∈ Fin ↦ (𝑐 ∈ (ℝ ↑m 𝑦), 𝑑 ∈ (ℝ ↑m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))))) | 
| 90 |  | eqeq1 2741 | . . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑤 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)))) ↔ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)))))) | 
| 91 | 90 | anbi2d 630 | . . . . . . 7
⊢ (𝑤 = 𝑧 → ((𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑤 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))))) | 
| 92 | 91 | rexbidv 3179 | . . . . . 6
⊢ (𝑤 = 𝑧 → (∃ℎ ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑤 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ ∃ℎ ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))))) | 
| 93 |  | simpl 482 | . . . . . . . . . . . . . . 15
⊢ ((ℎ = 𝑖 ∧ 𝑗 ∈ ℕ) → ℎ = 𝑖) | 
| 94 | 93 | fveq1d 6908 | . . . . . . . . . . . . . 14
⊢ ((ℎ = 𝑖 ∧ 𝑗 ∈ ℕ) → (ℎ‘𝑗) = (𝑖‘𝑗)) | 
| 95 | 94 | coeq2d 5873 | . . . . . . . . . . . . 13
⊢ ((ℎ = 𝑖 ∧ 𝑗 ∈ ℕ) → ([,) ∘ (ℎ‘𝑗)) = ([,) ∘ (𝑖‘𝑗))) | 
| 96 | 95 | fveq1d 6908 | . . . . . . . . . . . 12
⊢ ((ℎ = 𝑖 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (ℎ‘𝑗))‘𝑘) = (([,) ∘ (𝑖‘𝑗))‘𝑘)) | 
| 97 | 96 | ixpeq2dv 8953 | . . . . . . . . . . 11
⊢ ((ℎ = 𝑖 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) | 
| 98 | 97 | iuneq2dv 5016 | . . . . . . . . . 10
⊢ (ℎ = 𝑖 → ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) | 
| 99 | 98 | sseq2d 4016 | . . . . . . . . 9
⊢ (ℎ = 𝑖 → (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ↔ 𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) | 
| 100 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ ((ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋) → ℎ = 𝑖) | 
| 101 | 100 | fveq1d 6908 | . . . . . . . . . . . . . . . 16
⊢ ((ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋) → (ℎ‘𝑗) = (𝑖‘𝑗)) | 
| 102 | 101 | coeq2d 5873 | . . . . . . . . . . . . . . 15
⊢ ((ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋) → ([,) ∘ (ℎ‘𝑗)) = ([,) ∘ (𝑖‘𝑗))) | 
| 103 | 102 | fveq1d 6908 | . . . . . . . . . . . . . 14
⊢ ((ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (ℎ‘𝑗))‘𝑘) = (([,) ∘ (𝑖‘𝑗))‘𝑘)) | 
| 104 | 103 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ ((ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) | 
| 105 | 104 | prodeq2dv 15958 | . . . . . . . . . . . 12
⊢ (ℎ = 𝑖 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) | 
| 106 | 105 | mpteq2dv 5244 | . . . . . . . . . . 11
⊢ (ℎ = 𝑖 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) | 
| 107 | 106 | fveq2d 6910 | . . . . . . . . . 10
⊢ (ℎ = 𝑖 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) | 
| 108 | 107 | eqeq2d 2748 | . . . . . . . . 9
⊢ (ℎ = 𝑖 → (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)))) ↔ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) | 
| 109 | 99, 108 | anbi12d 632 | . . . . . . . 8
⊢ (ℎ = 𝑖 → ((𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) | 
| 110 | 109 | cbvrexvw 3238 | . . . . . . 7
⊢
(∃ℎ ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) | 
| 111 | 110 | a1i 11 | . . . . . 6
⊢ (𝑤 = 𝑧 → (∃ℎ ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) | 
| 112 | 92, 111 | bitrd 279 | . . . . 5
⊢ (𝑤 = 𝑧 → (∃ℎ ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑤 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) | 
| 113 | 112 | cbvrabv 3447 | . . . 4
⊢ {𝑤 ∈ ℝ*
∣ ∃ℎ ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑤 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} | 
| 114 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋) → 𝑗 = 𝑛) | 
| 115 | 114 | fveq2d 6910 | . . . . . . . . 9
⊢ ((𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋) → (𝑖‘𝑗) = (𝑖‘𝑛)) | 
| 116 | 115 | fveq1d 6908 | . . . . . . . 8
⊢ ((𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋) → ((𝑖‘𝑗)‘𝑙) = ((𝑖‘𝑛)‘𝑙)) | 
| 117 | 116 | fveq2d 6910 | . . . . . . 7
⊢ ((𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋) → (1st ‘((𝑖‘𝑗)‘𝑙)) = (1st ‘((𝑖‘𝑛)‘𝑙))) | 
| 118 | 117 | mpteq2dva 5242 | . . . . . 6
⊢ (𝑗 = 𝑛 → (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙))) = (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) | 
| 119 | 118 | cbvmptv 5255 | . . . . 5
⊢ (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙)))) = (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) | 
| 120 | 119 | mpteq2i 5247 | . . . 4
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ↦ (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙))))) = (𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ↦ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))))) | 
| 121 | 116 | fveq2d 6910 | . . . . . . 7
⊢ ((𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋) → (2nd ‘((𝑖‘𝑗)‘𝑙)) = (2nd ‘((𝑖‘𝑛)‘𝑙))) | 
| 122 | 121 | mpteq2dva 5242 | . . . . . 6
⊢ (𝑗 = 𝑛 → (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙))) = (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) | 
| 123 | 122 | cbvmptv 5255 | . . . . 5
⊢ (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙)))) = (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) | 
| 124 | 123 | mpteq2i 5247 | . . . 4
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ↦ (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙))))) = (𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ↦ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))))) | 
| 125 | 59, 61, 62, 63, 2, 89, 113, 120, 124 | ovnhoilem2 46617 | . . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) ≤ ((voln*‘𝑋)‘𝐼)) | 
| 126 | 70, 125 | pm2.61dan 813 | . 2
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ ((voln*‘𝑋)‘𝐼)) | 
| 127 | 12, 16, 67, 126 | xrletrid 13197 | 1
⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) |