Proof of Theorem i1fima2
Step | Hyp | Ref
| Expression |
1 | | i1fima 23251 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ 𝐴) ∈ dom vol) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ 𝐴) ∈ dom vol) |
3 | | mblvol 23105 |
. . 3
⊢ ((◡𝐹 “ 𝐴) ∈ dom vol → (vol‘(◡𝐹 “ 𝐴)) = (vol*‘(◡𝐹 “ 𝐴))) |
4 | 2, 3 | syl 17 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ 𝐴)) = (vol*‘(◡𝐹 “ 𝐴))) |
5 | | i1ff 23249 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ 𝐹:ℝ⟶ℝ) |
7 | | ffun 5961 |
. . . . . 6
⊢ (𝐹:ℝ⟶ℝ →
Fun 𝐹) |
8 | | inpreima 6250 |
. . . . . 6
⊢ (Fun
𝐹 → (◡𝐹 “ (𝐴 ∩ ran 𝐹)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹))) |
9 | 6, 7, 8 | 3syl 18 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (𝐴 ∩ ran 𝐹)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹))) |
10 | | cnvimass 5404 |
. . . . . . 7
⊢ (◡𝐹 “ 𝐴) ⊆ dom 𝐹 |
11 | | cnvimarndm 5405 |
. . . . . . 7
⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹 |
12 | 10, 11 | sseqtr4i 3601 |
. . . . . 6
⊢ (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ ran 𝐹) |
13 | | df-ss 3554 |
. . . . . 6
⊢ ((◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ ran 𝐹) ↔ ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝐴)) |
14 | 12, 13 | mpbi 219 |
. . . . 5
⊢ ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝐴) |
15 | 9, 14 | syl6req 2661 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ 𝐴) = (◡𝐹 “ (𝐴 ∩ ran 𝐹))) |
16 | | inss1 3795 |
. . . . . . . . . 10
⊢ (𝐴 ∩ ran 𝐹) ⊆ 𝐴 |
17 | 16 | sseli 3564 |
. . . . . . . . 9
⊢ (0 ∈
(𝐴 ∩ ran 𝐹) → 0 ∈ 𝐴) |
18 | 17 | con3i 149 |
. . . . . . . 8
⊢ (¬ 0
∈ 𝐴 → ¬ 0
∈ (𝐴 ∩ ran 𝐹)) |
19 | 18 | adantl 481 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ ¬ 0 ∈ (𝐴
∩ ran 𝐹)) |
20 | | disjsn 4192 |
. . . . . . 7
⊢ (((𝐴 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ ¬ 0 ∈
(𝐴 ∩ ran 𝐹)) |
21 | 19, 20 | sylibr 223 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ ((𝐴 ∩ ran 𝐹) ∩ {0}) =
∅) |
22 | | inss2 3796 |
. . . . . . . . 9
⊢ (𝐴 ∩ ran 𝐹) ⊆ ran 𝐹 |
23 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐹:ℝ⟶ℝ →
ran 𝐹 ⊆
ℝ) |
24 | 5, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ⊆
ℝ) |
25 | 22, 24 | syl5ss 3579 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝐴 ∩ ran 𝐹) ⊆
ℝ) |
26 | 25 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (𝐴 ∩ ran 𝐹) ⊆
ℝ) |
27 | | reldisj 3972 |
. . . . . . 7
⊢ ((𝐴 ∩ ran 𝐹) ⊆ ℝ → (((𝐴 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖
{0}))) |
28 | 26, 27 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (((𝐴 ∩ ran 𝐹) ∩ {0}) = ∅ ↔
(𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖
{0}))) |
29 | 21, 28 | mpbid 221 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖
{0})) |
30 | | imass2 5420 |
. . . . 5
⊢ ((𝐴 ∩ ran 𝐹) ⊆ (ℝ ∖ {0}) →
(◡𝐹 “ (𝐴 ∩ ran 𝐹)) ⊆ (◡𝐹 “ (ℝ ∖
{0}))) |
31 | 29, 30 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (𝐴 ∩ ran 𝐹)) ⊆ (◡𝐹 “ (ℝ ∖
{0}))) |
32 | 15, 31 | eqsstrd 3602 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ (ℝ ∖
{0}))) |
33 | | i1fima 23251 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol) |
34 | 33 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol) |
35 | | mblss 23106 |
. . . 4
⊢ ((◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol → (◡𝐹 “ (ℝ ∖ {0})) ⊆
ℝ) |
36 | 34, 35 | syl 17 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (◡𝐹 “ (ℝ ∖ {0})) ⊆
ℝ) |
37 | | mblvol 23105 |
. . . . 5
⊢ ((◡𝐹 “ (ℝ ∖ {0})) ∈ dom
vol → (vol‘(◡𝐹 “ (ℝ ∖ {0})))
= (vol*‘(◡𝐹 “ (ℝ ∖
{0})))) |
38 | 34, 37 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) =
(vol*‘(◡𝐹 “ (ℝ ∖
{0})))) |
39 | | isi1f 23247 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
↔ (𝐹 ∈ MblFn
∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ))) |
40 | 39 | simprbi 479 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) |
41 | 40 | simp3d 1068 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) |
42 | 41 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) |
43 | 38, 42 | eqeltrrd 2689 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol*‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) |
44 | | ovolsscl 23061 |
. . 3
⊢ (((◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ (ℝ ∖ {0})) ∧ (◡𝐹 “ (ℝ ∖ {0})) ⊆
ℝ ∧ (vol*‘(◡𝐹 “ (ℝ ∖ {0})))
∈ ℝ) → (vol*‘(◡𝐹 “ 𝐴)) ∈ ℝ) |
45 | 32, 36, 43, 44 | syl3anc 1318 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol*‘(◡𝐹 “ 𝐴)) ∈ ℝ) |
46 | 4, 45 | eqeltrd 2688 |
1
⊢ ((𝐹 ∈ dom ∫1
∧ ¬ 0 ∈ 𝐴)
→ (vol‘(◡𝐹 “ 𝐴)) ∈ ℝ) |