bddmulibl

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

		Ref	Expression
	Assertion	bddmulibl	$⊢ (F \in MblFn \land G \in 𝐿^{1} \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F \times_{f} G \in 𝐿^{1}$

Proof

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

Metamath Proof Explorer

Theorem bddmulibl

Proof