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	syl5bir	⊢ ( 𝜑 → ( ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹 ‘ 𝑦 ) ) ∧ ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ MblFn ) )
40	5 6 39	mp2and	⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ MblFn )