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 9083 | . . . . . 6
⊢ {𝑍} ∈ Fin | 
| 5 | 4 | a1i 11 | . . . . 5
⊢ (𝜑 → {𝑍} ∈ Fin) | 
| 6 |  | unfi 9211 | . . . . 5
⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin) | 
| 7 | 3, 5, 6 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin) | 
| 8 | 2, 7 | eqeltrid 2845 | . . 3
⊢ (𝜑 → 𝑋 ∈ Fin) | 
| 9 |  | hoiprodp1.3 | . . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝑉) | 
| 10 |  | snidg 4660 | . . . . . . 7
⊢ (𝑍 ∈ 𝑉 → 𝑍 ∈ {𝑍}) | 
| 11 | 9, 10 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑍 ∈ {𝑍}) | 
| 12 |  | elun2 4183 | . . . . . 6
⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍})) | 
| 13 | 11, 12 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑍 ∈ (𝑌 ∪ {𝑍})) | 
| 14 | 13, 2 | eleqtrrdi 2852 | . . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑋) | 
| 15 | 14 | ne0d 4342 | . . 3
⊢ (𝜑 → 𝑋 ≠ ∅) | 
| 16 |  | hoiprodp1.a | . . 3
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) | 
| 17 |  | hoiprodp1.b | . . 3
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) | 
| 18 | 1, 8, 15, 16, 17 | hoidmvn0val 46599 | . 2
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | 
| 19 | 16 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) | 
| 20 | 17 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) | 
| 21 |  | volicore 46596 | . . . . 5
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) | 
| 22 | 19, 20, 21 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) | 
| 23 | 22 | recnd 11289 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ) | 
| 24 |  | fveq2 6906 | . . . . . 6
⊢ (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍)) | 
| 25 |  | fveq2 6906 | . . . . . 6
⊢ (𝑘 = 𝑍 → (𝐵‘𝑘) = (𝐵‘𝑍)) | 
| 26 | 24, 25 | oveq12d 7449 | . . . . 5
⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑍)[,)(𝐵‘𝑍))) | 
| 27 | 26 | fveq2d 6910 | . . . 4
⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) | 
| 28 | 27 | adantl 481 | . . 3
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍)))) | 
| 29 | 8, 23, 14, 28 | fprodsplit1 45608 | . 2
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) | 
| 30 | 2 | difeq1i 4122 | . . . . . . . 8
⊢ (𝑋 ∖ {𝑍}) = ((𝑌 ∪ {𝑍}) ∖ {𝑍}) | 
| 31 | 30 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (𝑋 ∖ {𝑍}) = ((𝑌 ∪ {𝑍}) ∖ {𝑍})) | 
| 32 |  | difun2 4481 | . . . . . . . 8
⊢ ((𝑌 ∪ {𝑍}) ∖ {𝑍}) = (𝑌 ∖ {𝑍}) | 
| 33 | 32 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ((𝑌 ∪ {𝑍}) ∖ {𝑍}) = (𝑌 ∖ {𝑍})) | 
| 34 |  | hoiprodp1.z | . . . . . . . 8
⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) | 
| 35 |  | difsn 4798 | . . . . . . . 8
⊢ (¬
𝑍 ∈ 𝑌 → (𝑌 ∖ {𝑍}) = 𝑌) | 
| 36 | 34, 35 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝑌 ∖ {𝑍}) = 𝑌) | 
| 37 | 31, 33, 36 | 3eqtrd 2781 | . . . . . 6
⊢ (𝜑 → (𝑋 ∖ {𝑍}) = 𝑌) | 
| 38 | 37 | prodeq1d 15956 | . . . . 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 7447 | . . 3
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) = ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · 𝐺)) | 
| 44 | 16, 14 | ffvelcdmd 7105 | . . . . . 6
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ) | 
| 45 | 17, 14 | ffvelcdmd 7105 | . . . . . 6
⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ) | 
| 46 |  | volicore 46596 | . . . . . 6
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ) | 
| 47 | 44, 45, 46 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℝ) | 
| 48 | 47 | recnd 11289 | . . . 4
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) ∈ ℂ) | 
| 49 | 16 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐴:𝑋⟶ℝ) | 
| 50 |  | ssun1 4178 | . . . . . . . . . . . 12
⊢ 𝑌 ⊆ (𝑌 ∪ {𝑍}) | 
| 51 | 50, 2 | sseqtrri 4033 | . . . . . . . . . . 11
⊢ 𝑌 ⊆ 𝑋 | 
| 52 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑌) | 
| 53 | 51, 52 | sselid 3981 | . . . . . . . . . 10
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑋) | 
| 54 | 53 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝑘 ∈ 𝑋) | 
| 55 | 49, 54 | ffvelcdmd 7105 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (𝐴‘𝑘) ∈ ℝ) | 
| 56 | 17 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → 𝐵:𝑋⟶ℝ) | 
| 57 | 56, 54 | ffvelcdmd 7105 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (𝐵‘𝑘) ∈ ℝ) | 
| 58 | 55, 57, 21 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑌) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) | 
| 59 | 3, 58 | fprodrecl 15989 | . . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) | 
| 60 | 39, 59 | eqeltrid 2845 | . . . . 5
⊢ (𝜑 → 𝐺 ∈ ℝ) | 
| 61 | 60 | recnd 11289 | . . . 4
⊢ (𝜑 → 𝐺 ∈ ℂ) | 
| 62 | 48, 61 | mulcomd 11282 | . . 3
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · 𝐺) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) | 
| 63 | 43, 62 | eqtrd 2777 | . 2
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) | 
| 64 | 18, 29, 63 | 3eqtrd 2781 | 1
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) |