Proof of Theorem hoidmvval0
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. 2
⊢ (𝜑 → 𝜑) |
2 | | hoidmvval0.j |
. . 3
⊢ (𝜑 → ∃𝑗 ∈ 𝑋 (𝐵‘𝑗) ≤ (𝐴‘𝑗)) |
3 | | fveq2 6768 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝐵‘𝑘) = (𝐵‘𝑗)) |
4 | | fveq2 6768 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗)) |
5 | 3, 4 | breq12d 5088 |
. . . . 5
⊢ (𝑘 = 𝑗 → ((𝐵‘𝑘) ≤ (𝐴‘𝑘) ↔ (𝐵‘𝑗) ≤ (𝐴‘𝑗))) |
6 | 5 | cbvrexvw 3383 |
. . . 4
⊢
(∃𝑘 ∈
𝑋 (𝐵‘𝑘) ≤ (𝐴‘𝑘) ↔ ∃𝑗 ∈ 𝑋 (𝐵‘𝑗) ≤ (𝐴‘𝑗)) |
7 | | rexn0 4443 |
. . . 4
⊢
(∃𝑘 ∈
𝑋 (𝐵‘𝑘) ≤ (𝐴‘𝑘) → 𝑋 ≠ ∅) |
8 | 6, 7 | sylbir 234 |
. . 3
⊢
(∃𝑗 ∈
𝑋 (𝐵‘𝑗) ≤ (𝐴‘𝑗) → 𝑋 ≠ ∅) |
9 | 2, 8 | syl 17 |
. 2
⊢ (𝜑 → 𝑋 ≠ ∅) |
10 | | hoidmvval0.l |
. . . 4
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
11 | | hoidmvval0.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
12 | 11 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ∈ Fin) |
13 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ≠ ∅) |
14 | | hoidmvval0.a |
. . . . 5
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
15 | 14 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐴:𝑋⟶ℝ) |
16 | | hoidmvval0.b |
. . . . 5
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
17 | 16 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐵:𝑋⟶ℝ) |
18 | 10, 12, 13, 15, 17 | hoidmvn0val 44082 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
19 | 2 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑗 ∈ 𝑋 (𝐵‘𝑗) ≤ (𝐴‘𝑗)) |
20 | | hoidmvval0.p |
. . . . . 6
⊢
Ⅎ𝑗𝜑 |
21 | | nfv 1917 |
. . . . . 6
⊢
Ⅎ𝑗 𝑋 ≠ ∅ |
22 | 20, 21 | nfan 1902 |
. . . . 5
⊢
Ⅎ𝑗(𝜑 ∧ 𝑋 ≠ ∅) |
23 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑗∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0 |
24 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) |
25 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑘(vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) |
26 | 11 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → 𝑋 ∈ Fin) |
27 | 14 | ffvelrnda 6955 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
28 | 16 | ffvelrnda 6955 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
29 | | volicore 44079 |
. . . . . . . . . . 11
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
30 | 27, 28, 29 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
31 | 30 | recnd 10992 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ) |
32 | 31 | 3ad2antl1 1184 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ) |
33 | 4, 3 | oveq12d 7287 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑗)[,)(𝐵‘𝑗))) |
34 | 33 | fveq2d 6772 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗)))) |
35 | | simp2 1136 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → 𝑗 ∈ 𝑋) |
36 | 14 | ffvelrnda 6955 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐴‘𝑗) ∈ ℝ) |
37 | 36 | 3adant3 1131 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → (𝐴‘𝑗) ∈ ℝ) |
38 | 16 | ffvelrnda 6955 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐵‘𝑗) ∈ ℝ) |
39 | 38 | 3adant3 1131 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → (𝐵‘𝑗) ∈ ℝ) |
40 | | volico 43484 |
. . . . . . . . . 10
⊢ (((𝐴‘𝑗) ∈ ℝ ∧ (𝐵‘𝑗) ∈ ℝ) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) < (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0)) |
41 | 37, 39, 40 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) < (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0)) |
42 | | simp3 1137 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → (𝐵‘𝑗) ≤ (𝐴‘𝑗)) |
43 | 39, 37 | lenltd 11110 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → ((𝐵‘𝑗) ≤ (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) < (𝐵‘𝑗))) |
44 | 42, 43 | mpbid 231 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → ¬ (𝐴‘𝑗) < (𝐵‘𝑗)) |
45 | 44 | iffalsed 4472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → if((𝐴‘𝑗) < (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0) = 0) |
46 | 41, 45 | eqtrd 2778 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0) |
47 | 24, 25, 26, 32, 34, 35, 46 | fprod0 43097 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) |
48 | 47 | 3adant1r 1176 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) |
49 | 48 | 3exp 1118 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝑗 ∈ 𝑋 → ((𝐵‘𝑗) ≤ (𝐴‘𝑗) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0))) |
50 | 22, 23, 49 | rexlimd 3249 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑗 ∈ 𝑋 (𝐵‘𝑗) ≤ (𝐴‘𝑗) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0)) |
51 | 19, 50 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) |
52 | | eqidd 2739 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 0 =
0) |
53 | 18, 51, 52 | 3eqtrd 2782 |
. 2
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝐴(𝐿‘𝑋)𝐵) = 0) |
54 | 1, 9, 53 | syl2anc 584 |
1
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = 0) |