Step | Hyp | Ref
| Expression |
1 | | remulcl 9900 |
. . . 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 | | ax-resscn 9872 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
53 | 51, 52 | syl6ss 3580 |
. . . . . 6
⊢ (𝜑 → ran (𝐹 ∘𝑓 · 𝐺) ⊆
ℂ) |
54 | 53 | ssdifd 3708 |
. . . . 5
⊢ (𝜑 → (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0}) ⊆ (ℂ
∖ {0})) |
55 | 54 | sselda 3568 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → 𝑦 ∈ (ℂ ∖
{0})) |
56 | 3, 6 | i1fmullem 23267 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {0})) → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) = ∪
𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
57 | 55, 56 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) = ∪
𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
58 | | difss 3699 |
. . . . . 6
⊢ (ran
𝐺 ∖ {0}) ⊆ ran
𝐺 |
59 | | ssfi 8065 |
. . . . . 6
⊢ ((ran
𝐺 ∈ Fin ∧ (ran
𝐺 ∖ {0}) ⊆ ran
𝐺) → (ran 𝐺 ∖ {0}) ∈
Fin) |
60 | 16, 58, 59 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (ran 𝐺 ∖ {0}) ∈ Fin) |
61 | | i1fima 23251 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {(𝑦 / 𝑧)}) ∈ dom vol) |
62 | 3, 61 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (◡𝐹 “ {(𝑦 / 𝑧)}) ∈ dom vol) |
63 | | i1fima 23251 |
. . . . . . . 8
⊢ (𝐺 ∈ dom ∫1
→ (◡𝐺 “ {𝑧}) ∈ dom vol) |
64 | 6, 63 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (◡𝐺 “ {𝑧}) ∈ dom vol) |
65 | | inmbl 23117 |
. . . . . . 7
⊢ (((◡𝐹 “ {(𝑦 / 𝑧)}) ∈ dom vol ∧ (◡𝐺 “ {𝑧}) ∈ dom vol) → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
66 | 62, 64, 65 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
67 | 66 | ralrimivw 2950 |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
68 | | finiunmbl 23119 |
. . . . 5
⊢ (((ran
𝐺 ∖ {0}) ∈ Fin
∧ ∀𝑧 ∈ (ran
𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) → ∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
69 | 60, 67, 68 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
70 | 69 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → ∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
71 | 57, 70 | eqeltrd 2688 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ∈ dom vol) |
72 | | mblvol 23105 |
. . . 4
⊢ ((◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ∈ dom vol → (vol‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}))) |
73 | 71, 72 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}))) |
74 | | mblss 23106 |
. . . . 5
⊢ ((◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ∈ dom vol → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ⊆ ℝ) |
75 | 71, 74 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → (◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ⊆ ℝ) |
76 | 60 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → (ran
𝐺 ∖ {0}) ∈
Fin) |
77 | | inss2 3796 |
. . . . . . 7
⊢ ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) |
78 | 77 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧})) |
79 | 64 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ∈ dom vol) |
80 | | mblss 23106 |
. . . . . . 7
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
81 | 79, 80 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
82 | | mblvol 23105 |
. . . . . . . 8
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) |
83 | 79, 82 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) |
84 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) → 𝐺 ∈ dom
∫1) |
85 | | i1fima2sn 23253 |
. . . . . . . 8
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
86 | 84, 85 | sylan 487 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
87 | 83, 86 | eqeltrrd 2689 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
88 | | ovolsscl 23061 |
. . . . . 6
⊢ ((((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) ∧ (◡𝐺 “ {𝑧}) ⊆ ℝ ∧ (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
89 | 78, 81, 87, 88 | syl3anc 1318 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
90 | 76, 89 | fsumrecl 14312 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
91 | 57 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) = (vol*‘∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
92 | | mblss 23106 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) |
93 | 66, 92 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) |
94 | 93 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) |
95 | 94, 89 | jca 553 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
96 | 95 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
∀𝑧 ∈ (ran 𝐺 ∖ {0})(((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
97 | | ovolfiniun 23076 |
. . . . . 6
⊢ (((ran
𝐺 ∖ {0}) ∈ Fin
∧ ∀𝑧 ∈ (ran
𝐺 ∖ {0})(((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) →
(vol*‘∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
98 | 76, 96, 97 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol*‘∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
99 | 91, 98 | eqbrtrd 4605 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
100 | | ovollecl 23058 |
. . . 4
⊢ (((◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦}) ⊆ ℝ ∧ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ ∧ (vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) → (vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) ∈ ℝ) |
101 | 75, 90, 99, 100 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) ∈ ℝ) |
102 | 73, 101 | eqeltrd 2688 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘𝑓 · 𝐺) ∖ {0})) →
(vol‘(◡(𝐹 ∘𝑓 · 𝐺) “ {𝑦})) ∈ ℝ) |
103 | 12, 49, 71, 102 | i1fd 23254 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ dom
∫1) |