Step | Hyp | Ref
| Expression |
1 | | i1ff 23249 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
2 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐹:ℝ⟶ℝ) |
3 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐹 Fn
ℝ) |
5 | | fnfvelrn 6264 |
. . . . . 6
⊢ ((𝐹 Fn ℝ ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ran 𝐹) |
6 | 4, 5 | sylan 487 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈ ran 𝐹) |
7 | | i1f0rn 23255 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 0 ∈ ran 𝐹) |
8 | 7 | ad2antrr 758 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑥 ∈ ℝ)
→ 0 ∈ ran 𝐹) |
9 | 6, 8 | ifcld 4081 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑥 ∈ ℝ)
→ if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0) ∈ ran 𝐹) |
10 | | i1fres.1 |
. . . 4
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0)) |
11 | 9, 10 | fmptd 6292 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐺:ℝ⟶ran
𝐹) |
12 | | frn 5966 |
. . . 4
⊢ (𝐹:ℝ⟶ℝ →
ran 𝐹 ⊆
ℝ) |
13 | 2, 12 | syl 17 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ ran 𝐹 ⊆
ℝ) |
14 | 11, 13 | fssd 5970 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐺:ℝ⟶ℝ) |
15 | | i1frn 23250 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
16 | 15 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ ran 𝐹 ∈
Fin) |
17 | | frn 5966 |
. . . 4
⊢ (𝐺:ℝ⟶ran 𝐹 → ran 𝐺 ⊆ ran 𝐹) |
18 | 11, 17 | syl 17 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ ran 𝐺 ⊆ ran
𝐹) |
19 | | ssfi 8065 |
. . 3
⊢ ((ran
𝐹 ∈ Fin ∧ ran
𝐺 ⊆ ran 𝐹) → ran 𝐺 ∈ Fin) |
20 | 16, 18, 19 | syl2anc 691 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ ran 𝐺 ∈
Fin) |
21 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
22 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
23 | 21, 22 | ifbieq1d 4059 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0) = if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0)) |
24 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘𝑧) ∈ V |
25 | | c0ex 9913 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
26 | 24, 25 | ifex 4106 |
. . . . . . . . . . . . 13
⊢ if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) ∈ V |
27 | 23, 10, 26 | fvmpt 6191 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ → (𝐺‘𝑧) = if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0)) |
28 | 27 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → (𝐺‘𝑧) = if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0)) |
29 | 28 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → ((𝐺‘𝑧) = 𝑦 ↔ if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦)) |
30 | | eldifsni 4261 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (ran 𝐺 ∖ {0}) → 𝑦 ≠ 0) |
31 | 30 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → 𝑦 ≠ 0) |
32 | 31 | necomd 2837 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → 0 ≠
𝑦) |
33 | | iffalse 4045 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑧 ∈ 𝐴 → if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 0) |
34 | 33 | neeq1d 2841 |
. . . . . . . . . . . . 13
⊢ (¬
𝑧 ∈ 𝐴 → (if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) ≠ 𝑦 ↔ 0 ≠ 𝑦)) |
35 | 32, 34 | syl5ibrcom 236 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → (¬
𝑧 ∈ 𝐴 → if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) ≠ 𝑦)) |
36 | 35 | necon4bd 2802 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) →
(if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦 → 𝑧 ∈ 𝐴)) |
37 | 36 | pm4.71rd 665 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) →
(if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦 ↔ (𝑧 ∈ 𝐴 ∧ if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦))) |
38 | 29, 37 | bitrd 267 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → ((𝐺‘𝑧) = 𝑦 ↔ (𝑧 ∈ 𝐴 ∧ if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦))) |
39 | | iftrue 4042 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐴 → if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = (𝐹‘𝑧)) |
40 | 39 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐴 → (if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦 ↔ (𝐹‘𝑧) = 𝑦)) |
41 | 40 | pm5.32i 667 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐴 ∧ if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) = 𝑦)) |
42 | 38, 41 | syl6bb 275 |
. . . . . . . 8
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → ((𝐺‘𝑧) = 𝑦 ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) = 𝑦))) |
43 | 42 | pm5.32da 671 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → ((𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦) ↔ (𝑧 ∈ ℝ ∧ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) = 𝑦)))) |
44 | | an12 834 |
. . . . . . 7
⊢ ((𝑧 ∈ ℝ ∧ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) = 𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = 𝑦))) |
45 | 43, 44 | syl6bb 275 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → ((𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦) ↔ (𝑧 ∈ 𝐴 ∧ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = 𝑦)))) |
46 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐺:ℝ⟶ran 𝐹 → 𝐺 Fn ℝ) |
47 | 11, 46 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐺 Fn
ℝ) |
48 | 47 | adantr 480 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → 𝐺 Fn ℝ) |
49 | | fniniseg 6246 |
. . . . . . 7
⊢ (𝐺 Fn ℝ → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) |
50 | 48, 49 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) |
51 | 4 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → 𝐹 Fn ℝ) |
52 | | fniniseg 6246 |
. . . . . . . 8
⊢ (𝐹 Fn ℝ → (𝑧 ∈ (◡𝐹 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = 𝑦))) |
53 | 51, 52 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ (◡𝐹 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = 𝑦))) |
54 | 53 | anbi2d 736 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → ((𝑧 ∈ 𝐴 ∧ 𝑧 ∈ (◡𝐹 “ {𝑦})) ↔ (𝑧 ∈ 𝐴 ∧ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = 𝑦)))) |
55 | 45, 50, 54 | 3bitr4d 299 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ (◡𝐹 “ {𝑦})))) |
56 | | elin 3758 |
. . . . 5
⊢ (𝑧 ∈ (𝐴 ∩ (◡𝐹 “ {𝑦})) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ (◡𝐹 “ {𝑦}))) |
57 | 55, 56 | syl6bbr 277 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ 𝑧 ∈ (𝐴 ∩ (◡𝐹 “ {𝑦})))) |
58 | 57 | eqrdv 2608 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑦}) = (𝐴 ∩ (◡𝐹 “ {𝑦}))) |
59 | | simplr 788 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → 𝐴 ∈ dom
vol) |
60 | | i1fima 23251 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {𝑦}) ∈ dom vol) |
61 | 60 | ad2antrr 758 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (◡𝐹 “ {𝑦}) ∈ dom vol) |
62 | | inmbl 23117 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ (◡𝐹 “ {𝑦}) ∈ dom vol) → (𝐴 ∩ (◡𝐹 “ {𝑦})) ∈ dom vol) |
63 | 59, 61, 62 | syl2anc 691 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝐴 ∩ (◡𝐹 “ {𝑦})) ∈ dom vol) |
64 | 58, 63 | eqeltrd 2688 |
. 2
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑦}) ∈ dom vol) |
65 | 58 | fveq2d 6107 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑦})) = (vol‘(𝐴 ∩ (◡𝐹 “ {𝑦})))) |
66 | | mblvol 23105 |
. . . . 5
⊢ ((𝐴 ∩ (◡𝐹 “ {𝑦})) ∈ dom vol → (vol‘(𝐴 ∩ (◡𝐹 “ {𝑦}))) = (vol*‘(𝐴 ∩ (◡𝐹 “ {𝑦})))) |
67 | 63, 66 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(𝐴 ∩ (◡𝐹 “ {𝑦}))) = (vol*‘(𝐴 ∩ (◡𝐹 “ {𝑦})))) |
68 | 65, 67 | eqtrd 2644 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑦})) = (vol*‘(𝐴 ∩ (◡𝐹 “ {𝑦})))) |
69 | | inss2 3796 |
. . . . 5
⊢ (𝐴 ∩ (◡𝐹 “ {𝑦})) ⊆ (◡𝐹 “ {𝑦}) |
70 | 69 | a1i 11 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝐴 ∩ (◡𝐹 “ {𝑦})) ⊆ (◡𝐹 “ {𝑦})) |
71 | | mblss 23106 |
. . . . 5
⊢ ((◡𝐹 “ {𝑦}) ∈ dom vol → (◡𝐹 “ {𝑦}) ⊆ ℝ) |
72 | 61, 71 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (◡𝐹 “ {𝑦}) ⊆ ℝ) |
73 | | mblvol 23105 |
. . . . . 6
⊢ ((◡𝐹 “ {𝑦}) ∈ dom vol → (vol‘(◡𝐹 “ {𝑦})) = (vol*‘(◡𝐹 “ {𝑦}))) |
74 | 61, 73 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑦})) = (vol*‘(◡𝐹 “ {𝑦}))) |
75 | | i1fima2sn 23253 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
76 | 75 | adantlr 747 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
77 | 74, 76 | eqeltrrd 2689 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol*‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
78 | | ovolsscl 23061 |
. . . 4
⊢ (((𝐴 ∩ (◡𝐹 “ {𝑦})) ⊆ (◡𝐹 “ {𝑦}) ∧ (◡𝐹 “ {𝑦}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑦})) ∈ ℝ) → (vol*‘(𝐴 ∩ (◡𝐹 “ {𝑦}))) ∈ ℝ) |
79 | 70, 72, 77, 78 | syl3anc 1318 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol*‘(𝐴 ∩ (◡𝐹 “ {𝑦}))) ∈ ℝ) |
80 | 68, 79 | eqeltrd 2688 |
. 2
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑦})) ∈ ℝ) |
81 | 14, 20, 64, 80 | i1fd 23254 |
1
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐺 ∈ dom
∫1) |