Step | Hyp | Ref
| Expression |
1 | | readdcl 9898 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ) |
2 | 1 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ) |
3 | | i1fadd.1 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
4 | | i1ff 23249 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
6 | | i1fadd.2 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
7 | | i1ff 23249 |
. . . 4
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
8 | 6, 7 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
9 | | reex 9906 |
. . . 4
⊢ ℝ
∈ V |
10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ ∈
V) |
11 | | inidm 3784 |
. . 3
⊢ (ℝ
∩ ℝ) = ℝ |
12 | 2, 5, 8, 10, 10, 11 | off 6810 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):ℝ⟶ℝ) |
13 | | i1frn 23250 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
14 | 3, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
15 | | i1frn 23250 |
. . . . . 6
⊢ (𝐺 ∈ dom ∫1
→ ran 𝐺 ∈
Fin) |
16 | 6, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
17 | | xpfi 8116 |
. . . . 5
⊢ ((ran
𝐹 ∈ Fin ∧ ran
𝐺 ∈ Fin) → (ran
𝐹 × ran 𝐺) ∈ Fin) |
18 | 14, 16, 17 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin) |
19 | | eqid 2610 |
. . . . . 6
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) = (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) |
20 | | ovex 6577 |
. . . . . 6
⊢ (𝑢 + 𝑣) ∈ V |
21 | 19, 20 | fnmpt2i 7128 |
. . . . 5
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) Fn (ran 𝐹 × ran 𝐺) |
22 | | dffn4 6034 |
. . . . 5
⊢ ((𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) Fn (ran 𝐹 × ran 𝐺) ↔ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))) |
23 | 21, 22 | mpbi 219 |
. . . 4
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) |
24 | | fofi 8135 |
. . . 4
⊢ (((ran
𝐹 × ran 𝐺) ∈ Fin ∧ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))) → ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) ∈ Fin) |
25 | 18, 23, 24 | sylancl 693 |
. . 3
⊢ (𝜑 → ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) ∈ Fin) |
26 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 + 𝑦) = (𝑥 + 𝑦) |
27 | | rspceov 6590 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ∧ (𝑥 + 𝑦) = (𝑥 + 𝑦)) → ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣)) |
28 | 26, 27 | mp3an3 1405 |
. . . . . . . 8
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣)) |
29 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑥 + 𝑦) ∈ V |
30 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 + 𝑦) → (𝑤 = (𝑢 + 𝑣) ↔ (𝑥 + 𝑦) = (𝑢 + 𝑣))) |
31 | 30 | 2rexbidv 3039 |
. . . . . . . . 9
⊢ (𝑤 = (𝑥 + 𝑦) → (∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣) ↔ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣))) |
32 | 29, 31 | elab 3319 |
. . . . . . . 8
⊢ ((𝑥 + 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)} ↔ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣)) |
33 | 28, 32 | sylibr 223 |
. . . . . . 7
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → (𝑥 + 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}) |
34 | 33 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}) |
35 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
36 | 5, 35 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn ℝ) |
37 | | dffn3 5967 |
. . . . . . 7
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) |
38 | 36, 37 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) |
39 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐺:ℝ⟶ℝ →
𝐺 Fn
ℝ) |
40 | 8, 39 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn ℝ) |
41 | | dffn3 5967 |
. . . . . . 7
⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺) |
42 | 40, 41 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺) |
43 | 34, 38, 42, 10, 10, 11 | off 6810 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):ℝ⟶{𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}) |
44 | | frn 5966 |
. . . . 5
⊢ ((𝐹 ∘𝑓 +
𝐺):ℝ⟶{𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)} → ran (𝐹 ∘𝑓 + 𝐺) ⊆ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}) |
45 | 43, 44 | syl 17 |
. . . 4
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}) |
46 | 19 | rnmpt2 6668 |
. . . 4
⊢ ran
(𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) = {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)} |
47 | 45, 46 | syl6sseqr 3615 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))) |
48 | | ssfi 8065 |
. . 3
⊢ ((ran
(𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) ∈ Fin ∧ ran (𝐹 ∘𝑓 + 𝐺) ⊆ ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))) → ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin) |
49 | 25, 47, 48 | syl2anc 691 |
. 2
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin) |
50 | | frn 5966 |
. . . . . . . 8
⊢ ((𝐹 ∘𝑓 +
𝐺):ℝ⟶ℝ
→ ran (𝐹
∘𝑓 + 𝐺) ⊆ ℝ) |
51 | 12, 50 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆
ℝ) |
52 | 51 | ssdifssd 3710 |
. . . . . 6
⊢ (𝜑 → (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0}) ⊆
ℝ) |
53 | 52 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → 𝑦 ∈
ℝ) |
54 | 53 | recnd 9947 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → 𝑦 ∈
ℂ) |
55 | 3, 6 | i1faddlem 23266 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
56 | 54, 55 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
57 | 16 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → ran 𝐺 ∈ Fin) |
58 | 3 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹 ∈ dom
∫1) |
59 | | i1fmbf 23248 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
MblFn) |
60 | 58, 59 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹 ∈ MblFn) |
61 | 5 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹:ℝ⟶ℝ) |
62 | 12 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝐹 ∘𝑓 + 𝐺):ℝ⟶ℝ) |
63 | 62, 50 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ran (𝐹 ∘𝑓 + 𝐺) ⊆
ℝ) |
64 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0}) → 𝑦 ∈ ran (𝐹 ∘𝑓 + 𝐺)) |
65 | 64 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑦 ∈ ran (𝐹 ∘𝑓 + 𝐺)) |
66 | 63, 65 | sseldd 3569 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑦 ∈ ℝ) |
67 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → 𝐺:ℝ⟶ℝ) |
68 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐺:ℝ⟶ℝ →
ran 𝐺 ⊆
ℝ) |
69 | 67, 68 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → ran 𝐺 ⊆
ℝ) |
70 | 69 | sselda 3568 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ) |
71 | 66, 70 | resubcld 10337 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑦 − 𝑧) ∈ ℝ) |
72 | | mbfimasn 23207 |
. . . . . . 7
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧
(𝑦 − 𝑧) ∈ ℝ) → (◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol) |
73 | 60, 61, 71, 72 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol) |
74 | 6 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺 ∈ dom
∫1) |
75 | | i1fmbf 23248 |
. . . . . . . 8
⊢ (𝐺 ∈ dom ∫1
→ 𝐺 ∈
MblFn) |
76 | 74, 75 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺 ∈ MblFn) |
77 | 8 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺:ℝ⟶ℝ) |
78 | | mbfimasn 23207 |
. . . . . . 7
⊢ ((𝐺 ∈ MblFn ∧ 𝐺:ℝ⟶ℝ ∧
𝑧 ∈ ℝ) →
(◡𝐺 “ {𝑧}) ∈ dom vol) |
79 | 76, 77, 70, 78 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (◡𝐺 “ {𝑧}) ∈ dom vol) |
80 | | inmbl 23117 |
. . . . . 6
⊢ (((◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol ∧ (◡𝐺 “ {𝑧}) ∈ dom vol) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
81 | 73, 79, 80 | syl2anc 691 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
82 | 81 | ralrimiva 2949 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
∀𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
83 | | finiunmbl 23119 |
. . . 4
⊢ ((ran
𝐺 ∈ Fin ∧
∀𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) → ∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
84 | 57, 82, 83 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → ∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
85 | 56, 84 | eqeltrd 2688 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ∈ dom vol) |
86 | | mblvol 23105 |
. . . 4
⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ∈ dom vol → (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}))) |
87 | 85, 86 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}))) |
88 | | mblss 23106 |
. . . . 5
⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ∈ dom vol → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ⊆ ℝ) |
89 | 85, 88 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ⊆ ℝ) |
90 | | inss1 3795 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {(𝑦 − 𝑧)}) |
91 | 90 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {(𝑦 − 𝑧)})) |
92 | 73 | adantrr 749 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol) |
93 | | mblss 23106 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol → (◡𝐹 “ {(𝑦 − 𝑧)}) ⊆ ℝ) |
94 | 92, 93 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (◡𝐹 “ {(𝑦 − 𝑧)}) ⊆ ℝ) |
95 | | mblvol 23105 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) = (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)}))) |
96 | 92, 95 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) = (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)}))) |
97 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → 𝑧 = 0) |
98 | 97 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (𝑦 − 𝑧) = (𝑦 − 0)) |
99 | 54 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → 𝑦 ∈ ℂ) |
100 | 99 | subid1d 10260 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (𝑦 − 0) = 𝑦) |
101 | 98, 100 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (𝑦 − 𝑧) = 𝑦) |
102 | 101 | sneqd 4137 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → {(𝑦 − 𝑧)} = {𝑦}) |
103 | 102 | imaeq2d 5385 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (◡𝐹 “ {(𝑦 − 𝑧)}) = (◡𝐹 “ {𝑦})) |
104 | 103 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) = (vol‘(◡𝐹 “ {𝑦}))) |
105 | | i1fima2sn 23253 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 +
𝐺) ∖ {0})) →
(vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
106 | 3, 105 | sylan 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
107 | 106 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
108 | 104, 107 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) ∈ ℝ) |
109 | 96, 108 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)})) ∈ ℝ) |
110 | | ovolsscl 23061 |
. . . . . . . 8
⊢ ((((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {(𝑦 − 𝑧)}) ∧ (◡𝐹 “ {(𝑦 − 𝑧)}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
111 | 91, 94, 109, 110 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
112 | 111 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑧 = 0 → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
113 | | eldifsn 4260 |
. . . . . . . 8
⊢ (𝑧 ∈ (ran 𝐺 ∖ {0}) ↔ (𝑧 ∈ ran 𝐺 ∧ 𝑧 ≠ 0)) |
114 | | inss2 3796 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) |
115 | 114 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧})) |
116 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (ran 𝐺 ∖ {0}) → 𝑧 ∈ ran 𝐺) |
117 | | mblss 23106 |
. . . . . . . . . . 11
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
118 | 79, 117 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
119 | 116, 118 | sylan2 490 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
120 | | i1fima 23251 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ dom ∫1
→ (◡𝐺 “ {𝑧}) ∈ dom vol) |
121 | 6, 120 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐺 “ {𝑧}) ∈ dom vol) |
122 | 121 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ∈ dom vol) |
123 | | mblvol 23105 |
. . . . . . . . . . 11
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) |
124 | 122, 123 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) |
125 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → 𝐺 ∈ dom
∫1) |
126 | | i1fima2sn 23253 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
127 | 125, 126 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
128 | 124, 127 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
129 | | ovolsscl 23061 |
. . . . . . . . 9
⊢ ((((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) ∧ (◡𝐺 “ {𝑧}) ⊆ ℝ ∧ (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
130 | 115, 119,
128, 129 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
131 | 113, 130 | sylan2br 492 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 ≠ 0)) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
132 | 131 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑧 ≠ 0 → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
133 | 112, 132 | pm2.61dne 2868 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
134 | 57, 133 | fsumrecl 14312 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
135 | 56 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) = (vol*‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
136 | 114, 118 | syl5ss 3579 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) |
137 | 136, 133 | jca 553 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
138 | 137 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
∀𝑧 ∈ ran 𝐺(((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
139 | | ovolfiniun 23076 |
. . . . . 6
⊢ ((ran
𝐺 ∈ Fin ∧
∀𝑧 ∈ ran 𝐺(((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) →
(vol*‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
140 | 57, 138, 139 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol*‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
141 | 135, 140 | eqbrtrd 4605 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
142 | | ovollecl 23058 |
. . . 4
⊢ (((◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ⊆ ℝ ∧ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ ∧ (vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) → (vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) ∈ ℝ) |
143 | 89, 134, 141, 142 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) ∈ ℝ) |
144 | 87, 143 | eqeltrd 2688 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) ∈ ℝ) |
145 | 12, 49, 85, 144 | i1fd 23254 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ dom
∫1) |