Step | Hyp | Ref
| Expression |
1 | | ovnhoi.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | ovnhoi.c |
. . . . 5
⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
4 | | nfv 1843 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
5 | | ovnhoi.a |
. . . . . 6
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
6 | 5 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
7 | | ovnhoi.b |
. . . . . . 7
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
8 | 7 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
9 | 8 | rexrd 10089 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈
ℝ*) |
10 | 4, 6, 9 | hoissrrn2 40792 |
. . . 4
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ (ℝ
↑𝑚 𝑋)) |
11 | 3, 10 | eqsstrd 3639 |
. . 3
⊢ (𝜑 → 𝐼 ⊆ (ℝ ↑𝑚
𝑋)) |
12 | 1, 11 | ovnxrcl 40783 |
. 2
⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) ∈
ℝ*) |
13 | | icossxr 12258 |
. . 3
⊢
(0[,)+∞) ⊆ ℝ* |
14 | | ovnhoi.l |
. . . 4
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
15 | 14, 1, 5, 7 | hoidmvcl 40796 |
. . 3
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ∈ (0[,)+∞)) |
16 | 13, 15 | sseldi 3601 |
. 2
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ∈
ℝ*) |
17 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑋 = ∅ →
(voln*‘𝑋) =
(voln*‘∅)) |
18 | 17 | fveq1d 6193 |
. . . . . . 7
⊢ (𝑋 = ∅ →
((voln*‘𝑋)‘𝐼) = ((voln*‘∅)‘𝐼)) |
19 | 18 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) = ((voln*‘∅)‘𝐼)) |
20 | | ixpeq1 7919 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = X𝑘 ∈ ∅ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
21 | | ixp0x 7936 |
. . . . . . . . . . . 12
⊢ X𝑘 ∈
∅ ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = {∅} |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → X𝑘 ∈
∅ ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = {∅}) |
23 | 20, 22 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = {∅}) |
24 | 23 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = {∅}) |
25 | 2 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
26 | | reex 10027 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
27 | | mapdm0 7872 |
. . . . . . . . . . 11
⊢ (ℝ
∈ V → (ℝ ↑𝑚 ∅) =
{∅}) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . 10
⊢ (ℝ
↑𝑚 ∅) = {∅} |
29 | 28 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → (ℝ
↑𝑚 ∅) = {∅}) |
30 | 24, 25, 29 | 3eqtr4d 2666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐼 = (ℝ ↑𝑚
∅)) |
31 | | eqimss 3657 |
. . . . . . . 8
⊢ (𝐼 = (ℝ
↑𝑚 ∅) → 𝐼 ⊆ (ℝ ↑𝑚
∅)) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐼 ⊆ (ℝ ↑𝑚
∅)) |
33 | 32 | ovn0val 40764 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) →
((voln*‘∅)‘𝐼) = 0) |
34 | 19, 33 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) = 0) |
35 | | 0red 10041 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 ∈
ℝ) |
36 | 34, 35 | eqeltrd 2701 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) ∈ ℝ) |
37 | | eqidd 2623 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 = 0) |
38 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑋 = ∅ → (𝐿‘𝑋) = (𝐿‘∅)) |
39 | 38 | oveqd 6667 |
. . . . . . 7
⊢ (𝑋 = ∅ → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵)) |
40 | 39 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵)) |
41 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:𝑋⟶ℝ) |
42 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝑋 = ∅) |
43 | 42 | feq2d 6031 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ)) |
44 | 41, 43 | mpbid 222 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:∅⟶ℝ) |
45 | 7 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:𝑋⟶ℝ) |
46 | 42 | feq2d 6031 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ)) |
47 | 45, 46 | mpbid 222 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:∅⟶ℝ) |
48 | 14, 44, 47 | hoidmv0val 40797 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘∅)𝐵) = 0) |
49 | 40, 48 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = 0) |
50 | 37, 34, 49 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) |
51 | 36, 50 | eqled 10140 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) ≤ (𝐴(𝐿‘𝑋)𝐵)) |
52 | | eqid 2622 |
. . . . . 6
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
53 | | eqeq1 2626 |
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → (𝑛 = 1 ↔ 𝑗 = 1)) |
54 | 53 | ifbid 4108 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → if(𝑛 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉) = if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) |
55 | 54 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → (𝑘 ∈ 𝑋 ↦ if(𝑛 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) = (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) |
56 | 55 | cbvmptv 4750 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ if(𝑛 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) |
57 | 1, 5, 7, 2, 52, 56 | ovnhoilem1 40815 |
. . . . 5
⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) ≤ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
58 | 57 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) ≤ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
59 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ∈ Fin) |
60 | | neqne 2802 |
. . . . . . 7
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
61 | 60 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) |
62 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝐴:𝑋⟶ℝ) |
63 | 7 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝐵:𝑋⟶ℝ) |
64 | 14, 59, 61, 62, 63 | hoidmvn0val 40798 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
65 | 64 | eqcomd 2628 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (𝐴(𝐿‘𝑋)𝐵)) |
66 | 58, 65 | breqtrd 4679 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐼) ≤ (𝐴(𝐿‘𝑋)𝐵)) |
67 | 51, 66 | pm2.61dan 832 |
. 2
⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) ≤ (𝐴(𝐿‘𝑋)𝐵)) |
68 | 49, 35 | eqeltrd 2701 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) ∈ ℝ) |
69 | 50 | eqcomd 2628 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = ((voln*‘𝑋)‘𝐼)) |
70 | 68, 69 | eqled 10140 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) ≤ ((voln*‘𝑋)‘𝐼)) |
71 | | fveq1 6190 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → (𝑎‘𝑘) = (𝑐‘𝑘)) |
72 | 71 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑐 → ((𝑎‘𝑘)[,)(𝑏‘𝑘)) = ((𝑐‘𝑘)[,)(𝑏‘𝑘))) |
73 | 72 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑐 → (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘)))) |
74 | 73 | prodeq2ad 39824 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑐 → ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘)))) |
75 | 74 | ifeq2d 4105 |
. . . . . . . . 9
⊢ (𝑎 = 𝑐 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘))))) |
76 | | fveq1 6190 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑑 → (𝑏‘𝑘) = (𝑑‘𝑘)) |
77 | 76 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑑 → ((𝑐‘𝑘)[,)(𝑏‘𝑘)) = ((𝑐‘𝑘)[,)(𝑑‘𝑘))) |
78 | 77 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑑 → (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘))) = (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))) |
79 | 78 | prodeq2ad 39824 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑑 → ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))) |
80 | 79 | ifeq2d 4105 |
. . . . . . . . 9
⊢ (𝑏 = 𝑑 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘))))) |
81 | 75, 80 | cbvmpt2v 6735 |
. . . . . . . 8
⊢ (𝑎 ∈ (ℝ
↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑐 ∈ (ℝ ↑𝑚
𝑥), 𝑑 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘))))) |
82 | 81 | a1i 11 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑐 ∈ (ℝ ↑𝑚
𝑥), 𝑑 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))))) |
83 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (ℝ ↑𝑚
𝑥) = (ℝ
↑𝑚 𝑦)) |
84 | | eqeq1 2626 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅)) |
85 | | prodeq1 14639 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘))) = ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))) |
86 | 84, 85 | ifbieq2d 4111 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘))))) |
87 | 83, 83, 86 | mpt2eq123dv 6717 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑐 ∈ (ℝ ↑𝑚
𝑥), 𝑑 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘))))) = (𝑐 ∈ (ℝ ↑𝑚
𝑦), 𝑑 ∈ (ℝ ↑𝑚
𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))))) |
88 | 82, 87 | eqtrd 2656 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑐 ∈ (ℝ ↑𝑚
𝑦), 𝑑 ∈ (ℝ ↑𝑚
𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))))) |
89 | 88 | cbvmptv 4750 |
. . . . 5
⊢ (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ
↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑦), 𝑑 ∈ (ℝ ↑𝑚
𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))))) |
90 | 14, 89 | eqtri 2644 |
. . . 4
⊢ 𝐿 = (𝑦 ∈ Fin ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑦), 𝑑 ∈ (ℝ ↑𝑚
𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑐‘𝑘)[,)(𝑑‘𝑘)))))) |
91 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑤 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)))) ↔ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)))))) |
92 | 91 | anbi2d 740 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → ((𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑤 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))))) |
93 | 92 | rexbidv 3052 |
. . . . . 6
⊢ (𝑤 = 𝑧 → (∃ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑤 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ ∃ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))))) |
94 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ = 𝑖 ∧ 𝑗 ∈ ℕ) → ℎ = 𝑖) |
95 | 94 | fveq1d 6193 |
. . . . . . . . . . . . . 14
⊢ ((ℎ = 𝑖 ∧ 𝑗 ∈ ℕ) → (ℎ‘𝑗) = (𝑖‘𝑗)) |
96 | 95 | coeq2d 5284 |
. . . . . . . . . . . . 13
⊢ ((ℎ = 𝑖 ∧ 𝑗 ∈ ℕ) → ([,) ∘ (ℎ‘𝑗)) = ([,) ∘ (𝑖‘𝑗))) |
97 | 96 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ ((ℎ = 𝑖 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (ℎ‘𝑗))‘𝑘) = (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
98 | 97 | ixpeq2dv 7924 |
. . . . . . . . . . 11
⊢ ((ℎ = 𝑖 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
99 | 98 | iuneq2dv 4542 |
. . . . . . . . . 10
⊢ (ℎ = 𝑖 → ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
100 | 99 | sseq2d 3633 |
. . . . . . . . 9
⊢ (ℎ = 𝑖 → (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ↔ 𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
101 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋) → ℎ = 𝑖) |
102 | 101 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋) → (ℎ‘𝑗) = (𝑖‘𝑗)) |
103 | 102 | coeq2d 5284 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋) → ([,) ∘ (ℎ‘𝑗)) = ([,) ∘ (𝑖‘𝑗))) |
104 | 103 | fveq1d 6193 |
. . . . . . . . . . . . . 14
⊢ ((ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (ℎ‘𝑗))‘𝑘) = (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
105 | 104 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((ℎ = 𝑖 ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
106 | 105 | prodeq2dv 14653 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑖 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
107 | 106 | mpteq2dv 4745 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑖 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) |
108 | 107 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (ℎ = 𝑖 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
109 | 108 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (ℎ = 𝑖 → (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)))) ↔ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
110 | 100, 109 | anbi12d 747 |
. . . . . . . 8
⊢ (ℎ = 𝑖 → ((𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
111 | 110 | cbvrexv 3172 |
. . . . . . 7
⊢
(∃ℎ ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
112 | 111 | a1i 11 |
. . . . . 6
⊢ (𝑤 = 𝑧 → (∃ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
113 | 93, 112 | bitrd 268 |
. . . . 5
⊢ (𝑤 = 𝑧 → (∃ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑤 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
114 | 113 | cbvrabv 3199 |
. . . 4
⊢ {𝑤 ∈ ℝ*
∣ ∃ℎ ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ∧ 𝑤 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (ℎ‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
115 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋) → 𝑗 = 𝑛) |
116 | 115 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋) → (𝑖‘𝑗) = (𝑖‘𝑛)) |
117 | 116 | fveq1d 6193 |
. . . . . . . 8
⊢ ((𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋) → ((𝑖‘𝑗)‘𝑙) = ((𝑖‘𝑛)‘𝑙)) |
118 | 117 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋) → (1st ‘((𝑖‘𝑗)‘𝑙)) = (1st ‘((𝑖‘𝑛)‘𝑙))) |
119 | 118 | mpteq2dva 4744 |
. . . . . 6
⊢ (𝑗 = 𝑛 → (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙))) = (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) |
120 | 119 | cbvmptv 4750 |
. . . . 5
⊢ (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙)))) = (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) |
121 | 120 | mpteq2i 4741 |
. . . 4
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
↦ (𝑗 ∈ ℕ
↦ (𝑙 ∈ 𝑋 ↦ (1st
‘((𝑖‘𝑗)‘𝑙))))) = (𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
↦ (𝑛 ∈ ℕ
↦ (𝑙 ∈ 𝑋 ↦ (1st
‘((𝑖‘𝑛)‘𝑙))))) |
122 | 117 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝑗 = 𝑛 ∧ 𝑙 ∈ 𝑋) → (2nd ‘((𝑖‘𝑗)‘𝑙)) = (2nd ‘((𝑖‘𝑛)‘𝑙))) |
123 | 122 | mpteq2dva 4744 |
. . . . . 6
⊢ (𝑗 = 𝑛 → (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙))) = (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) |
124 | 123 | cbvmptv 4750 |
. . . . 5
⊢ (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙)))) = (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) |
125 | 124 | mpteq2i 4741 |
. . . 4
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
↦ (𝑗 ∈ ℕ
↦ (𝑙 ∈ 𝑋 ↦ (2nd
‘((𝑖‘𝑗)‘𝑙))))) = (𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
↦ (𝑛 ∈ ℕ
↦ (𝑙 ∈ 𝑋 ↦ (2nd
‘((𝑖‘𝑛)‘𝑙))))) |
126 | 59, 61, 62, 63, 2, 90, 114, 121, 125 | ovnhoilem2 40816 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) ≤ ((voln*‘𝑋)‘𝐼)) |
127 | 70, 126 | pm2.61dan 832 |
. 2
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ ((voln*‘𝑋)‘𝐼)) |
128 | 12, 16, 67, 127 | xrletrid 11986 |
1
⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) |