Proof of Theorem i1fima2
Step | Hyp | Ref
| Expression |
1 | | i1fima 24823 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ 𝐴) ∈ dom vol) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ 𝐴) ∈ dom vol) |
3 | | mblvol 24675 |
. . 3
⊢ ((◡𝐹 “ 𝐴) ∈ dom vol → (vol‘(◡𝐹 “ 𝐴)) = (vol*‘(◡𝐹 “ 𝐴))) |
4 | 2, 3 | syl 17 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ 𝐴)) = (vol*‘(◡𝐹 “ 𝐴))) |
5 | | i1ff 24821 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ 𝐹:ℝ⟶ℝ) |
7 | | ffun 6599 |
. . . . . 6
⊢ (𝐹:ℝ⟶ℝ →
Fun 𝐹) |
8 | | inpreima 6935 |
. . . . . 6
⊢ (Fun
𝐹 → (◡𝐹 “ (𝐴 ∩ ran 𝐹)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹))) |
9 | 6, 7, 8 | 3syl 18 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (𝐴 ∩ ran 𝐹)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹))) |
10 | | cnvimass 5986 |
. . . . . . 7
⊢ (◡𝐹 “ 𝐴) ⊆ dom 𝐹 |
11 | | cnvimarndm 5987 |
. . . . . . 7
⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹 |
12 | 10, 11 | sseqtrri 3962 |
. . . . . 6
⊢ (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ ran 𝐹) |
13 | | df-ss 3908 |
. . . . . 6
⊢ ((◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ ran 𝐹) ↔ ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝐴)) |
14 | 12, 13 | mpbi 229 |
. . . . 5
⊢ ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝐴) |
15 | 9, 14 | eqtr2di 2796 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ 𝐴) = (◡𝐹 “ (𝐴 ∩ ran 𝐹))) |
16 | | elinel1 4133 |
. . . . . . . . 9
⊢ (0 ∈
(𝐴 ∩ ran 𝐹) → 0 ∈ 𝐴) |
17 | 16 | con3i 154 |
. . . . . . . 8
⊢ (¬ 0
∈ 𝐴 → ¬ 0
∈ (𝐴 ∩ ran 𝐹)) |
18 | 17 | adantl 481 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ ¬ 0 ∈ (𝐴
∩ ran 𝐹)) |
19 | | disjsn 4652 |
. . . . . . 7
⊢ (((𝐴 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ ¬ 0 ∈
(𝐴 ∩ ran 𝐹)) |
20 | 18, 19 | sylibr 233 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ ((𝐴 ∩ ran 𝐹) ∩ {0}) =
∅) |
21 | | inss2 4168 |
. . . . . . . . 9
⊢ (𝐴 ∩ ran 𝐹) ⊆ ran 𝐹 |
22 | 5 | frnd 6604 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ⊆
ℝ) |
23 | 21, 22 | sstrid 3936 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝐴 ∩ ran 𝐹) ⊆
ℝ) |
24 | 23 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (𝐴 ∩ ran 𝐹) ⊆
ℝ) |
25 | | reldisj 4390 |
. . . . . . 7
⊢ ((𝐴 ∩ ran 𝐹) ⊆ ℝ → (((𝐴 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖
{0}))) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (((𝐴 ∩ ran 𝐹) ∩ {0}) = ∅ ↔
(𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖
{0}))) |
27 | 20, 26 | mpbid 231 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖
{0})) |
28 | | imass2 6007 |
. . . . 5
⊢ ((𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖ {0}) →
(◡𝐹 “ (𝐴 ∩ ran 𝐹)) ⊆ (◡𝐹 “ (ℝ ∖
{0}))) |
29 | 27, 28 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (𝐴 ∩ ran 𝐹)) ⊆ (◡𝐹 “ (ℝ ∖
{0}))) |
30 | 15, 29 | eqsstrd 3963 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ (ℝ ∖
{0}))) |
31 | | i1fima 24823 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol) |
32 | 31 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol) |
33 | | mblss 24676 |
. . . 4
⊢ ((◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol → (◡𝐹 “ (ℝ ∖ {0})) ⊆
ℝ) |
34 | 32, 33 | syl 17 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (ℝ ∖ {0})) ⊆
ℝ) |
35 | | mblvol 24675 |
. . . . 5
⊢ ((◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol → (vol‘(◡𝐹 “ (ℝ ∖ {0})))
= (vol*‘(◡𝐹 “ (ℝ ∖
{0})))) |
36 | 32, 35 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) =
(vol*‘(◡𝐹 “ (ℝ ∖
{0})))) |
37 | | isi1f 24819 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
↔ (𝐹 ∈ MblFn
∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ))) |
38 | 37 | simprbi 496 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) |
39 | 38 | simp3d 1142 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) |
40 | 39 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) |
41 | 36, 40 | eqeltrrd 2841 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol*‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) |
42 | | ovolsscl 24631 |
. . 3
⊢ (((◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ (ℝ ∖ {0})) ∧ (◡𝐹 “ (ℝ ∖ {0})) ⊆
ℝ ∧ (vol*‘(◡𝐹 “ (ℝ ∖ {0})))
∈ ℝ) → (vol*‘(◡𝐹 “ 𝐴)) ∈ ℝ) |
43 | 30, 34, 41, 42 | syl3anc 1369 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol*‘(◡𝐹 “ 𝐴)) ∈ ℝ) |
44 | 4, 43 | eqeltrd 2840 |
1
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ 𝐴)) ∈ ℝ) |