Proof of Theorem hoiprodp1
Step | Hyp | Ref
| Expression |
1 | | hoiprodp1.l |
. . 3
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
2 | | hoiprodp1.x |
. . . 4
⊢ 𝑋 = (𝑌 ∪ {𝑍}) |
3 | | hoiprodp1.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ Fin) |
4 | | snfi 8721 |
. . . . . 6
⊢ {𝑍} ∈ Fin |
5 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑍} ∈ Fin) |
6 | | unfi 8850 |
. . . . 5
⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin) |
7 | 3, 5, 6 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin) |
8 | 2, 7 | eqeltrid 2842 |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
9 | | hoiprodp1.3 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
10 | | snidg 4575 |
. . . . . . 7
⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍}) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ {𝑍}) |
12 | | elun2 4091 |
. . . . . 6
⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
14 | 13, 2 | eleqtrrdi 2849 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑋) |
15 | 14 | ne0d 4250 |
. . 3
⊢ (𝜑 → 𝑋 ≠ ∅) |
16 | | hoiprodp1.a |
. . 3
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
17 | | hoiprodp1.b |
. . 3
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
18 | 1, 8, 15, 16, 17 | hoidmvn0val 43800 |
. 2
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
19 | 16 | ffvelrnda 6904 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
20 | 17 | ffvelrnda 6904 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
21 | | volicore 43797 |
. . . . 5
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
22 | 19, 20, 21 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
23 | 22 | recnd 10861 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ) |
24 | | fveq2 6717 |
. . . . . 6
⊢ (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍)) |
25 | | fveq2 6717 |
. . . . . 6
⊢ (𝑘 = 𝑍 → (𝐵‘𝑘) = (𝐵‘𝑍)) |
26 | 24, 25 | oveq12d 7231 |
. . . . 5
⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍))) |
27 | 26 | fveq2d 6721 |
. . . 4
⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
28 | 27 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
29 | 8, 23, 14, 28 | fprodsplit1 42812 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
30 | 2 | difeq1i 4033 |
. . . . . . . 8
⊢ (𝑋 ∖ {𝑍}) = ((𝑌 ∪ {𝑍}) ∖ {𝑍}) |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∖ {𝑍}) = ((𝑌 ∪ {𝑍}) ∖ {𝑍})) |
32 | | difun2 4395 |
. . . . . . . 8
⊢ ((𝑌 ∪ {𝑍}) ∖ {𝑍}) = (𝑌 ∖ {𝑍}) |
33 | 32 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((𝑌 ∪ {𝑍}) ∖ {𝑍}) = (𝑌 ∖ {𝑍})) |
34 | | hoiprodp1.z |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) |
35 | | difsn 4711 |
. . . . . . . 8
⊢ (¬
𝑍 ∈ 𝑌 → (𝑌 ∖ {𝑍}) = 𝑌) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑌 ∖ {𝑍}) = 𝑌) |
37 | 31, 33, 36 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∖ {𝑍}) = 𝑌) |
38 | 37 | prodeq1d 15483 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
39 | | hoiprodp1.g |
. . . . . . 7
⊢ 𝐺 = ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
40 | 39 | eqcomi 2746 |
. . . . . 6
⊢
∏𝑘 ∈
𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 𝐺 |
41 | 40 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 𝐺) |
42 | 38, 41 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 𝐺) |
43 | 42 | oveq2d 7229 |
. . 3
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) = ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · 𝐺)) |
44 | 16, 14 | ffvelrnd 6905 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ) |
45 | 17, 14 | ffvelrnd 6905 |
. . . . . 6
⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ) |
46 | | volicore 43797 |
. . . . . 6
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ) |
47 | 44, 45, 46 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ) |
48 | 47 | recnd 10861 |
. . . 4
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ) |
49 | 16 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐴:𝑋⟶ℝ) |
50 | | ssun1 4086 |
. . . . . . . . . . . 12
⊢ 𝑌 ⊆ (𝑌 ∪ {𝑍}) |
51 | 50, 2 | sseqtrri 3938 |
. . . . . . . . . . 11
⊢ 𝑌 ⊆ 𝑋 |
52 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑌) |
53 | 51, 52 | sseldi 3899 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑋) |
54 | 53 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝑘 ∈ 𝑋) |
55 | 49, 54 | ffvelrnd 6905 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (𝐴‘𝑘) ∈ ℝ) |
56 | 17 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐵:𝑋⟶ℝ) |
57 | 56, 54 | ffvelrnd 6905 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (𝐵‘𝑘) ∈ ℝ) |
58 | 55, 57, 21 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
59 | 3, 58 | fprodrecl 15515 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
60 | 39, 59 | eqeltrid 2842 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ ℝ) |
61 | 60 | recnd 10861 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ ℂ) |
62 | 48, 61 | mulcomd 10854 |
. . 3
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · 𝐺) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) |
63 | 43, 62 | eqtrd 2777 |
. 2
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) |
64 | 18, 29, 63 | 3eqtrd 2781 |
1
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) |