Step | Hyp | Ref
| Expression |
1 | | readdcl 10355 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ) |
2 | 1 | adantl 475 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ) |
3 | | i1fadd.1 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
4 | | i1ff 23880 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
6 | | i1fadd.2 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
7 | | i1ff 23880 |
. . . 4
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
8 | 6, 7 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
9 | | reex 10363 |
. . . 4
⊢ ℝ
∈ V |
10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ ∈
V) |
11 | | inidm 4042 |
. . 3
⊢ (ℝ
∩ ℝ) = ℝ |
12 | 2, 5, 8, 10, 10, 11 | off 7189 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):ℝ⟶ℝ) |
13 | | i1frn 23881 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
14 | 3, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
15 | | i1frn 23881 |
. . . . . 6
⊢ (𝐺 ∈ dom ∫1
→ ran 𝐺 ∈
Fin) |
16 | 6, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
17 | | xpfi 8519 |
. . . . 5
⊢ ((ran
𝐹 ∈ Fin ∧ ran
𝐺 ∈ Fin) → (ran
𝐹 × ran 𝐺) ∈ Fin) |
18 | 14, 16, 17 | syl2anc 579 |
. . . 4
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin) |
19 | | eqid 2777 |
. . . . . 6
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) = (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) |
20 | | ovex 6954 |
. . . . . 6
⊢ (𝑢 + 𝑣) ∈ V |
21 | 19, 20 | fnmpt2i 7519 |
. . . . 5
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) Fn (ran 𝐹 × ran 𝐺) |
22 | | dffn4 6372 |
. . . . 5
⊢ ((𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) Fn (ran 𝐹 × ran 𝐺) ↔ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))) |
23 | 21, 22 | mpbi 222 |
. . . 4
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) |
24 | | fofi 8540 |
. . . 4
⊢ (((ran
𝐹 × ran 𝐺) ∈ Fin ∧ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))) → ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) ∈ Fin) |
25 | 18, 23, 24 | sylancl 580 |
. . 3
⊢ (𝜑 → ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) ∈ Fin) |
26 | | eqid 2777 |
. . . . . . . . 9
⊢ (𝑥 + 𝑦) = (𝑥 + 𝑦) |
27 | | rspceov 6968 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ∧ (𝑥 + 𝑦) = (𝑥 + 𝑦)) → ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣)) |
28 | 26, 27 | mp3an3 1523 |
. . . . . . . 8
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣)) |
29 | | ovex 6954 |
. . . . . . . . 9
⊢ (𝑥 + 𝑦) ∈ V |
30 | | eqeq1 2781 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 + 𝑦) → (𝑤 = (𝑢 + 𝑣) ↔ (𝑥 + 𝑦) = (𝑢 + 𝑣))) |
31 | 30 | 2rexbidv 3241 |
. . . . . . . . 9
⊢ (𝑤 = (𝑥 + 𝑦) → (∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣) ↔ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣))) |
32 | 29, 31 | elab 3557 |
. . . . . . . 8
⊢ ((𝑥 + 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)} ↔ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣)) |
33 | 28, 32 | sylibr 226 |
. . . . . . 7
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → (𝑥 + 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}) |
34 | 33 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}) |
35 | 5 | ffnd 6292 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn ℝ) |
36 | | dffn3 6302 |
. . . . . . 7
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) |
37 | 35, 36 | sylib 210 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) |
38 | 8 | ffnd 6292 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn ℝ) |
39 | | dffn3 6302 |
. . . . . . 7
⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺) |
40 | 38, 39 | sylib 210 |
. . . . . 6
⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺) |
41 | 34, 37, 40, 10, 10, 11 | off 7189 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):ℝ⟶{𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}) |
42 | 41 | frnd 6298 |
. . . 4
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}) |
43 | 19 | rnmpt2 7047 |
. . . 4
⊢ ran
(𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) = {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)} |
44 | 42, 43 | syl6sseqr 3870 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))) |
45 | | ssfi 8468 |
. . 3
⊢ ((ran
(𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) ∈ Fin ∧ ran (𝐹 ∘𝑓 + 𝐺) ⊆ ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))) → ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin) |
46 | 25, 44, 45 | syl2anc 579 |
. 2
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin) |
47 | 12 | frnd 6298 |
. . . . . . 7
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆
ℝ) |
48 | 47 | ssdifssd 3970 |
. . . . . 6
⊢ (𝜑 → (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0}) ⊆
ℝ) |
49 | 48 | sselda 3820 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → 𝑦 ∈
ℝ) |
50 | 49 | recnd 10405 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → 𝑦 ∈
ℂ) |
51 | 3, 6 | i1faddlem 23897 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
52 | 50, 51 | syldan 585 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
53 | 16 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → ran 𝐺 ∈ Fin) |
54 | 3 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹 ∈ dom
∫1) |
55 | | i1fmbf 23879 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
MblFn) |
56 | 54, 55 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹 ∈ MblFn) |
57 | 5 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹:ℝ⟶ℝ) |
58 | 12 | ad2antrr 716 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝐹 ∘𝑓 + 𝐺):ℝ⟶ℝ) |
59 | 58 | frnd 6298 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ran (𝐹 ∘𝑓 + 𝐺) ⊆
ℝ) |
60 | | eldifi 3954 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0}) → 𝑦 ∈ ran (𝐹 ∘𝑓 + 𝐺)) |
61 | 60 | ad2antlr 717 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑦 ∈ ran (𝐹 ∘𝑓 + 𝐺)) |
62 | 59, 61 | sseldd 3821 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑦 ∈ ℝ) |
63 | 8 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → 𝐺:ℝ⟶ℝ) |
64 | 63 | frnd 6298 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → ran 𝐺 ⊆
ℝ) |
65 | 64 | sselda 3820 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ) |
66 | 62, 65 | resubcld 10803 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑦 − 𝑧) ∈ ℝ) |
67 | | mbfimasn 23836 |
. . . . . . 7
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧
(𝑦 − 𝑧) ∈ ℝ) → (◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol) |
68 | 56, 57, 66, 67 | syl3anc 1439 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol) |
69 | 6 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺 ∈ dom
∫1) |
70 | | i1fmbf 23879 |
. . . . . . . 8
⊢ (𝐺 ∈ dom ∫1
→ 𝐺 ∈
MblFn) |
71 | 69, 70 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺 ∈ MblFn) |
72 | 8 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺:ℝ⟶ℝ) |
73 | | mbfimasn 23836 |
. . . . . . 7
⊢ ((𝐺 ∈ MblFn ∧ 𝐺:ℝ⟶ℝ ∧
𝑧 ∈ ℝ) →
(◡𝐺 “ {𝑧}) ∈ dom vol) |
74 | 71, 72, 65, 73 | syl3anc 1439 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (◡𝐺 “ {𝑧}) ∈ dom vol) |
75 | | inmbl 23746 |
. . . . . 6
⊢ (((◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol ∧ (◡𝐺 “ {𝑧}) ∈ dom vol) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
76 | 68, 74, 75 | syl2anc 579 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
77 | 76 | ralrimiva 3147 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
∀𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
78 | | finiunmbl 23748 |
. . . 4
⊢ ((ran
𝐺 ∈ Fin ∧
∀𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) → ∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
79 | 53, 77, 78 | syl2anc 579 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → ∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
80 | 52, 79 | eqeltrd 2858 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ∈ dom vol) |
81 | | mblvol 23734 |
. . . 4
⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ∈ dom vol → (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}))) |
82 | 80, 81 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}))) |
83 | | mblss 23735 |
. . . . 5
⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ∈ dom vol → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ⊆ ℝ) |
84 | 80, 83 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ⊆ ℝ) |
85 | | inss1 4052 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {(𝑦 − 𝑧)}) |
86 | 85 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {(𝑦 − 𝑧)})) |
87 | 68 | adantrr 707 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol) |
88 | | mblss 23735 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol → (◡𝐹 “ {(𝑦 − 𝑧)}) ⊆ ℝ) |
89 | 87, 88 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (◡𝐹 “ {(𝑦 − 𝑧)}) ⊆ ℝ) |
90 | | mblvol 23734 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) = (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)}))) |
91 | 87, 90 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) = (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)}))) |
92 | | simprr 763 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → 𝑧 = 0) |
93 | 92 | oveq2d 6938 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (𝑦 − 𝑧) = (𝑦 − 0)) |
94 | 50 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → 𝑦 ∈ ℂ) |
95 | 94 | subid1d 10723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (𝑦 − 0) = 𝑦) |
96 | 93, 95 | eqtrd 2813 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (𝑦 − 𝑧) = 𝑦) |
97 | 96 | sneqd 4409 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → {(𝑦 − 𝑧)} = {𝑦}) |
98 | 97 | imaeq2d 5720 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (◡𝐹 “ {(𝑦 − 𝑧)}) = (◡𝐹 “ {𝑦})) |
99 | 98 | fveq2d 6450 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) = (vol‘(◡𝐹 “ {𝑦}))) |
100 | | i1fima2sn 23884 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 +
𝐺) ∖ {0})) →
(vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
101 | 3, 100 | sylan 575 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
102 | 101 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
103 | 99, 102 | eqeltrd 2858 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) ∈ ℝ) |
104 | 91, 103 | eqeltrrd 2859 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)})) ∈ ℝ) |
105 | | ovolsscl 23690 |
. . . . . . . 8
⊢ ((((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {(𝑦 − 𝑧)}) ∧ (◡𝐹 “ {(𝑦 − 𝑧)}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
106 | 86, 89, 104, 105 | syl3anc 1439 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
107 | 106 | expr 450 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑧 = 0 → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
108 | | eldifsn 4549 |
. . . . . . . 8
⊢ (𝑧 ∈ (ran 𝐺 ∖ {0}) ↔ (𝑧 ∈ ran 𝐺 ∧ 𝑧 ≠ 0)) |
109 | | inss2 4053 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) |
110 | 109 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧})) |
111 | | eldifi 3954 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (ran 𝐺 ∖ {0}) → 𝑧 ∈ ran 𝐺) |
112 | | mblss 23735 |
. . . . . . . . . . 11
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
113 | 74, 112 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
114 | 111, 113 | sylan2 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
115 | | i1fima 23882 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ dom ∫1
→ (◡𝐺 “ {𝑧}) ∈ dom vol) |
116 | 6, 115 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐺 “ {𝑧}) ∈ dom vol) |
117 | 116 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ∈ dom vol) |
118 | | mblvol 23734 |
. . . . . . . . . . 11
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) |
119 | 117, 118 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) |
120 | 6 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) → 𝐺 ∈ dom
∫1) |
121 | | i1fima2sn 23884 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
122 | 120, 121 | sylan 575 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
123 | 119, 122 | eqeltrrd 2859 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
124 | | ovolsscl 23690 |
. . . . . . . . 9
⊢ ((((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) ∧ (◡𝐺 “ {𝑧}) ⊆ ℝ ∧ (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
125 | 110, 114,
123, 124 | syl3anc 1439 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
126 | 108, 125 | sylan2br 588 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 ≠ 0)) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
127 | 126 | expr 450 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑧 ≠ 0 → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
128 | 107, 127 | pm2.61dne 3055 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
129 | 53, 128 | fsumrecl 14872 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
130 | 52 | fveq2d 6450 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) = (vol*‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
131 | 109, 113 | syl5ss 3831 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) |
132 | 131, 128 | jca 507 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
133 | 132 | ralrimiva 3147 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
∀𝑧 ∈ ran 𝐺(((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
134 | | ovolfiniun 23705 |
. . . . . 6
⊢ ((ran
𝐺 ∈ Fin ∧
∀𝑧 ∈ ran 𝐺(((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) →
(vol*‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
135 | 53, 133, 134 | syl2anc 579 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol*‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
136 | 130, 135 | eqbrtrd 4908 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
137 | | ovollecl 23687 |
. . . 4
⊢ (((◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦}) ⊆ ℝ ∧ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ ∧ (vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) → (vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) ∈ ℝ) |
138 | 84, 129, 136, 137 | syl3anc 1439 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) ∈ ℝ) |
139 | 82, 138 | eqeltrd 2858 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0})) →
(vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑦})) ∈ ℝ) |
140 | 12, 46, 80, 139 | i1fd 23885 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ dom
∫1) |