Metamath Proof Explorer

Theorem mbfmullem

Description: Lemma for mbfmul . (Contributed by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses mbfmul.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfmul.2 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
mbfmul.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
mbfmul.4 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℝ )
Assertion mbfmullem ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ MblFn )

Proof

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