Proof of Theorem ovnhoilem1
Step | Hyp | Ref
| Expression |
1 | | ovnhoilem1.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | ovnhoilem1.c |
. . . . 5
⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
4 | | nfv 1843 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
5 | | ovnhoilem1.a |
. . . . . 6
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
6 | 5 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
7 | | ovnhoilem1.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 | | ovnhoilem1.m |
. . 3
⊢ 𝑀 = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
13 | 1, 11, 12 | ovnval2 40759 |
. 2
⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) = if(𝑋 = ∅, 0, inf(𝑀, ℝ*, <
))) |
14 | | iftrue 4092 |
. . . . 5
⊢ (𝑋 = ∅ → if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < )) =
0) |
15 | 14 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < )) =
0) |
16 | | 0xr 10086 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
17 | 16 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ*) |
18 | | pnfxr 10092 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
19 | 18 | a1i 11 |
. . . . . 6
⊢ (𝜑 → +∞ ∈
ℝ*) |
20 | 4, 1, 6, 8 | hoiprodcl3 40794 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ (0[,)+∞)) |
21 | | icogelb 12225 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ (0[,)+∞)) → 0 ≤
∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
22 | 17, 19, 20, 21 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → 0 ≤ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
23 | 22 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 ≤ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
24 | 15, 23 | eqbrtrd 4675 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < )) ≤
∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
25 | | iffalse 4095 |
. . . . 5
⊢ (¬
𝑋 = ∅ → if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < )) =
inf(𝑀, ℝ*,
< )) |
26 | 25 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < )) = inf(𝑀, ℝ*, <
)) |
27 | | ssrab2 3687 |
. . . . . . 7
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆
ℝ* |
28 | 12, 27 | eqsstri 3635 |
. . . . . 6
⊢ 𝑀 ⊆
ℝ* |
29 | 28 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑀 ⊆
ℝ*) |
30 | | icossxr 12258 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ* |
31 | 30, 20 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈
ℝ*) |
32 | 31 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈
ℝ*) |
33 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → 〈(𝐴‘𝑘), (𝐵‘𝑘)〉 ∈ (ℝ ×
ℝ)) |
34 | 6, 8, 33 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 〈(𝐴‘𝑘), (𝐵‘𝑘)〉 ∈ (ℝ ×
ℝ)) |
35 | | 0re 10040 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
36 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ ∧ 0 ∈ ℝ) → 〈0, 0〉 ∈ (ℝ
× ℝ)) |
37 | 35, 35, 36 | mp2an 708 |
. . . . . . . . . . . . . . . . 17
⊢ 〈0,
0〉 ∈ (ℝ × ℝ) |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 〈0, 0〉 ∈ (ℝ
× ℝ)) |
39 | 34, 38 | ifcld 4131 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉) ∈ (ℝ
× ℝ)) |
40 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) = (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) |
41 | 39, 40 | fmptd 6385 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)):𝑋⟶(ℝ ×
ℝ)) |
42 | | reex 10027 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
∈ V |
43 | 42, 42 | xpex 6962 |
. . . . . . . . . . . . . . . 16
⊢ (ℝ
× ℝ) ∈ V |
44 | 1, 43 | jctil 560 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℝ × ℝ)
∈ V ∧ 𝑋 ∈
Fin)) |
45 | | elmapg 7870 |
. . . . . . . . . . . . . . 15
⊢
(((ℝ × ℝ) ∈ V ∧ 𝑋 ∈ Fin) → ((𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) ∈ ((ℝ
× ℝ) ↑𝑚 𝑋) ↔ (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)):𝑋⟶(ℝ ×
ℝ))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) ∈ ((ℝ
× ℝ) ↑𝑚 𝑋) ↔ (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)):𝑋⟶(ℝ ×
ℝ))) |
47 | 41, 46 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) ∈ ((ℝ
× ℝ) ↑𝑚 𝑋)) |
48 | 47 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) ∈ ((ℝ
× ℝ) ↑𝑚 𝑋)) |
49 | | ovnhoilem1.h |
. . . . . . . . . . . 12
⊢ 𝐻 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) |
50 | 48, 49 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻:ℕ⟶((ℝ × ℝ)
↑𝑚 𝑋)) |
51 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ ((ℝ
× ℝ) ↑𝑚 𝑋) ∈ V |
52 | | nnex 11026 |
. . . . . . . . . . . 12
⊢ ℕ
∈ V |
53 | 51, 52 | elmap 7886 |
. . . . . . . . . . 11
⊢ (𝐻 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ↔
𝐻:ℕ⟶((ℝ
× ℝ) ↑𝑚 𝑋)) |
54 | 50, 53 | sylibr 224 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
55 | 54 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝐻 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
56 | | eqidd 2623 |
. . . . . . . . . . . . 13
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
57 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ 𝑋 ↦ 〈(𝐴‘𝑘), (𝐵‘𝑘)〉) = (𝑘 ∈ 𝑋 ↦ 〈(𝐴‘𝑘), (𝐵‘𝑘)〉) |
58 | 34, 57 | fmptd 6385 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ 〈(𝐴‘𝑘), (𝐵‘𝑘)〉):𝑋⟶(ℝ ×
ℝ)) |
59 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐻 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0,
0〉)))) |
60 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 1 → if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉) = 〈(𝐴‘𝑘), (𝐵‘𝑘)〉) |
61 | 60 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 1 → (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) = (𝑘 ∈ 𝑋 ↦ 〈(𝐴‘𝑘), (𝐵‘𝑘)〉)) |
62 | 61 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 = 1) → (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) = (𝑘 ∈ 𝑋 ↦ 〈(𝐴‘𝑘), (𝐵‘𝑘)〉)) |
63 | | 1nn 11031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℕ |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
ℕ) |
65 | | mptexg 6484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑋 ∈ Fin → (𝑘 ∈ 𝑋 ↦ 〈(𝐴‘𝑘), (𝐵‘𝑘)〉) ∈ V) |
66 | 1, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ 〈(𝐴‘𝑘), (𝐵‘𝑘)〉) ∈ V) |
67 | 59, 62, 64, 66 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐻‘1) = (𝑘 ∈ 𝑋 ↦ 〈(𝐴‘𝑘), (𝐵‘𝑘)〉)) |
68 | 67 | feq1d 6030 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐻‘1):𝑋⟶(ℝ × ℝ) ↔
(𝑘 ∈ 𝑋 ↦ 〈(𝐴‘𝑘), (𝐵‘𝑘)〉):𝑋⟶(ℝ ×
ℝ))) |
69 | 58, 68 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐻‘1):𝑋⟶(ℝ ×
ℝ)) |
70 | 69 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐻‘1):𝑋⟶(ℝ ×
ℝ)) |
71 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
72 | 70, 71 | fvovco 39381 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝐻‘1))‘𝑘) = ((1st ‘((𝐻‘1)‘𝑘))[,)(2nd
‘((𝐻‘1)‘𝑘)))) |
73 | 34 | elexd 3214 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 〈(𝐴‘𝑘), (𝐵‘𝑘)〉 ∈ V) |
74 | 67, 73 | fvmpt2d 6293 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐻‘1)‘𝑘) = 〈(𝐴‘𝑘), (𝐵‘𝑘)〉) |
75 | 74 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1st ‘((𝐻‘1)‘𝑘)) = (1st
‘〈(𝐴‘𝑘), (𝐵‘𝑘)〉)) |
76 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴‘𝑘) ∈ V |
77 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵‘𝑘) ∈ V |
78 | 76, 77 | op1st 7176 |
. . . . . . . . . . . . . . . . . 18
⊢
(1st ‘〈(𝐴‘𝑘), (𝐵‘𝑘)〉) = (𝐴‘𝑘) |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1st ‘〈(𝐴‘𝑘), (𝐵‘𝑘)〉) = (𝐴‘𝑘)) |
80 | 75, 79 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1st ‘((𝐻‘1)‘𝑘)) = (𝐴‘𝑘)) |
81 | 74 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (2nd ‘((𝐻‘1)‘𝑘)) = (2nd
‘〈(𝐴‘𝑘), (𝐵‘𝑘)〉)) |
82 | 76, 77 | op2nd 7177 |
. . . . . . . . . . . . . . . . . 18
⊢
(2nd ‘〈(𝐴‘𝑘), (𝐵‘𝑘)〉) = (𝐵‘𝑘) |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (2nd ‘〈(𝐴‘𝑘), (𝐵‘𝑘)〉) = (𝐵‘𝑘)) |
84 | 81, 83 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (2nd ‘((𝐻‘1)‘𝑘)) = (𝐵‘𝑘)) |
85 | 80, 84 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((1st ‘((𝐻‘1)‘𝑘))[,)(2nd
‘((𝐻‘1)‘𝑘))) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
86 | 72, 85 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝐻‘1))‘𝑘) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
87 | 86 | ixpeq2dva 7923 |
. . . . . . . . . . . . 13
⊢ (𝜑 → X𝑘 ∈
𝑋 (([,) ∘ (𝐻‘1))‘𝑘) = X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
88 | 56, 3, 87 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 = X𝑘 ∈ 𝑋 (([,) ∘ (𝐻‘1))‘𝑘)) |
89 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 1 → (𝐻‘𝑗) = (𝐻‘1)) |
90 | 89 | coeq2d 5284 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 1 → ([,) ∘ (𝐻‘𝑗)) = ([,) ∘ (𝐻‘1))) |
91 | 90 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 1 → (([,) ∘ (𝐻‘𝑗))‘𝑘) = (([,) ∘ (𝐻‘1))‘𝑘)) |
92 | 91 | ixpeq2dv 7924 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 1 → X𝑘 ∈
𝑋 (([,) ∘ (𝐻‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ (𝐻‘1))‘𝑘)) |
93 | 92 | ssiun2s 4564 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℕ → X𝑘 ∈ 𝑋 (([,) ∘ (𝐻‘1))‘𝑘) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐻‘𝑗))‘𝑘)) |
94 | 63, 93 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ X𝑘 ∈
𝑋 (([,) ∘ (𝐻‘1))‘𝑘) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝐻‘𝑗))‘𝑘) |
95 | 88, 94 | syl6eqss 3655 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐻‘𝑗))‘𝑘)) |
96 | 95 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐻‘𝑗))‘𝑘)) |
97 | 86 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ (𝐻‘1))‘𝑘)) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
98 | 97 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘(([,) ∘ (𝐻‘1))‘𝑘))) |
99 | 98 | prodeq2dv 14653 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘1))‘𝑘))) |
100 | 99 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘1))‘𝑘))) |
101 | | 1red 10055 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ) |
102 | | icossicc 12260 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
103 | 4, 1, 69 | hoiprodcl 40761 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘1))‘𝑘)) ∈ (0[,)+∞)) |
104 | 102, 103 | sseldi 3601 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘1))‘𝑘)) ∈ (0[,]+∞)) |
105 | 91 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 1 → (vol‘(([,)
∘ (𝐻‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐻‘1))‘𝑘))) |
106 | 105 | prodeq2ad 39824 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 1 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘1))‘𝑘))) |
107 | 101, 104,
106 | sge0snmpt 40600 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ {1} ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)))) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘1))‘𝑘))) |
108 | 107 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘1))‘𝑘)) =
(Σ^‘(𝑗 ∈ {1} ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘))))) |
109 | 108 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘1))‘𝑘)) =
(Σ^‘(𝑗 ∈ {1} ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘))))) |
110 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗(𝜑 ∧ ¬ 𝑋 = ∅) |
111 | 52 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ℕ ∈
V) |
112 | | snssi 4339 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℕ → {1} ⊆ ℕ) |
113 | 63, 112 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ {1}
⊆ ℕ |
114 | 113 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → {1} ⊆
ℕ) |
115 | | nfv 1843 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ {1}) |
116 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ {1}) → 𝑋 ∈ Fin) |
117 | | simpl 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ {1}) → 𝜑) |
118 | | elsni 4194 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ {1} → 𝑗 = 1) |
119 | 118 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ {1}) → 𝑗 = 1) |
120 | 69 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 = 1) → (𝐻‘1):𝑋⟶(ℝ ×
ℝ)) |
121 | 89 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 = 1) → (𝐻‘𝑗) = (𝐻‘1)) |
122 | 121 | feq1d 6030 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 = 1) → ((𝐻‘𝑗):𝑋⟶(ℝ × ℝ) ↔
(𝐻‘1):𝑋⟶(ℝ ×
ℝ))) |
123 | 120, 122 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 = 1) → (𝐻‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
124 | 117, 119,
123 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ {1}) → (𝐻‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
125 | 124 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ {1}) → (𝐻‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
126 | 115, 116,
125 | hoiprodcl 40761 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ {1}) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)) ∈ (0[,)+∞)) |
127 | 102, 126 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ {1}) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)) ∈ (0[,]+∞)) |
128 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ 𝑋 ↦ 〈0, 0〉) = (𝑘 ∈ 𝑋 ↦ 〈0, 0〉) |
129 | 38, 128 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ 〈0, 0〉):𝑋⟶(ℝ ×
ℝ)) |
130 | 129 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) → (𝑘 ∈ 𝑋 ↦ 〈0, 0〉):𝑋⟶(ℝ ×
ℝ)) |
131 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) → 𝜑) |
132 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 ∈ (ℕ ∖ {1})
→ 𝑗 ∈
ℕ) |
133 | 132 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) → 𝑗 ∈
ℕ) |
134 | 48 | elexd 3214 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) ∈
V) |
135 | 59, 134 | fvmpt2d 6293 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑗) = (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) |
136 | 131, 133,
135 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) → (𝐻‘𝑗) = (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) |
137 | | eldifsni 4320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 ∈ (ℕ ∖ {1})
→ 𝑗 ≠
1) |
138 | 137 | neneqd 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 ∈ (ℕ ∖ {1})
→ ¬ 𝑗 =
1) |
139 | 138 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 ∈ (ℕ ∖ {1})
→ if(𝑗 = 1,
〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉) = 〈0,
0〉) |
140 | 139 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ (ℕ ∖ {1})
→ (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) = (𝑘 ∈ 𝑋 ↦ 〈0, 0〉)) |
141 | 140 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) → (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) = (𝑘 ∈ 𝑋 ↦ 〈0, 0〉)) |
142 | 136, 141 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) → (𝐻‘𝑗) = (𝑘 ∈ 𝑋 ↦ 〈0, 0〉)) |
143 | 142 | feq1d 6030 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) → ((𝐻‘𝑗):𝑋⟶(ℝ × ℝ) ↔
(𝑘 ∈ 𝑋 ↦ 〈0, 0〉):𝑋⟶(ℝ ×
ℝ))) |
144 | 130, 143 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) → (𝐻‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
145 | 144 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (𝐻‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
146 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
147 | 145, 146 | fvovco 39381 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝐻‘𝑗))‘𝑘) = ((1st ‘((𝐻‘𝑗)‘𝑘))[,)(2nd ‘((𝐻‘𝑗)‘𝑘)))) |
148 | 37 | elexi 3213 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 〈0,
0〉 ∈ V |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → 〈0, 0〉 ∈
V) |
150 | 142, 149 | fvmpt2d 6293 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → ((𝐻‘𝑗)‘𝑘) = 〈0, 0〉) |
151 | 150 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (1st ‘((𝐻‘𝑗)‘𝑘)) = (1st ‘〈0,
0〉)) |
152 | 16 | elexi 3213 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
V |
153 | 152, 152 | op1st 7176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1st ‘〈0, 0〉) = 0 |
154 | 153 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (1st ‘〈0,
0〉) = 0) |
155 | 151, 154 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (1st ‘((𝐻‘𝑗)‘𝑘)) = 0) |
156 | 150 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (2nd ‘((𝐻‘𝑗)‘𝑘)) = (2nd ‘〈0,
0〉)) |
157 | 152, 152 | op2nd 7177 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(2nd ‘〈0, 0〉) = 0 |
158 | 157 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (2nd ‘〈0,
0〉) = 0) |
159 | 156, 158 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (2nd ‘((𝐻‘𝑗)‘𝑘)) = 0) |
160 | 155, 159 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → ((1st ‘((𝐻‘𝑗)‘𝑘))[,)(2nd ‘((𝐻‘𝑗)‘𝑘))) = (0[,)0)) |
161 | | 0le0 11110 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≤
0 |
162 | | ico0 12221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ* ∧ 0 ∈ ℝ*) → ((0[,)0)
= ∅ ↔ 0 ≤ 0)) |
163 | 16, 16, 162 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0[,)0)
= ∅ ↔ 0 ≤ 0) |
164 | 161, 163 | mpbir 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0[,)0) =
∅ |
165 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (0[,)0) = ∅) |
166 | 147, 160,
165 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝐻‘𝑗))‘𝑘) = ∅) |
167 | 166 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)) = (vol‘∅)) |
168 | | vol0 40175 |
. . . . . . . . . . . . . . . . 17
⊢
(vol‘∅) = 0 |
169 | 168 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (vol‘∅) =
0) |
170 | 167, 169 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)) = 0) |
171 | 170 | prodeq2dv 14653 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℕ ∖ {1})) →
∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 0) |
172 | 171 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ (ℕ ∖ {1})) →
∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 0) |
173 | | 0cnd 10033 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℂ) |
174 | | fprodconst 14708 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ Fin ∧ 0 ∈
ℂ) → ∏𝑘
∈ 𝑋 0 =
(0↑(#‘𝑋))) |
175 | 1, 173, 174 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 0 = (0↑(#‘𝑋))) |
176 | 175 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ (ℕ ∖ {1})) →
∏𝑘 ∈ 𝑋 0 = (0↑(#‘𝑋))) |
177 | | neqne 2802 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
178 | 177 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) |
179 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ∈ Fin) |
180 | | hashnncl 13157 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ Fin →
((#‘𝑋) ∈ ℕ
↔ 𝑋 ≠
∅)) |
181 | 179, 180 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
182 | 178, 181 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → (#‘𝑋) ∈
ℕ) |
183 | | 0exp 12895 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑋) ∈
ℕ → (0↑(#‘𝑋)) = 0) |
184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → (0↑(#‘𝑋)) = 0) |
185 | 184 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ (ℕ ∖ {1})) →
(0↑(#‘𝑋)) =
0) |
186 | 172, 176,
185 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑗 ∈ (ℕ ∖ {1})) →
∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)) = 0) |
187 | 110, 111,
114, 127, 186 | sge0ss 40629 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) →
(Σ^‘(𝑗 ∈ {1} ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘))))) |
188 | 100, 109,
187 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘))))) |
189 | 96, 188 | jca 554 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐻‘𝑗))‘𝑘) ∧ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)))))) |
190 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘𝑖 |
191 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘ℕ |
192 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘(𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉)) |
193 | 191, 192 | nfmpt 4746 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) |
194 | 49, 193 | nfcxfr 2762 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘𝐻 |
195 | 190, 194 | nfeq 2776 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘 𝑖 = 𝐻 |
196 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝐻 → (𝑖‘𝑗) = (𝐻‘𝑗)) |
197 | 196 | coeq2d 5284 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝐻 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐻‘𝑗))) |
198 | 197 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝐻 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐻‘𝑗))‘𝑘)) |
199 | 198 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = 𝐻 ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐻‘𝑗))‘𝑘)) |
200 | 195, 199 | ixpeq2d 39237 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝐻 → X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ (𝐻‘𝑗))‘𝑘)) |
201 | 200 | iuneq2d 4547 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐻 → ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐻‘𝑗))‘𝑘)) |
202 | 201 | sseq2d 3633 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐻 → (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ 𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐻‘𝑗))‘𝑘))) |
203 | 198 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝐻 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘))) |
204 | 203 | a1d 25 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝐻 → (𝑘 ∈ 𝑋 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)))) |
205 | 195, 204 | ralrimi 2957 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝐻 → ∀𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘))) |
206 | 205 | prodeq2d 14652 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝐻 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘))) |
207 | 206 | mpteq2dv 4745 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝐻 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)))) |
208 | 207 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐻 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘))))) |
209 | 208 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐻 → (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)))))) |
210 | 202, 209 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐻 → ((𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐻‘𝑗))‘𝑘) ∧ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘))))))) |
211 | 210 | rspcev 3309 |
. . . . . . . . 9
⊢ ((𝐻 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝐻‘𝑗))‘𝑘) ∧ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐻‘𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
212 | 55, 189, 211 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
213 | 32, 212 | jca 554 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
214 | | eqeq1 2626 |
. . . . . . . . . 10
⊢ (𝑧 = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) → (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
215 | 214 | anbi2d 740 |
. . . . . . . . 9
⊢ (𝑧 = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) → ((𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
216 | 215 | rexbidv 3052 |
. . . . . . . 8
⊢ (𝑧 = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) → (∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
217 | 216 | elrab 3363 |
. . . . . . 7
⊢
(∏𝑘 ∈
𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ↔ (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
218 | 213, 217 | sylibr 224 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
219 | 12 | eqcomi 2631 |
. . . . . . 7
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = 𝑀 |
220 | 219 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = 𝑀) |
221 | 218, 220 | eleqtrd 2703 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ 𝑀) |
222 | | infxrlb 12164 |
. . . . 5
⊢ ((𝑀 ⊆ ℝ*
∧ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ 𝑀) → inf(𝑀, ℝ*, < ) ≤
∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
223 | 29, 221, 222 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → inf(𝑀, ℝ*, < ) ≤
∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
224 | 26, 223 | eqbrtrd 4675 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < )) ≤
∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
225 | 24, 224 | pm2.61dan 832 |
. 2
⊢ (𝜑 → if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < )) ≤
∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
226 | 13, 225 | eqbrtrd 4675 |
1
⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) ≤ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |