Step | Hyp | Ref
| Expression |
1 | | remulcl 10337 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
2 | 1 | adantl 475 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) |
3 | | i1fadd.1 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
4 | | i1ff 23842 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
6 | | i1fadd.2 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
7 | | i1ff 23842 |
. . . 4
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
8 | 6, 7 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
9 | | reex 10343 |
. . . 4
⊢ ℝ
∈ V |
10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ ∈
V) |
11 | | inidm 4047 |
. . 3
⊢ (ℝ
∩ ℝ) = ℝ |
12 | 2, 5, 8, 10, 10, 11 | off 7172 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺):ℝ⟶ℝ) |
13 | | i1frn 23843 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
14 | 3, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
15 | | i1frn 23843 |
. . . . . 6
⊢ (𝐺 ∈ dom ∫1
→ ran 𝐺 ∈
Fin) |
16 | 6, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
17 | | xpfi 8500 |
. . . . 5
⊢ ((ran
𝐹 ∈ Fin ∧ ran
𝐺 ∈ Fin) → (ran
𝐹 × ran 𝐺) ∈ Fin) |
18 | 14, 16, 17 | syl2anc 581 |
. . . 4
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin) |
19 | | eqid 2825 |
. . . . . 6
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) = (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) |
20 | | ovex 6937 |
. . . . . 6
⊢ (𝑢 · 𝑣) ∈ V |
21 | 19, 20 | fnmpt2i 7502 |
. . . . 5
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) Fn (ran 𝐹 × ran 𝐺) |
22 | | dffn4 6359 |
. . . . 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 8521 |
. . . 4
⊢ (((ran
𝐹 × ran 𝐺) ∈ Fin ∧ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣))) → ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) ∈ Fin) |
25 | 18, 23, 24 | sylancl 582 |
. . 3
⊢ (𝜑 → ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) ∈ Fin) |
26 | | eqid 2825 |
. . . . . . . . 9
⊢ (𝑥 · 𝑦) = (𝑥 · 𝑦) |
27 | | rspceov 6951 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ∧ (𝑥 · 𝑦) = (𝑥 · 𝑦)) → ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 · 𝑦) = (𝑢 · 𝑣)) |
28 | 26, 27 | mp3an3 1580 |
. . . . . . . 8
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 · 𝑦) = (𝑢 · 𝑣)) |
29 | | ovex 6937 |
. . . . . . . . 9
⊢ (𝑥 · 𝑦) ∈ V |
30 | | eqeq1 2829 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 · 𝑦) → (𝑤 = (𝑢 · 𝑣) ↔ (𝑥 · 𝑦) = (𝑢 · 𝑣))) |
31 | 30 | 2rexbidv 3267 |
. . . . . . . . 9
⊢ (𝑤 = (𝑥 · 𝑦) → (∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 · 𝑣) ↔ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 · 𝑦) = (𝑢 · 𝑣))) |
32 | 29, 31 | elab 3571 |
. . . . . . . 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 6279 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn ℝ) |
36 | | dffn3 6289 |
. . . . . . 7
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) |
37 | 35, 36 | sylib 210 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) |
38 | 8 | ffnd 6279 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn ℝ) |
39 | | dffn3 6289 |
. . . . . . 7
⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺) |
40 | 38, 39 | sylib 210 |
. . . . . 6
⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺) |
41 | 34, 37, 40, 10, 10, 11 | off 7172 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺):ℝ⟶{𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 · 𝑣)}) |
42 | 41 | frnd 6285 |
. . . 4
⊢ (𝜑 → ran (𝐹 ∘𝑓 · 𝐺) ⊆ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 · 𝑣)}) |
43 | 19 | rnmpt2 7030 |
. . . 4
⊢ ran
(𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) = {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 · 𝑣)} |
44 | 42, 43 | syl6sseqr 3877 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘𝑓 · 𝐺) ⊆ ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣))) |
45 | | ssfi 8449 |
. . 3
⊢ ((ran
(𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) ∈ Fin ∧ ran (𝐹 ∘𝑓 · 𝐺) ⊆ ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣))) → ran (𝐹 ∘𝑓 · 𝐺) ∈ Fin) |
46 | 25, 44, 45 | syl2anc 581 |
. 2
⊢ (𝜑 → ran (𝐹 ∘𝑓 · 𝐺) ∈ Fin) |
47 | 12 | frnd 6285 |
. . . . . . 7
⊢ (𝜑 → ran (𝐹 ∘𝑓 · 𝐺) ⊆
ℝ) |
48 | | ax-resscn 10309 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
49 | 47, 48 | syl6ss 3839 |
. . . . . 6
⊢ (𝜑 → ran (𝐹 ∘𝑓 · 𝐺) ⊆
ℂ) |
50 | 49 | ssdifd 3973 |
. . . . 5
⊢ (𝜑 → (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0}) ⊆ (ℂ
∖ {0})) |
51 | 50 | sselda 3827 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → 𝑦 ∈ (ℂ ∖
{0})) |
52 | 3, 6 | i1fmullem 23860 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {0})) → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) = ∪
𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
53 | 51, 52 | syldan 587 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) = ∪
𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
54 | | difss 3964 |
. . . . . 6
⊢ (ran
𝐺 ∖ {0}) ⊆ ran
𝐺 |
55 | | ssfi 8449 |
. . . . . 6
⊢ ((ran
𝐺 ∈ Fin ∧ (ran
𝐺 ∖ {0}) ⊆ ran
𝐺) → (ran 𝐺 ∖ {0}) ∈
Fin) |
56 | 16, 54, 55 | sylancl 582 |
. . . . 5
⊢ (𝜑 → (ran 𝐺 ∖ {0}) ∈ Fin) |
57 | | i1fima 23844 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {(𝑦 / 𝑧)}) ∈ dom vol) |
58 | 3, 57 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (◡𝐹 “ {(𝑦 / 𝑧)}) ∈ dom vol) |
59 | | i1fima 23844 |
. . . . . . . 8
⊢ (𝐺 ∈ dom ∫1
→ (◡𝐺 “ {𝑧}) ∈ dom vol) |
60 | 6, 59 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (◡𝐺 “ {𝑧}) ∈ dom vol) |
61 | | inmbl 23708 |
. . . . . . 7
⊢ (((◡𝐹 “ {(𝑦 / 𝑧)}) ∈ dom vol ∧ (◡𝐺 “ {𝑧}) ∈ dom vol) → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
62 | 58, 60, 61 | syl2anc 581 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
63 | 62 | ralrimivw 3176 |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
64 | | finiunmbl 23710 |
. . . . 5
⊢ (((ran
𝐺 ∖ {0}) ∈ Fin
∧ ∀𝑧 ∈ (ran
𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) → ∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
65 | 56, 63, 64 | syl2anc 581 |
. . . 4
⊢ (𝜑 → ∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
66 | 65 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → ∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
67 | 53, 66 | eqeltrd 2906 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ∈ dom vol) |
68 | | mblvol 23696 |
. . . 4
⊢ ((◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ∈ dom vol → (vol‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}))) |
69 | 67, 68 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}))) |
70 | | mblss 23697 |
. . . . 5
⊢ ((◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ∈ dom vol → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ⊆ ℝ) |
71 | 67, 70 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ⊆ ℝ) |
72 | 56 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → (ran
𝐺 ∖ {0}) ∈
Fin) |
73 | | inss2 4058 |
. . . . . . 7
⊢ ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) |
74 | 73 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧})) |
75 | 60 | ad2antrr 719 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ∈ dom vol) |
76 | | mblss 23697 |
. . . . . . 7
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
77 | 75, 76 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
78 | | mblvol 23696 |
. . . . . . . 8
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) |
79 | 75, 78 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) |
80 | 6 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → 𝐺 ∈ dom
∫1) |
81 | | i1fima2sn 23846 |
. . . . . . . 8
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
82 | 80, 81 | sylan 577 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
83 | 79, 82 | eqeltrrd 2907 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
84 | | ovolsscl 23652 |
. . . . . 6
⊢ ((((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) ∧ (◡𝐺 “ {𝑧}) ⊆ ℝ ∧ (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
85 | 74, 77, 83, 84 | syl3anc 1496 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
86 | 72, 85 | fsumrecl 14842 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
87 | 53 | fveq2d 6437 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) = (vol*‘∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
88 | | mblss 23697 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) |
89 | 62, 88 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) |
90 | 89 | ad2antrr 719 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) |
91 | 90, 85 | jca 509 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
92 | 91 | ralrimiva 3175 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
∀𝑧 ∈ (ran 𝐺 ∖ {0})(((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
93 | | ovolfiniun 23667 |
. . . . . 6
⊢ (((ran
𝐺 ∖ {0}) ∈ Fin
∧ ∀𝑧 ∈ (ran
𝐺 ∖ {0})(((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) →
(vol*‘∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
94 | 72, 92, 93 | syl2anc 581 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol*‘∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
95 | 87, 94 | eqbrtrd 4895 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
96 | | ovollecl 23649 |
. . . 4
⊢ (((◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ⊆ ℝ ∧ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ ∧ (vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) → (vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) ∈ ℝ) |
97 | 71, 86, 95, 96 | syl3anc 1496 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) ∈ ℝ) |
98 | 69, 97 | eqeltrd 2906 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) ∈ ℝ) |
99 | 12, 46, 67, 98 | i1fd 23847 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ dom
∫1) |