Step | Hyp | Ref
| Expression |
1 | | mbfmul.3 |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
2 | | ffn 6045 |
. . . 4
⊢ (𝐹:𝐴⟶ℝ → 𝐹 Fn 𝐴) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝐴) |
4 | | mbfmul.4 |
. . . 4
⊢ (𝜑 → 𝐺:𝐴⟶ℝ) |
5 | | ffn 6045 |
. . . 4
⊢ (𝐺:𝐴⟶ℝ → 𝐺 Fn 𝐴) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 Fn 𝐴) |
7 | | fdm 6051 |
. . . . 5
⊢ (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴) |
8 | 1, 7 | syl 17 |
. . . 4
⊢ (𝜑 → dom 𝐹 = 𝐴) |
9 | | mbfmul.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ MblFn) |
10 | | mbfdm 23395 |
. . . . 5
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝜑 → dom 𝐹 ∈ dom vol) |
12 | 8, 11 | eqeltrrd 2702 |
. . 3
⊢ (𝜑 → 𝐴 ∈ dom vol) |
13 | | inidm 3822 |
. . 3
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
14 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
15 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
16 | 3, 6, 12, 12, 13, 14, 15 | offval 6904 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥) · (𝐺‘𝑥)))) |
17 | | nnuz 11723 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
18 | | 1zzd 11408 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
19 | | 1zzd 11408 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℤ) |
20 | | mbfmul.6 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
21 | | nnex 11026 |
. . . . . 6
⊢ ℕ
∈ V |
22 | 21 | mptex 6486 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥))) ∈ V |
23 | 22 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥))) ∈ V) |
24 | | mbfmul.8 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥)) |
25 | | mbfmul.5 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃:ℕ⟶dom
∫1) |
26 | 25 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑃‘𝑛) ∈ dom
∫1) |
27 | | i1ff 23443 |
. . . . . . . . . 10
⊢ ((𝑃‘𝑛) ∈ dom ∫1 → (𝑃‘𝑛):ℝ⟶ℝ) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑃‘𝑛):ℝ⟶ℝ) |
29 | 28 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) → (𝑃‘𝑛):ℝ⟶ℝ) |
30 | | mblss 23299 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
31 | 12, 30 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
32 | 31 | sselda 3603 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
33 | 32 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ) |
34 | 29, 33 | ffvelrnd 6360 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) → ((𝑃‘𝑛)‘𝑥) ∈ ℝ) |
35 | 34 | recnd 10068 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) → ((𝑃‘𝑛)‘𝑥) ∈ ℂ) |
36 | | eqid 2622 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) |
37 | 35, 36 | fmptd 6385 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)):ℕ⟶ℂ) |
38 | 37 | ffvelrnda 6359 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥))‘𝑘) ∈ ℂ) |
39 | | mbfmul.7 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄:ℕ⟶dom
∫1) |
40 | 39 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑄‘𝑛) ∈ dom
∫1) |
41 | | i1ff 23443 |
. . . . . . . . . 10
⊢ ((𝑄‘𝑛) ∈ dom ∫1 → (𝑄‘𝑛):ℝ⟶ℝ) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑄‘𝑛):ℝ⟶ℝ) |
43 | 42 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) → (𝑄‘𝑛):ℝ⟶ℝ) |
44 | 43, 33 | ffvelrnd 6360 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) → ((𝑄‘𝑛)‘𝑥) ∈ ℝ) |
45 | 44 | recnd 10068 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) → ((𝑄‘𝑛)‘𝑥) ∈ ℂ) |
46 | | eqid 2622 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) |
47 | 45, 46 | fmptd 6385 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)):ℕ⟶ℂ) |
48 | 47 | ffvelrnda 6359 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥))‘𝑘) ∈ ℂ) |
49 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (𝑃‘𝑛) = (𝑃‘𝑘)) |
50 | 49 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → ((𝑃‘𝑛)‘𝑥) = ((𝑃‘𝑘)‘𝑥)) |
51 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (𝑄‘𝑛) = (𝑄‘𝑘)) |
52 | 51 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → ((𝑄‘𝑛)‘𝑥) = ((𝑄‘𝑘)‘𝑥)) |
53 | 50, 52 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥)) = (((𝑃‘𝑘)‘𝑥) · ((𝑄‘𝑘)‘𝑥))) |
54 | | eqid 2622 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥))) = (𝑛 ∈ ℕ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥))) |
55 | | ovex 6678 |
. . . . . . 7
⊢ (((𝑃‘𝑘)‘𝑥) · ((𝑄‘𝑘)‘𝑥)) ∈ V |
56 | 53, 54, 55 | fvmpt 6282 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥)))‘𝑘) = (((𝑃‘𝑘)‘𝑥) · ((𝑄‘𝑘)‘𝑥))) |
57 | 56 | adantl 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥)))‘𝑘) = (((𝑃‘𝑘)‘𝑥) · ((𝑄‘𝑘)‘𝑥))) |
58 | | fvex 6201 |
. . . . . . . 8
⊢ ((𝑃‘𝑘)‘𝑥) ∈ V |
59 | 50, 36, 58 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥))‘𝑘) = ((𝑃‘𝑘)‘𝑥)) |
60 | | fvex 6201 |
. . . . . . . 8
⊢ ((𝑄‘𝑘)‘𝑥) ∈ V |
61 | 52, 46, 60 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥))‘𝑘) = ((𝑄‘𝑘)‘𝑥)) |
62 | 59, 61 | oveq12d 6668 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥))‘𝑘) · ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥))‘𝑘)) = (((𝑃‘𝑘)‘𝑥) · ((𝑄‘𝑘)‘𝑥))) |
63 | 62 | adantl 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥))‘𝑘) · ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥))‘𝑘)) = (((𝑃‘𝑘)‘𝑥) · ((𝑄‘𝑘)‘𝑥))) |
64 | 57, 63 | eqtr4d 2659 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥)))‘𝑘) = (((𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥))‘𝑘) · ((𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥))‘𝑘))) |
65 | 17, 19, 20, 23, 24, 38, 48, 64 | climmul 14363 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥))) ⇝ ((𝐹‘𝑥) · (𝐺‘𝑥))) |
66 | 31 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) |
67 | 66 | resmptd 5452 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥))) ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥)))) |
68 | | ffn 6045 |
. . . . . . . 8
⊢ ((𝑃‘𝑛):ℝ⟶ℝ → (𝑃‘𝑛) Fn ℝ) |
69 | 28, 68 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑃‘𝑛) Fn ℝ) |
70 | | ffn 6045 |
. . . . . . . 8
⊢ ((𝑄‘𝑛):ℝ⟶ℝ → (𝑄‘𝑛) Fn ℝ) |
71 | 42, 70 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑄‘𝑛) Fn ℝ) |
72 | | reex 10027 |
. . . . . . . 8
⊢ ℝ
∈ V |
73 | 72 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℝ ∈
V) |
74 | | inidm 3822 |
. . . . . . 7
⊢ (ℝ
∩ ℝ) = ℝ |
75 | | eqidd 2623 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑃‘𝑛)‘𝑥) = ((𝑃‘𝑛)‘𝑥)) |
76 | | eqidd 2623 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑄‘𝑛)‘𝑥) = ((𝑄‘𝑛)‘𝑥)) |
77 | 69, 71, 73, 73, 74, 75, 76 | offval 6904 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑃‘𝑛) ∘𝑓 · (𝑄‘𝑛)) = (𝑥 ∈ ℝ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥)))) |
78 | 26, 40 | i1fmul 23463 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑃‘𝑛) ∘𝑓 · (𝑄‘𝑛)) ∈ dom
∫1) |
79 | | i1fmbf 23442 |
. . . . . . 7
⊢ (((𝑃‘𝑛) ∘𝑓 · (𝑄‘𝑛)) ∈ dom ∫1 →
((𝑃‘𝑛) ∘𝑓
· (𝑄‘𝑛)) ∈
MblFn) |
80 | 78, 79 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑃‘𝑛) ∘𝑓 · (𝑄‘𝑛)) ∈ MblFn) |
81 | 77, 80 | eqeltrrd 2702 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ ℝ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥))) ∈ MblFn) |
82 | 12 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ dom vol) |
83 | | mbfres 23411 |
. . . . 5
⊢ (((𝑥 ∈ ℝ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥))) ∈ MblFn ∧ 𝐴 ∈ dom vol) → ((𝑥 ∈ ℝ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥))) ↾ 𝐴) ∈ MblFn) |
84 | 81, 82, 83 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ ℝ ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥))) ↾ 𝐴) ∈ MblFn) |
85 | 67, 84 | eqeltrrd 2702 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐴 ↦ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥))) ∈ MblFn) |
86 | | ovex 6678 |
. . . 4
⊢ (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥)) ∈ V |
87 | 86 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐴)) → (((𝑃‘𝑛)‘𝑥) · ((𝑄‘𝑛)‘𝑥)) ∈ V) |
88 | 17, 18, 65, 85, 87 | mbflim 23435 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) ∈ MblFn) |
89 | 16, 88 | eqeltrd 2701 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ MblFn) |