Proof of Theorem hoiprodp1
Step | Hyp | Ref
| Expression |
1 | | hoiprodp1.l |
. . 3
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
2 | | hoiprodp1.x |
. . . 4
⊢ 𝑋 = (𝑌 ∪ {𝑍}) |
3 | | hoiprodp1.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ Fin) |
4 | | snfi 8038 |
. . . . . 6
⊢ {𝑍} ∈ Fin |
5 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑍} ∈ Fin) |
6 | | unfi 8227 |
. . . . 5
⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin) |
7 | 3, 5, 6 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin) |
8 | 2, 7 | syl5eqel 2705 |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
9 | | hoiprodp1.3 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
10 | | snidg 4206 |
. . . . . . 7
⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍}) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ {𝑍}) |
12 | | elun2 3781 |
. . . . . 6
⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
14 | 13, 2 | syl6eleqr 2712 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑋) |
15 | | ne0i 3921 |
. . . 4
⊢ (𝑍 ∈ 𝑋 → 𝑋 ≠ ∅) |
16 | 14, 15 | syl 17 |
. . 3
⊢ (𝜑 → 𝑋 ≠ ∅) |
17 | | hoiprodp1.a |
. . 3
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
18 | | hoiprodp1.b |
. . 3
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
19 | 1, 8, 16, 17, 18 | hoidmvn0val 40798 |
. 2
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
20 | 17 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
21 | 18 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
22 | | volicore 40795 |
. . . . 5
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
23 | 20, 21, 22 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
24 | 23 | recnd 10068 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ) |
25 | | fveq2 6191 |
. . . . . 6
⊢ (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍)) |
26 | | fveq2 6191 |
. . . . . 6
⊢ (𝑘 = 𝑍 → (𝐵‘𝑘) = (𝐵‘𝑍)) |
27 | 25, 26 | oveq12d 6668 |
. . . . 5
⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍))) |
28 | 27 | fveq2d 6195 |
. . . 4
⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
29 | 28 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
30 | 8, 24, 14, 29 | fprodsplit1 39825 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
31 | 2 | difeq1i 3724 |
. . . . . . . 8
⊢ (𝑋 ∖ {𝑍}) = ((𝑌 ∪ {𝑍}) ∖ {𝑍}) |
32 | 31 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∖ {𝑍}) = ((𝑌 ∪ {𝑍}) ∖ {𝑍})) |
33 | | difun2 4048 |
. . . . . . . 8
⊢ ((𝑌 ∪ {𝑍}) ∖ {𝑍}) = (𝑌 ∖ {𝑍}) |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((𝑌 ∪ {𝑍}) ∖ {𝑍}) = (𝑌 ∖ {𝑍})) |
35 | | hoiprodp1.z |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) |
36 | | difsn 4328 |
. . . . . . . 8
⊢ (¬
𝑍 ∈ 𝑌 → (𝑌 ∖ {𝑍}) = 𝑌) |
37 | 35, 36 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑌 ∖ {𝑍}) = 𝑌) |
38 | 32, 34, 37 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∖ {𝑍}) = 𝑌) |
39 | 38 | prodeq1d 14651 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
40 | | hoiprodp1.g |
. . . . . . 7
⊢ 𝐺 = ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
41 | 40 | eqcomi 2631 |
. . . . . 6
⊢
∏𝑘 ∈
𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 𝐺 |
42 | 41 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 𝐺) |
43 | 39, 42 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 𝐺) |
44 | 43 | oveq2d 6666 |
. . 3
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) = ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · 𝐺)) |
45 | 17, 14 | ffvelrnd 6360 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ) |
46 | 18, 14 | ffvelrnd 6360 |
. . . . . 6
⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ) |
47 | | volicore 40795 |
. . . . . 6
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ) |
48 | 45, 46, 47 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ) |
49 | 48 | recnd 10068 |
. . . 4
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ) |
50 | 17 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐴:𝑋⟶ℝ) |
51 | | ssun1 3776 |
. . . . . . . . . . . 12
⊢ 𝑌 ⊆ (𝑌 ∪ {𝑍}) |
52 | 51, 2 | sseqtr4i 3638 |
. . . . . . . . . . 11
⊢ 𝑌 ⊆ 𝑋 |
53 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑌) |
54 | 52, 53 | sseldi 3601 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑋) |
55 | 54 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝑘 ∈ 𝑋) |
56 | 50, 55 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (𝐴‘𝑘) ∈ ℝ) |
57 | 18 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐵:𝑋⟶ℝ) |
58 | 57, 55 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (𝐵‘𝑘) ∈ ℝ) |
59 | 56, 58, 22 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
60 | 3, 59 | fprodrecl 14683 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
61 | 40, 60 | syl5eqel 2705 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ ℝ) |
62 | 61 | recnd 10068 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ ℂ) |
63 | 49, 62 | mulcomd 10061 |
. . 3
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · 𝐺) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) |
64 | 44, 63 | eqtrd 2656 |
. 2
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) |
65 | 19, 30, 64 | 3eqtrd 2660 |
1
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) |