Metamath Proof Explorer

Theorem mbfmullem2

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

Ref Expression
Hypotheses mbfmul.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfmul.2 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
mbfmul.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
mbfmul.4 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℝ )
mbfmul.5 ⊢ ( 𝜑 → 𝑃 : ℕ ⟶ dom ∫1 )
mbfmul.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) )
mbfmul.7 ⊢ ( 𝜑 → 𝑄 : ℕ ⟶ dom ∫1 )
mbfmul.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) )
Assertion mbfmullem2 ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfmul.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 mbfmul.2 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
3 mbfmul.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
4 mbfmul.4 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℝ )
5 mbfmul.5 ⊢ ( 𝜑 → 𝑃 : ℕ ⟶ dom ∫1 )
6 mbfmul.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) )
7 mbfmul.7 ⊢ ( 𝜑 → 𝑄 : ℕ ⟶ dom ∫1 )
8 mbfmul.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐺 ‘ 𝑥 ) )
9 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
10 4 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
11 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
12 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
13 1 12 syl ⊢ ( 𝜑 → dom 𝐹 ∈ dom vol )
14 11 13 eqeltrrd ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
15 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
16 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
17 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
18 9 10 14 14 15 16 17 offval ⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
19 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
20 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
21 1zzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 1 ∈ ℤ )
22 nnex ⊢ ℕ ∈ V
23 22 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ∈ V
24 23 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ∈ V )
25 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑃 ‘ 𝑛 ) ∈ dom ∫1 )
26 i1ff ⊢ ( ( 𝑃 ‘ 𝑛 ) ∈ dom ∫1 → ( 𝑃 ‘ 𝑛 ) : ℝ ⟶ ℝ )
27 25 26 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑃 ‘ 𝑛 ) : ℝ ⟶ ℝ )
28 27 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 ‘ 𝑛 ) : ℝ ⟶ ℝ )
29 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
30 14 29 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
31 30 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
32 31 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ℝ )
33 28 32 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
34 33 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℂ )
35 34 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) : ℕ ⟶ ℂ )
36 35 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ∈ ℂ )
37 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑄 ‘ 𝑛 ) ∈ dom ∫1 )
38 i1ff ⊢ ( ( 𝑄 ‘ 𝑛 ) ∈ dom ∫1 → ( 𝑄 ‘ 𝑛 ) : ℝ ⟶ ℝ )
39 37 38 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑄 ‘ 𝑛 ) : ℝ ⟶ ℝ )
40 39 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑄 ‘ 𝑛 ) : ℝ ⟶ ℝ )
41 40 32 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
42 41 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℂ )
43 42 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) : ℕ ⟶ ℂ )
44 43 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ∈ ℂ )
45 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑃 ‘ 𝑛 ) = ( 𝑃 ‘ 𝑘 ) )
46 45 fveq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝑃 ‘ 𝑘 ) ‘ 𝑥 ) )
47 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑄 ‘ 𝑛 ) = ( 𝑄 ‘ 𝑘 ) )
48 47 fveq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝑄 ‘ 𝑘 ) ‘ 𝑥 ) )
49 46 48 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( ( ( 𝑃 ‘ 𝑘 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑘 ) ‘ 𝑥 ) ) )
50 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) )
51 ovex ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ V
52 49 50 51 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( ( 𝑃 ‘ 𝑘 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑘 ) ‘ 𝑥 ) ) )
53 52 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( ( 𝑃 ‘ 𝑘 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑘 ) ‘ 𝑥 ) ) )
54 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) )
55 fvex ⊢ ( ( 𝑃 ‘ 𝑘 ) ‘ 𝑥 ) ∈ V
56 46 54 55 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( 𝑃 ‘ 𝑘 ) ‘ 𝑥 ) )
57 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) )
58 fvex ⊢ ( ( 𝑄 ‘ 𝑘 ) ‘ 𝑥 ) ∈ V
59 48 57 58 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( 𝑄 ‘ 𝑘 ) ‘ 𝑥 ) )
60 56 59 oveq12d ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ) = ( ( ( 𝑃 ‘ 𝑘 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑘 ) ‘ 𝑥 ) ) )
61 60 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ) = ( ( ( 𝑃 ‘ 𝑘 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑘 ) ‘ 𝑥 ) ) )
62 53 61 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ) )
63 19 21 6 24 8 36 44 62 climmul ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ⇝ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
64 30 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
65 64 resmptd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑥 ∈ ℝ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) )
66 27 ffnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑃 ‘ 𝑛 ) Fn ℝ )
67 39 ffnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑄 ‘ 𝑛 ) Fn ℝ )
68 reex ⊢ ℝ ∈ V
69 68 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ℝ ∈ V )
70 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
71 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) )
72 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) )
73 66 67 69 69 70 71 72 offval ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑛 ) ∘f · ( 𝑄 ‘ 𝑛 ) ) = ( 𝑥 ∈ ℝ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) )
74 25 37 i1fmul ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑛 ) ∘f · ( 𝑄 ‘ 𝑛 ) ) ∈ dom ∫1 )
75 i1fmbf ⊢ ( ( ( 𝑃 ‘ 𝑛 ) ∘f · ( 𝑄 ‘ 𝑛 ) ) ∈ dom ∫1 → ( ( 𝑃 ‘ 𝑛 ) ∘f · ( 𝑄 ‘ 𝑛 ) ) ∈ MblFn )
76 74 75 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑛 ) ∘f · ( 𝑄 ‘ 𝑛 ) ) ∈ MblFn )
77 73 76 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ∈ MblFn )
78 14 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ dom vol )
79 mbfres ⊢ ( ( ( 𝑥 ∈ ℝ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ( 𝑥 ∈ ℝ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ↾ 𝐴 ) ∈ MblFn )
80 77 78 79 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑥 ∈ ℝ ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ↾ 𝐴 ) ∈ MblFn )
81 65 80 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ∈ 𝐴 ↦ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ) ∈ MblFn )
82 ovex ⊢ ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ V
83 82 a1i ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐴 ) ) → ( ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) · ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ V )
84 19 20 63 81 83 mbflim ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn )
85 18 84 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ MblFn )