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 7923 |
. . . . . 6
⊢ {𝑍} ∈ Fin |
5 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑍} ∈ Fin) |
6 | | unfi 8112 |
. . . . 5
⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin) |
7 | 3, 5, 6 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin) |
8 | 2, 7 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
9 | | hoiprodp1.3 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
10 | | snidg 4153 |
. . . . . . 7
⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍}) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ {𝑍}) |
12 | | elun2 3743 |
. . . . . 6
⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
14 | 13, 2 | syl6eleqr 2699 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑋) |
15 | | ne0i 3880 |
. . . 4
⊢ (𝑍 ∈ 𝑋 → 𝑋 ≠ ∅) |
16 | 14, 15 | syl 17 |
. . 3
⊢ (𝜑 → 𝑋 ≠ ∅) |
17 | | hoiprodp1.a |
. . 3
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
18 | | hoiprodp1.b |
. . 3
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
19 | 1, 8, 16, 17, 18 | hoidmvn0val 39474 |
. 2
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
20 | 17 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
21 | 18 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
22 | | volicore 39471 |
. . . . 5
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
23 | 20, 21, 22 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
24 | 23 | recnd 9947 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ) |
25 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍)) |
26 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝑍 → (𝐵‘𝑘) = (𝐵‘𝑍)) |
27 | 25, 26 | oveq12d 6567 |
. . . . 5
⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍))) |
28 | 27 | fveq2d 6107 |
. . . 4
⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
29 | 28 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) |
30 | 8, 24, 14, 29 | fprodsplit1 38660 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
31 | 2 | difeq1i 3686 |
. . . . . . . 8
⊢ (𝑋 ∖ {𝑍}) = ((𝑌 ∪ {𝑍}) ∖ {𝑍}) |
32 | 31 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∖ {𝑍}) = ((𝑌 ∪ {𝑍}) ∖ {𝑍})) |
33 | | difun2 4000 |
. . . . . . . 8
⊢ ((𝑌 ∪ {𝑍}) ∖ {𝑍}) = (𝑌 ∖ {𝑍}) |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((𝑌 ∪ {𝑍}) ∖ {𝑍}) = (𝑌 ∖ {𝑍})) |
35 | | hoiprodp1.z |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) |
36 | | difsn 4269 |
. . . . . . . 8
⊢ (¬
𝑍 ∈ 𝑌 → (𝑌 ∖ {𝑍}) = 𝑌) |
37 | 35, 36 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑌 ∖ {𝑍}) = 𝑌) |
38 | 32, 34, 37 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∖ {𝑍}) = 𝑌) |
39 | 38 | prodeq1d 14490 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
40 | | hoiprodp1.g |
. . . . . . 7
⊢ 𝐺 = ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
41 | 40 | eqcomi 2619 |
. . . . . 6
⊢
∏𝑘 ∈
𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 𝐺 |
42 | 41 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 𝐺) |
43 | 39, 42 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 𝐺) |
44 | 43 | oveq2d 6565 |
. . 3
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) = ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · 𝐺)) |
45 | 17, 14 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ) |
46 | 18, 14 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ) |
47 | | volicore 39471 |
. . . . . 6
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ) |
48 | 45, 46, 47 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ) |
49 | 48 | recnd 9947 |
. . . 4
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ) |
50 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐴:𝑋⟶ℝ) |
51 | | ssun1 3738 |
. . . . . . . . . . . 12
⊢ 𝑌 ⊆ (𝑌 ∪ {𝑍}) |
52 | 51, 2 | sseqtr4i 3601 |
. . . . . . . . . . 11
⊢ 𝑌 ⊆ 𝑋 |
53 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑌) |
54 | 52, 53 | sseldi 3566 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑋) |
55 | 54 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝑘 ∈ 𝑋) |
56 | 50, 55 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (𝐴‘𝑘) ∈ ℝ) |
57 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐵:𝑋⟶ℝ) |
58 | 57, 55 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (𝐵‘𝑘) ∈ ℝ) |
59 | 56, 58, 22 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
60 | 3, 59 | fprodrecl 14522 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
61 | 40, 60 | syl5eqel 2692 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ ℝ) |
62 | 61 | recnd 9947 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ ℂ) |
63 | 49, 62 | mulcomd 9940 |
. . 3
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · 𝐺) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) |
64 | 44, 63 | eqtrd 2644 |
. 2
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) |
65 | 19, 30, 64 | 3eqtrd 2648 |
1
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) |