Proof of Theorem i1fima2
| Step | Hyp | Ref
| Expression |
| 1 | | i1fima 25713 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ 𝐴) ∈ dom vol) |
| 2 | 1 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ 𝐴) ∈ dom vol) |
| 3 | | mblvol 25565 |
. . 3
⊢ ((◡𝐹 “ 𝐴) ∈ dom vol → (vol‘(◡𝐹 “ 𝐴)) = (vol*‘(◡𝐹 “ 𝐴))) |
| 4 | 2, 3 | syl 17 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ 𝐴)) = (vol*‘(◡𝐹 “ 𝐴))) |
| 5 | | i1ff 25711 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
| 6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ 𝐹:ℝ⟶ℝ) |
| 7 | | ffun 6739 |
. . . . . 6
⊢ (𝐹:ℝ⟶ℝ →
Fun 𝐹) |
| 8 | | inpreima 7084 |
. . . . . 6
⊢ (Fun
𝐹 → (◡𝐹 “ (𝐴 ∩ ran 𝐹)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹))) |
| 9 | 6, 7, 8 | 3syl 18 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (𝐴 ∩ ran 𝐹)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹))) |
| 10 | | cnvimass 6100 |
. . . . . . 7
⊢ (◡𝐹 “ 𝐴) ⊆ dom 𝐹 |
| 11 | | cnvimarndm 6101 |
. . . . . . 7
⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹 |
| 12 | 10, 11 | sseqtrri 4033 |
. . . . . 6
⊢ (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ ran 𝐹) |
| 13 | | dfss2 3969 |
. . . . . 6
⊢ ((◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ ran 𝐹) ↔ ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝐴)) |
| 14 | 12, 13 | mpbi 230 |
. . . . 5
⊢ ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝐴) |
| 15 | 9, 14 | eqtr2di 2794 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ 𝐴) = (◡𝐹 “ (𝐴 ∩ ran 𝐹))) |
| 16 | | elinel1 4201 |
. . . . . . . . 9
⊢ (0 ∈
(𝐴 ∩ ran 𝐹) → 0 ∈ 𝐴) |
| 17 | 16 | con3i 154 |
. . . . . . . 8
⊢ (¬ 0
∈ 𝐴 → ¬ 0
∈ (𝐴 ∩ ran 𝐹)) |
| 18 | 17 | adantl 481 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ ¬ 0 ∈ (𝐴
∩ ran 𝐹)) |
| 19 | | disjsn 4711 |
. . . . . . 7
⊢ (((𝐴 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ ¬ 0 ∈
(𝐴 ∩ ran 𝐹)) |
| 20 | 18, 19 | sylibr 234 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ ((𝐴 ∩ ran 𝐹) ∩ {0}) =
∅) |
| 21 | | inss2 4238 |
. . . . . . . . 9
⊢ (𝐴 ∩ ran 𝐹) ⊆ ran 𝐹 |
| 22 | 5 | frnd 6744 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ⊆
ℝ) |
| 23 | 21, 22 | sstrid 3995 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝐴 ∩ ran 𝐹) ⊆
ℝ) |
| 24 | 23 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (𝐴 ∩ ran 𝐹) ⊆
ℝ) |
| 25 | | reldisj 4453 |
. . . . . . 7
⊢ ((𝐴 ∩ ran 𝐹) ⊆ ℝ → (((𝐴 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖
{0}))) |
| 26 | 24, 25 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (((𝐴 ∩ ran 𝐹) ∩ {0}) = ∅ ↔
(𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖
{0}))) |
| 27 | 20, 26 | mpbid 232 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖
{0})) |
| 28 | | imass2 6120 |
. . . . 5
⊢ ((𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖ {0}) →
(◡𝐹 “ (𝐴 ∩ ran 𝐹)) ⊆ (◡𝐹 “ (ℝ ∖
{0}))) |
| 29 | 27, 28 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (𝐴 ∩ ran 𝐹)) ⊆ (◡𝐹 “ (ℝ ∖
{0}))) |
| 30 | 15, 29 | eqsstrd 4018 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ (ℝ ∖
{0}))) |
| 31 | | i1fima 25713 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol) |
| 32 | 31 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol) |
| 33 | | mblss 25566 |
. . . 4
⊢ ((◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol → (◡𝐹 “ (ℝ ∖ {0})) ⊆
ℝ) |
| 34 | 32, 33 | syl 17 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (ℝ ∖ {0})) ⊆
ℝ) |
| 35 | | mblvol 25565 |
. . . . 5
⊢ ((◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol → (vol‘(◡𝐹 “ (ℝ ∖ {0})))
= (vol*‘(◡𝐹 “ (ℝ ∖
{0})))) |
| 36 | 32, 35 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) =
(vol*‘(◡𝐹 “ (ℝ ∖
{0})))) |
| 37 | | isi1f 25709 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
↔ (𝐹 ∈ MblFn
∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ))) |
| 38 | 37 | simprbi 496 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) |
| 39 | 38 | simp3d 1145 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) |
| 40 | 39 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) |
| 41 | 36, 40 | eqeltrrd 2842 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol*‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) |
| 42 | | ovolsscl 25521 |
. . 3
⊢ (((◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ (ℝ ∖ {0})) ∧ (◡𝐹 “ (ℝ ∖ {0})) ⊆
ℝ ∧ (vol*‘(◡𝐹 “ (ℝ ∖ {0})))
∈ ℝ) → (vol*‘(◡𝐹 “ 𝐴)) ∈ ℝ) |
| 43 | 30, 34, 41, 42 | syl3anc 1373 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol*‘(◡𝐹 “ 𝐴)) ∈ ℝ) |
| 44 | 4, 43 | eqeltrd 2841 |
1
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ 𝐴)) ∈ ℝ) |