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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑃 ‘ 𝑛 ) ∈ 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	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
34	33	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℂ )
35	34	fmpttd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) : ℕ ⟶ ℂ )
36	35	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ∈ ℂ )
37	7	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑄 ‘ 𝑛 ) ∈ dom ∫1 )
38		i1ff	⊢ ( ( 𝑄 ‘ 𝑛 ) ∈ dom ∫1 → ( 𝑄 ‘ 𝑛 ) : ℝ ⟶ ℝ )
39	37 38	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑄 ‘ 𝑛 ) : ℝ ⟶ ℝ )
40	39	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑄 ‘ 𝑛 ) : ℝ ⟶ ℝ )
41	40 32	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
42	41	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℂ )
43	42	fmpttd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) : ℕ ⟶ ℂ )
44	43	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑄 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑘 ) ∈ ℂ )
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 )