| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | reex 11247 | . . . . 5
⊢ ℝ
∈ V | 
| 2 | 1 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → ℝ ∈
V) | 
| 3 |  | i1fmulc.2 | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ dom
∫1) | 
| 4 |  | i1ff 25712 | . . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) | 
| 5 | 3, 4 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) | 
| 6 | 5 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐹:ℝ⟶ℝ) | 
| 7 |  | i1fmulc.3 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 8 | 7 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐴 ∈ ℝ) | 
| 9 |  | 0red 11265 | . . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → 0 ∈
ℝ) | 
| 10 |  | simplr 768 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → 𝐴 = 0) | 
| 11 | 10 | oveq1d 7447 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = (0 · 𝑥)) | 
| 12 |  | mul02lem2 11439 | . . . . . 6
⊢ (𝑥 ∈ ℝ → (0
· 𝑥) =
0) | 
| 13 | 12 | adantl 481 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0) | 
| 14 | 11, 13 | eqtrd 2776 | . . . 4
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = 0) | 
| 15 | 2, 6, 8, 9, 14 | caofid2 7734 | . . 3
⊢ ((𝜑 ∧ 𝐴 = 0) → ((ℝ × {𝐴}) ∘f ·
𝐹) = (ℝ ×
{0})) | 
| 16 |  | i1f0 25723 | . . 3
⊢ (ℝ
× {0}) ∈ dom ∫1 | 
| 17 | 15, 16 | eqeltrdi 2848 | . 2
⊢ ((𝜑 ∧ 𝐴 = 0) → ((ℝ × {𝐴}) ∘f ·
𝐹) ∈ dom
∫1) | 
| 18 |  | remulcl 11241 | . . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) | 
| 19 | 18 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) | 
| 20 |  | fconst6g 6796 | . . . . . 6
⊢ (𝐴 ∈ ℝ → (ℝ
× {𝐴}):ℝ⟶ℝ) | 
| 21 | 7, 20 | syl 17 | . . . . 5
⊢ (𝜑 → (ℝ × {𝐴}):ℝ⟶ℝ) | 
| 22 | 1 | a1i 11 | . . . . 5
⊢ (𝜑 → ℝ ∈
V) | 
| 23 |  | inidm 4226 | . . . . 5
⊢ (ℝ
∩ ℝ) = ℝ | 
| 24 | 19, 21, 5, 22, 22, 23 | off 7716 | . . . 4
⊢ (𝜑 → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶ℝ) | 
| 25 | 24 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶ℝ) | 
| 26 |  | i1frn 25713 | . . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) | 
| 27 | 3, 26 | syl 17 | . . . . . 6
⊢ (𝜑 → ran 𝐹 ∈ Fin) | 
| 28 |  | ovex 7465 | . . . . . . . 8
⊢ (𝐴 · 𝑦) ∈ V | 
| 29 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) | 
| 30 | 28, 29 | fnmpti 6710 | . . . . . . 7
⊢ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) Fn ran 𝐹 | 
| 31 |  | dffn4 6825 | . . . . . . 7
⊢ ((𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) Fn ran 𝐹 ↔ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)):ran 𝐹–onto→ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦))) | 
| 32 | 30, 31 | mpbi 230 | . . . . . 6
⊢ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)):ran 𝐹–onto→ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) | 
| 33 |  | fofi 9352 | . . . . . 6
⊢ ((ran
𝐹 ∈ Fin ∧ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)):ran 𝐹–onto→ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦))) → ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) ∈ Fin) | 
| 34 | 27, 32, 33 | sylancl 586 | . . . . 5
⊢ (𝜑 → ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) ∈ Fin) | 
| 35 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑤 ∈ ran 𝐹 → 𝑤 ∈ ran 𝐹) | 
| 36 |  | elsni 4642 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝐴} → 𝑥 = 𝐴) | 
| 37 | 36 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝑥 ∈ {𝐴} → (𝑥 · 𝑤) = (𝐴 · 𝑤)) | 
| 38 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝐴 · 𝑦) = (𝐴 · 𝑤)) | 
| 39 | 38 | rspceeqv 3644 | . . . . . . . . . . 11
⊢ ((𝑤 ∈ ran 𝐹 ∧ (𝑥 · 𝑤) = (𝐴 · 𝑤)) → ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦)) | 
| 40 | 35, 37, 39 | syl2anr 597 | . . . . . . . . . 10
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑤 ∈ ran 𝐹) → ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦)) | 
| 41 |  | ovex 7465 | . . . . . . . . . . 11
⊢ (𝑥 · 𝑤) ∈ V | 
| 42 |  | eqeq1 2740 | . . . . . . . . . . . 12
⊢ (𝑧 = (𝑥 · 𝑤) → (𝑧 = (𝐴 · 𝑦) ↔ (𝑥 · 𝑤) = (𝐴 · 𝑦))) | 
| 43 | 42 | rexbidv 3178 | . . . . . . . . . . 11
⊢ (𝑧 = (𝑥 · 𝑤) → (∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦) ↔ ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦))) | 
| 44 | 41, 43 | elab 3678 | . . . . . . . . . 10
⊢ ((𝑥 · 𝑤) ∈ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)} ↔ ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦)) | 
| 45 | 40, 44 | sylibr 234 | . . . . . . . . 9
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑤 ∈ ran 𝐹) → (𝑥 · 𝑤) ∈ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) | 
| 46 | 45 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ {𝐴} ∧ 𝑤 ∈ ran 𝐹)) → (𝑥 · 𝑤) ∈ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) | 
| 47 |  | fconstg 6794 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (ℝ
× {𝐴}):ℝ⟶{𝐴}) | 
| 48 | 7, 47 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (ℝ × {𝐴}):ℝ⟶{𝐴}) | 
| 49 | 5 | ffnd 6736 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn ℝ) | 
| 50 |  | dffn3 6747 | . . . . . . . . 9
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) | 
| 51 | 49, 50 | sylib 218 | . . . . . . . 8
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) | 
| 52 | 46, 48, 51, 22, 22, 23 | off 7716 | . . . . . . 7
⊢ (𝜑 → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶{𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) | 
| 53 | 52 | frnd 6743 | . . . . . 6
⊢ (𝜑 → ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ⊆ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) | 
| 54 | 29 | rnmpt 5967 | . . . . . 6
⊢ ran
(𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) = {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)} | 
| 55 | 53, 54 | sseqtrrdi 4024 | . . . . 5
⊢ (𝜑 → ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ⊆ ran
(𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦))) | 
| 56 | 34, 55 | ssfid 9302 | . . . 4
⊢ (𝜑 → ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∈
Fin) | 
| 57 | 56 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∈
Fin) | 
| 58 | 24 | frnd 6743 | . . . . . . . 8
⊢ (𝜑 → ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ⊆
ℝ) | 
| 59 | 58 | ssdifssd 4146 | . . . . . . 7
⊢ (𝜑 → (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
⊆ ℝ) | 
| 60 | 59 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
⊆ ℝ) | 
| 61 | 60 | sselda 3982 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑦 ∈
ℝ) | 
| 62 | 3, 7 | i1fmulclem 25738 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑦}) = (◡𝐹 “ {(𝑦 / 𝐴)})) | 
| 63 | 61, 62 | syldan 591 | . . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑦}) = (◡𝐹 “ {(𝑦 / 𝐴)})) | 
| 64 |  | i1fima 25714 | . . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {(𝑦 / 𝐴)}) ∈ dom vol) | 
| 65 | 3, 64 | syl 17 | . . . . 5
⊢ (𝜑 → (◡𝐹 “ {(𝑦 / 𝐴)}) ∈ dom vol) | 
| 66 | 65 | ad2antrr 726 | . . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(◡𝐹 “ {(𝑦 / 𝐴)}) ∈ dom vol) | 
| 67 | 63, 66 | eqeltrd 2840 | . . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑦}) ∈ dom vol) | 
| 68 | 63 | fveq2d 6909 | . . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(vol‘(◡((ℝ × {𝐴}) ∘f ·
𝐹) “ {𝑦})) = (vol‘(◡𝐹 “ {(𝑦 / 𝐴)}))) | 
| 69 | 3 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐹 ∈ dom
∫1) | 
| 70 | 7 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ∈
ℝ) | 
| 71 |  | simplr 768 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ≠ 0) | 
| 72 | 61, 70, 71 | redivcld 12096 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑦 / 𝐴) ∈ ℝ) | 
| 73 | 61 | recnd 11290 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑦 ∈
ℂ) | 
| 74 | 70 | recnd 11290 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ∈
ℂ) | 
| 75 |  | eldifsni 4789 | . . . . . . . 8
⊢ (𝑦 ∈ (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
→ 𝑦 ≠
0) | 
| 76 | 75 | adantl 481 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑦 ≠ 0) | 
| 77 | 73, 74, 76, 71 | divne0d 12060 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑦 / 𝐴) ≠ 0) | 
| 78 |  | eldifsn 4785 | . . . . . 6
⊢ ((𝑦 / 𝐴) ∈ (ℝ ∖ {0}) ↔
((𝑦 / 𝐴) ∈ ℝ ∧ (𝑦 / 𝐴) ≠ 0)) | 
| 79 | 72, 77, 78 | sylanbrc 583 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑦 / 𝐴) ∈ (ℝ ∖
{0})) | 
| 80 |  | i1fima2sn 25716 | . . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ (𝑦 / 𝐴) ∈ (ℝ ∖ {0}))
→ (vol‘(◡𝐹 “ {(𝑦 / 𝐴)})) ∈ ℝ) | 
| 81 | 69, 79, 80 | syl2anc 584 | . . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(vol‘(◡𝐹 “ {(𝑦 / 𝐴)})) ∈ ℝ) | 
| 82 | 68, 81 | eqeltrd 2840 | . . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(vol‘(◡((ℝ × {𝐴}) ∘f ·
𝐹) “ {𝑦})) ∈
ℝ) | 
| 83 | 25, 57, 67, 82 | i1fd 25717 | . 2
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘f ·
𝐹) ∈ dom
∫1) | 
| 84 | 17, 83 | pm2.61dane 3028 | 1
⊢ (𝜑 → ((ℝ × {𝐴}) ∘f ·
𝐹) ∈ dom
∫1) |