| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mbfmul.1 | . . 3
⊢ (𝜑 → 𝐹 ∈ MblFn) | 
| 2 |  | mbfmul.3 | . . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) | 
| 3 | 1, 2 | mbfi1flim 25758 | . 2
⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦))) | 
| 4 |  | mbfmul.2 | . . 3
⊢ (𝜑 → 𝐺 ∈ MblFn) | 
| 5 |  | mbfmul.4 | . . 3
⊢ (𝜑 → 𝐺:𝐴⟶ℝ) | 
| 6 | 4, 5 | mbfi1flim 25758 | . 2
⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦))) | 
| 7 |  | exdistrv 1955 | . . 3
⊢
(∃𝑓∃𝑔((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦))) ↔ (∃𝑓(𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) | 
| 8 | 1 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) → 𝐹 ∈ MblFn) | 
| 9 | 4 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) → 𝐺 ∈ MblFn) | 
| 10 | 2 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) → 𝐹:𝐴⟶ℝ) | 
| 11 | 5 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) → 𝐺:𝐴⟶ℝ) | 
| 12 |  | simprll 779 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) → 𝑓:ℕ⟶dom
∫1) | 
| 13 |  | simprlr 780 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) → ∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) | 
| 14 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((𝑓‘𝑛)‘𝑦) = ((𝑓‘𝑛)‘𝑥)) | 
| 15 | 14 | mpteq2dv 5244 | . . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) = (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥))) | 
| 16 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚)) | 
| 17 | 16 | fveq1d 6908 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → ((𝑓‘𝑛)‘𝑥) = ((𝑓‘𝑚)‘𝑥)) | 
| 18 | 17 | cbvmptv 5255 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑥)) = (𝑚 ∈ ℕ ↦ ((𝑓‘𝑚)‘𝑥)) | 
| 19 | 15, 18 | eqtrdi 2793 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑓‘𝑚)‘𝑥))) | 
| 20 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) | 
| 21 | 19, 20 | breq12d 5156 | . . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦) ↔ (𝑚 ∈ ℕ ↦ ((𝑓‘𝑚)‘𝑥)) ⇝ (𝐹‘𝑥))) | 
| 22 | 21 | rspccva 3621 | . . . . . . 7
⊢
((∀𝑦 ∈
𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑚 ∈ ℕ ↦ ((𝑓‘𝑚)‘𝑥)) ⇝ (𝐹‘𝑥)) | 
| 23 | 13, 22 | sylan 580 | . . . . . 6
⊢ (((𝜑 ∧ ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) ∧ 𝑥 ∈ 𝐴) → (𝑚 ∈ ℕ ↦ ((𝑓‘𝑚)‘𝑥)) ⇝ (𝐹‘𝑥)) | 
| 24 |  | simprrl 781 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) → 𝑔:ℕ⟶dom
∫1) | 
| 25 |  | simprrr 782 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) → ∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)) | 
| 26 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((𝑔‘𝑛)‘𝑦) = ((𝑔‘𝑛)‘𝑥)) | 
| 27 | 26 | mpteq2dv 5244 | . . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) = (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥))) | 
| 28 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚)) | 
| 29 | 28 | fveq1d 6908 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛)‘𝑥) = ((𝑔‘𝑚)‘𝑥)) | 
| 30 | 29 | cbvmptv 5255 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚)‘𝑥)) | 
| 31 | 27, 30 | eqtrdi 2793 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚)‘𝑥))) | 
| 32 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝐺‘𝑦) = (𝐺‘𝑥)) | 
| 33 | 31, 32 | breq12d 5156 | . . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦) ↔ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚)‘𝑥)) ⇝ (𝐺‘𝑥))) | 
| 34 | 33 | rspccva 3621 | . . . . . . 7
⊢
((∀𝑦 ∈
𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚)‘𝑥)) ⇝ (𝐺‘𝑥)) | 
| 35 | 25, 34 | sylan 580 | . . . . . 6
⊢ (((𝜑 ∧ ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) ∧ 𝑥 ∈ 𝐴) → (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚)‘𝑥)) ⇝ (𝐺‘𝑥)) | 
| 36 | 8, 9, 10, 11, 12, 23, 24, 35 | mbfmullem2 25759 | . . . . 5
⊢ ((𝜑 ∧ ((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦)))) → (𝐹 ∘f · 𝐺) ∈ MblFn) | 
| 37 | 36 | ex 412 | . . . 4
⊢ (𝜑 → (((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦))) → (𝐹 ∘f · 𝐺) ∈
MblFn)) | 
| 38 | 37 | exlimdvv 1934 | . . 3
⊢ (𝜑 → (∃𝑓∃𝑔((𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ (𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦))) → (𝐹 ∘f · 𝐺) ∈
MblFn)) | 
| 39 | 7, 38 | biimtrrid 243 | . 2
⊢ (𝜑 → ((∃𝑓(𝑓:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑓‘𝑛)‘𝑦)) ⇝ (𝐹‘𝑦)) ∧ ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑦 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑦)) ⇝ (𝐺‘𝑦))) → (𝐹 ∘f · 𝐺) ∈
MblFn)) | 
| 40 | 3, 6, 39 | mp2and 699 | 1
⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn) |