Theorem bddmulibl

Description: A bounded function times an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

	Ref	Expression
Assertion	bddmulibl	⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝐿1 )

Proof

Step	Hyp	Ref	Expression
1		mbff	⊢ ( 𝐹 ∈ MblFn → 𝐹 : dom 𝐹 ⟶ ℂ )
2	1	ad2antrr	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
3	2	ffnd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐹 Fn dom 𝐹 )
4		iblmbf	⊢ ( 𝐺 ∈ 𝐿1 → 𝐺 ∈ MblFn )
5	4	ad2antlr	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐺 ∈ MblFn )
6		mbff	⊢ ( 𝐺 ∈ MblFn → 𝐺 : dom 𝐺 ⟶ ℂ )
7	5 6	syl	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐺 : dom 𝐺 ⟶ ℂ )
8	7	ffnd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐺 Fn dom 𝐺 )
9		mbfdm	⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
10	9	ad2antrr	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → dom 𝐹 ∈ dom vol )
11		mbfdm	⊢ ( 𝐺 ∈ MblFn → dom 𝐺 ∈ dom vol )
12	5 11	syl	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → dom 𝐺 ∈ dom vol )
13		eqid	⊢ ( dom 𝐹 ∩ dom 𝐺 ) = ( dom 𝐹 ∩ dom 𝐺 )
14		eqidd	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
15		eqidd	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
16	3 8 10 12 13 14 15	offval	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝐹 ∘f · 𝐺 ) = ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) )
17		ovexd	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ∈ V )
18		simpll	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐹 ∈ MblFn )
19	18 5	mbfmul	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ MblFn )
20	16 19	eqeltrrd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ MblFn )
21		absf	⊢ abs : ℂ ⟶ ℝ
22	21	a1i	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → abs : ℂ ⟶ ℝ )
23	20 17	mbfmptcl	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
24	22 23	cofmpt	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( abs ∘ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) )
25	23	fmpttd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℂ )
26		ax-resscn	⊢ ℝ ⊆ ℂ
27		ssid	⊢ ℂ ⊆ ℂ
28		cncfss	⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ ) )
29	26 27 28	mp2an	⊢ ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ )
30		abscncf	⊢ abs ∈ ( ℂ –cn→ ℝ )
31	29 30	sselii	⊢ abs ∈ ( ℂ –cn→ ℂ )
32	31	a1i	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → abs ∈ ( ℂ –cn→ ℂ ) )
33		cncombf	⊢ ( ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ MblFn ∧ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℂ ∧ abs ∈ ( ℂ –cn→ ℂ ) ) → ( abs ∘ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ MblFn )
34	20 25 32 33	syl3anc	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( abs ∘ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ MblFn )
35	24 34	eqeltrrd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ MblFn )
36	23	abscld	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ )
37	36	rexrd	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ* )
38	23	absge0d	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) )
39		elxrge0	⊢ ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) )
40	37 38 39	sylanbrc	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( 0 [,] +∞ ) )
41		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
42	41	a1i	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ∈ ( 0 [,] +∞ ) )
43	40 42	ifclda	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
44	43	adantr	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ℝ ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
45	44	fmpttd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
46		reex	⊢ ℝ ∈ V
47	46	a1i	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ℝ ∈ V )
48		simprl	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
49	48	ad2antrr	⊢ ( ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) ∧ 𝑧 ∈ ℝ ) → 𝑥 ∈ ℝ )
50		elinel2	⊢ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑧 ∈ dom 𝐺 )
51		ffvelrn	⊢ ( ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ 𝑧 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
52	7 50 51	syl2an	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
53	52	abscld	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ )
54	52	absge0d	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) )
55		elrege0	⊢ ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
56	53 54 55	sylanbrc	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( 0 [,) +∞ ) )
57		0e0icopnf	⊢ 0 ∈ ( 0 [,) +∞ )
58	57	a1i	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ∈ ( 0 [,) +∞ ) )
59	56 58	ifclda	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
60	59	ad2antrr	⊢ ( ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) ∧ 𝑧 ∈ ℝ ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
61		fconstmpt	⊢ ( ℝ × { 𝑥 } ) = ( 𝑧 ∈ ℝ ↦ 𝑥 )
62	61	a1i	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ℝ × { 𝑥 } ) = ( 𝑧 ∈ ℝ ↦ 𝑥 ) )
63		eqidd	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) = ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) )
64	47 49 60 62 63	offval2	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( ℝ × { 𝑥 } ) ∘f · ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) = ( 𝑧 ∈ ℝ ↦ ( 𝑥 · if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) )
65		ovif2	⊢ ( 𝑥 · if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) = if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , ( 𝑥 · 0 ) )
66	48	recnd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝑥 ∈ ℂ )
67	66	adantr	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → 𝑥 ∈ ℂ )
68	67	mul01d	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑥 · 0 ) = 0 )
69	68	ifeq2d	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , ( 𝑥 · 0 ) ) = if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
70	65 69	eqtrid	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑥 · if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) = if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
71	70	mpteq2dv	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑧 ∈ ℝ ↦ ( 𝑥 · if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) = ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
72	64 71	eqtrd	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( ℝ × { 𝑥 } ) ∘f · ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) = ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
73	72	fveq2d	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ∫2 ‘ ( ( ℝ × { 𝑥 } ) ∘f · ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ) = ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) )
74	59	adantr	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ℝ ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
75	74	fmpttd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
76	75	adantr	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
77		inss2	⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺
78	77	a1i	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺 )
79	20 17	mbfdm2	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol )
80	7	ffvelrnda	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
81	7	feqmptd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐺 = ( 𝑧 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑧 ) ) )
82		simplr	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐺 ∈ 𝐿1 )
83	81 82	eqeltrrd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ 𝐿1 )
84	78 79 80 83	iblss	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ 𝐿1 )
85	52 84	iblabs	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ 𝐿1 )
86	53 54	iblpos	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ 𝐿1 ↔ ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ∈ ℝ ) ) )
87	85 86	mpbid	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ∈ ℝ ) )
88	87	simprd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ∈ ℝ )
89	88	adantr	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ∈ ℝ )
90		simplrl	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → 𝑥 ∈ ℝ )
91		neq0	⊢ ( ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ↔ ∃ 𝑧 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) )
92		0re	⊢ 0 ∈ ℝ
93	92	a1i	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ∈ ℝ )
94		elinel1	⊢ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑧 ∈ dom 𝐹 )
95		ffvelrn	⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
96	2 94 95	syl2an	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
97	96	abscld	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
98		simplrl	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 𝑥 ∈ ℝ )
99	96	absge0d	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
100		simprr	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
101		2fveq3	⊢ ( 𝑦 = 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
102	101	breq1d	⊢ ( 𝑦 = 𝑧 → ( ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ↔ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑥 ) )
103	102	rspccva	⊢ ( ( ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ∧ 𝑧 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑥 )
104	100 94 103	syl2an	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑥 )
105	93 97 98 99 104	letrd	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ≤ 𝑥 )
106	105	ex	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 0 ≤ 𝑥 ) )
107	106	exlimdv	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ∃ 𝑧 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 0 ≤ 𝑥 ) )
108	91 107	syl5bi	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → 0 ≤ 𝑥 ) )
109	108	imp	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → 0 ≤ 𝑥 )
110		elrege0	⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
111	90 109 110	sylanbrc	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → 𝑥 ∈ ( 0 [,) +∞ ) )
112	76 89 111	itg2mulc	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ∫2 ‘ ( ( ℝ × { 𝑥 } ) ∘f · ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ) = ( 𝑥 · ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ) )
113	73 112	eqtr3d	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) = ( 𝑥 · ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ) )
114	90 89	remulcld	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑥 · ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ) ∈ ℝ )
115	113 114	eqeltrd	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ )
116	115	ex	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ ) )
117		noel	⊢ ¬ 𝑧 ∈ ∅
118		eleq2	⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↔ 𝑧 ∈ ∅ ) )
119	117 118	mtbiri	⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) )
120		iffalse	⊢ ( ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = 0 )
121	119 120	syl	⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = 0 )
122	121	mpteq2dv	⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) = ( 𝑧 ∈ ℝ ↦ 0 ) )
123		fconstmpt	⊢ ( ℝ × { 0 } ) = ( 𝑧 ∈ ℝ ↦ 0 )
124	122 123	eqtr4di	⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) = ( ℝ × { 0 } ) )
125	124	fveq2d	⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( ℝ × { 0 } ) ) )
126		itg20	⊢ ( ∫2 ‘ ( ℝ × { 0 } ) ) = 0
127	126 92	eqeltri	⊢ ( ∫2 ‘ ( ℝ × { 0 } ) ) ∈ ℝ
128	125 127	eqeltrdi	⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ )
129	116 128	pm2.61d2	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ )
130	98 53	remulcld	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ )
131	130	rexrd	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ* )
132	98 53 105 54	mulge0d	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ≤ ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
133		elxrge0	⊢ ( ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ* ∧ 0 ≤ ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) )
134	131 132 133	sylanbrc	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( 0 [,] +∞ ) )
135	134 42	ifclda	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
136	135	adantr	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ℝ ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
137	136	fmpttd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
138	96 52	absmuld	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
139		abscl	⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ ℂ → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ )
140		absge0	⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ ℂ → 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) )
141	139 140	jca	⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ ℂ → ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
142	52 141	syl	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
143		lemul1a	⊢ ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ≤ ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
144	97 98 142 104 143	syl31anc	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ≤ ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
145	138 144	eqbrtrd	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ≤ ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
146		iftrue	⊢ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) )
147	146	adantl	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) )
148		iftrue	⊢ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
149	148	adantl	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
150	145 147 149	3brtr4d	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
151		0le0	⊢ 0 ≤ 0
152	151	a1i	⊢ ( ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 0 ≤ 0 )
153		iffalse	⊢ ( ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = 0 )
154	152 153 120	3brtr4d	⊢ ( ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
155	154	adantl	⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
156	150 155	pm2.61dan	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
157	156	ralrimivw	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ∀ 𝑧 ∈ ℝ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
158	46	a1i	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ℝ ∈ V )
159		eqidd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) = ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
160		eqidd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) = ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
161	158 44 136 159 160	ofrfval2	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ∘r ≤ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ↔ ∀ 𝑧 ∈ ℝ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
162	157 161	mpbird	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ∘r ≤ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
163		itg2le	⊢ ( ( ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ∘r ≤ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) )
164	45 137 162 163	syl3anc	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) )
165		itg2lecl	⊢ ( ( ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ )
166	45 129 164 165	syl3anc	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ )
167	36 38	iblpos	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ 𝐿1 ↔ ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
168	35 166 167	mpbir2and	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ 𝐿1 )
169	17 20 168	iblabsr	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ 𝐿1 )
170	16 169	eqeltrd	⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝐿1 )
171	170	rexlimdvaa	⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 → ( 𝐹 ∘f · 𝐺 ) ∈ 𝐿1 ) )
172	171	3impia	⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝐿1 )