Proof of Theorem hoidmvval
Step | Hyp | Ref
| Expression |
1 | | hoidmvval.l |
. . . 4
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))) |
3 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = 𝑋 → (ℝ ↑𝑚
𝑥) = (ℝ
↑𝑚 𝑋)) |
4 | | eqeq1 2614 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 = ∅ ↔ 𝑋 = ∅)) |
5 | | prodeq1 14478 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑘 ∈ 𝑋 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) |
6 | 4, 5 | ifbieq2d 4061 |
. . . . 5
⊢ (𝑥 = 𝑋 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) |
7 | 3, 3, 6 | mpt2eq123dv 6615 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑𝑚
𝑋), 𝑏 ∈ (ℝ ↑𝑚
𝑋) ↦ if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
8 | 7 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑𝑚
𝑋), 𝑏 ∈ (ℝ ↑𝑚
𝑋) ↦ if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
9 | | hoidmvval.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
10 | | ovex 6577 |
. . . . 5
⊢ (ℝ
↑𝑚 𝑋) ∈ V |
11 | 10, 10 | mpt2ex 7136 |
. . . 4
⊢ (𝑎 ∈ (ℝ
↑𝑚 𝑋), 𝑏 ∈ (ℝ ↑𝑚
𝑋) ↦ if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) ∈ V |
12 | 11 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (ℝ ↑𝑚
𝑋), 𝑏 ∈ (ℝ ↑𝑚
𝑋) ↦ if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) ∈ V) |
13 | 2, 8, 9, 12 | fvmptd 6197 |
. 2
⊢ (𝜑 → (𝐿‘𝑋) = (𝑎 ∈ (ℝ ↑𝑚
𝑋), 𝑏 ∈ (ℝ ↑𝑚
𝑋) ↦ if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
14 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎‘𝑘) = (𝐴‘𝑘)) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎‘𝑘) = (𝐴‘𝑘)) |
16 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (𝑏‘𝑘) = (𝐵‘𝑘)) |
17 | 16 | adantl 481 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑏‘𝑘) = (𝐵‘𝑘)) |
18 | 15, 17 | oveq12d 6567 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑎‘𝑘)[,)(𝑏‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
19 | 18 | fveq2d 6107 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
20 | 19 | prodeq2ad 38659 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ∏𝑘 ∈ 𝑋 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
21 | 20 | ifeq2d 4055 |
. . 3
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
22 | 21 | adantl 481 |
. 2
⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) → if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
23 | | hoidmvval.a |
. . 3
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
24 | | reex 9906 |
. . . . 5
⊢ ℝ
∈ V |
25 | 24 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ∈
V) |
26 | | elmapg 7757 |
. . . 4
⊢ ((ℝ
∈ V ∧ 𝑋 ∈
Fin) → (𝐴 ∈
(ℝ ↑𝑚 𝑋) ↔ 𝐴:𝑋⟶ℝ)) |
27 | 25, 9, 26 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐴 ∈ (ℝ ↑𝑚
𝑋) ↔ 𝐴:𝑋⟶ℝ)) |
28 | 23, 27 | mpbird 246 |
. 2
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑𝑚
𝑋)) |
29 | | hoidmvval.b |
. . 3
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
30 | | elmapg 7757 |
. . . 4
⊢ ((ℝ
∈ V ∧ 𝑋 ∈
Fin) → (𝐵 ∈
(ℝ ↑𝑚 𝑋) ↔ 𝐵:𝑋⟶ℝ)) |
31 | 25, 9, 30 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐵 ∈ (ℝ ↑𝑚
𝑋) ↔ 𝐵:𝑋⟶ℝ)) |
32 | 29, 31 | mpbird 246 |
. 2
⊢ (𝜑 → 𝐵 ∈ (ℝ ↑𝑚
𝑋)) |
33 | | c0ex 9913 |
. . . 4
⊢ 0 ∈
V |
34 | | prodex 14476 |
. . . 4
⊢
∏𝑘 ∈
𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ V |
35 | 33, 34 | ifex 4106 |
. . 3
⊢ if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) ∈ V |
36 | 35 | a1i 11 |
. 2
⊢ (𝜑 → if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) ∈ V) |
37 | 13, 22, 28, 32, 36 | ovmpt2d 6686 |
1
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |