iblabs

Description: The absolute value of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypotheses	iblabs.1	$⊢ (φ \land x \in A) \to B \in V$
	iblabs.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
Assertion	iblabs	$⊢ φ \to (x \in A ⟼ \|B\|) \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		iblabs.1	$⊢ (φ \land x \in A) \to B \in V$
2		iblabs.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
3		absf	$⊢ abs : ℂ ⟶ ℝ$
4	3	a1i	$⊢ φ \to abs : ℂ ⟶ ℝ$
5		iblmbf	$⊢ (x \in A ⟼ B) \in 𝐿^{1} \to (x \in A ⟼ B) \in MblFn$
6	2 5	syl	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
7	6 1	mbfmptcl	$⊢ (φ \land x \in A) \to B \in ℂ$
8	4 7	cofmpt	$⊢ φ \to abs \circ (x \in A ⟼ B) = (x \in A ⟼ \|B\|)$
9	7	fmpttd	$⊢ φ \to (x \in A ⟼ B) : A ⟶ ℂ$
10		ax-resscn	$⊢ ℝ \subseteq ℂ$
11		ssid	$⊢ ℂ \subseteq ℂ$
12		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to ℂ \underset{cn}{⟶} ℝ \subseteq ℂ \underset{cn}{⟶} ℂ$
13	10 11 12	mp2an	$⊢ ℂ \underset{cn}{⟶} ℝ \subseteq ℂ \underset{cn}{⟶} ℂ$
14		abscncf	$⊢ abs : ℂ \underset{cn}{⟶} ℝ$
15	13 14	sselii	$⊢ abs : ℂ \underset{cn}{⟶} ℂ$
16	15	a1i	$⊢ φ \to abs : ℂ \underset{cn}{⟶} ℂ$
17		cncombf	$⊢ ((x \in A ⟼ B) \in MblFn \land (x \in A ⟼ B) : A ⟶ ℂ \land abs : ℂ \underset{cn}{⟶} ℂ) \to abs \circ (x \in A ⟼ B) \in MblFn$
18	6 9 16 17	syl3anc	$⊢ φ \to abs \circ (x \in A ⟼ B) \in MblFn$
19	8 18	eqeltrrd	$⊢ φ \to (x \in A ⟼ \|B\|) \in MblFn$
20	7	abscld	$⊢ (φ \land x \in A) \to \|B\| \in ℝ$
21	20	rexrd	$⊢ (φ \land x \in A) \to \|B\| \in ℝ^{*}$
22	7	absge0d	$⊢ (φ \land x \in A) \to 0 \leq \|B\|$
23		elxrge0	$⊢ \|B\| \in [0, +∞] \leftrightarrow (\|B\| \in ℝ^{*} \land 0 \leq \|B\|)$
24	21 22 23	sylanbrc	$⊢ (φ \land x \in A) \to \|B\| \in [0, +∞]$
25		0e0iccpnf	$⊢ 0 \in [0, +∞]$
26	25	a1i	$⊢ (φ \land \neg x \in A) \to 0 \in [0, +∞]$
27	24 26	ifclda	$⊢ φ \to if (x \in A, \|B\|, 0) \in [0, +∞]$
28	27	adantr	$⊢ (φ \land x \in ℝ) \to if (x \in A, \|B\|, 0) \in [0, +∞]$
29	28	fmpttd	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|B\|, 0)) : ℝ ⟶ [0, +∞]$
30		reex	$⊢ ℝ \in V$
31	30	a1i	$⊢ φ \to ℝ \in V$
32	7	recld	$⊢ (φ \land x \in A) \to ℜ (B) \in ℝ$
33	32	recnd	$⊢ (φ \land x \in A) \to ℜ (B) \in ℂ$
34	33	abscld	$⊢ (φ \land x \in A) \to \|ℜ (B)\| \in ℝ$
35	33	absge0d	$⊢ (φ \land x \in A) \to 0 \leq \|ℜ (B)\|$
36		elrege0	$⊢ \|ℜ (B)\| \in [0, +∞) \leftrightarrow (\|ℜ (B)\| \in ℝ \land 0 \leq \|ℜ (B)\|)$
37	34 35 36	sylanbrc	$⊢ (φ \land x \in A) \to \|ℜ (B)\| \in [0, +∞)$
38		0e0icopnf	$⊢ 0 \in [0, +∞)$
39	38	a1i	$⊢ (φ \land \neg x \in A) \to 0 \in [0, +∞)$
40	37 39	ifclda	$⊢ φ \to if (x \in A, \|ℜ (B)\|, 0) \in [0, +∞)$
41	40	adantr	$⊢ (φ \land x \in ℝ) \to if (x \in A, \|ℜ (B)\|, 0) \in [0, +∞)$
42	7	imcld	$⊢ (φ \land x \in A) \to ℑ (B) \in ℝ$
43	42	recnd	$⊢ (φ \land x \in A) \to ℑ (B) \in ℂ$
44	43	abscld	$⊢ (φ \land x \in A) \to \|ℑ (B)\| \in ℝ$
45	43	absge0d	$⊢ (φ \land x \in A) \to 0 \leq \|ℑ (B)\|$
46		elrege0	$⊢ \|ℑ (B)\| \in [0, +∞) \leftrightarrow (\|ℑ (B)\| \in ℝ \land 0 \leq \|ℑ (B)\|)$
47	44 45 46	sylanbrc	$⊢ (φ \land x \in A) \to \|ℑ (B)\| \in [0, +∞)$
48	47 39	ifclda	$⊢ φ \to if (x \in A, \|ℑ (B)\|, 0) \in [0, +∞)$
49	48	adantr	$⊢ (φ \land x \in ℝ) \to if (x \in A, \|ℑ (B)\|, 0) \in [0, +∞)$
50		eqidd	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0)) = (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0))$
51		eqidd	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0)) = (x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0))$
52	31 41 49 50 51	offval2	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0)) +_{f} (x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0)) = (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0) + if (x \in A, \|ℑ (B)\|, 0))$
53		iftrue	$⊢ x \in A \to if (x \in A, \|ℜ (B)\|, 0) = \|ℜ (B)\|$
54		iftrue	$⊢ x \in A \to if (x \in A, \|ℑ (B)\|, 0) = \|ℑ (B)\|$
55	53 54	oveq12d	$⊢ x \in A \to if (x \in A, \|ℜ (B)\|, 0) + if (x \in A, \|ℑ (B)\|, 0) = \|ℜ (B)\| + \|ℑ (B)\|$
56		iftrue	$⊢ x \in A \to if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0) = \|ℜ (B)\| + \|ℑ (B)\|$
57	55 56	eqtr4d	$⊢ x \in A \to if (x \in A, \|ℜ (B)\|, 0) + if (x \in A, \|ℑ (B)\|, 0) = if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)$
58		00id	$⊢ 0 + 0 = 0$
59		iffalse	$⊢ \neg x \in A \to if (x \in A, \|ℜ (B)\|, 0) = 0$
60		iffalse	$⊢ \neg x \in A \to if (x \in A, \|ℑ (B)\|, 0) = 0$
61	59 60	oveq12d	$⊢ \neg x \in A \to if (x \in A, \|ℜ (B)\|, 0) + if (x \in A, \|ℑ (B)\|, 0) = 0 + 0$
62		iffalse	$⊢ \neg x \in A \to if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0) = 0$
63	58 61 62	3eqtr4a	$⊢ \neg x \in A \to if (x \in A, \|ℜ (B)\|, 0) + if (x \in A, \|ℑ (B)\|, 0) = if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)$
64	57 63	pm2.61i	$⊢ if (x \in A, \|ℜ (B)\|, 0) + if (x \in A, \|ℑ (B)\|, 0) = if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)$
65	64	mpteq2i	$⊢ (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0) + if (x \in A, \|ℑ (B)\|, 0)) = (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0))$
66	52 65	eqtr2di	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)) = (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0)) +_{f} (x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0))$
67	66	fveq2d	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0))) = \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0)) +_{f} (x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0)))$
68		eqid	$⊢ (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0)) = (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0))$
69	7	iblcn	$⊢ φ \to ((x \in A ⟼ B) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1}))$
70	2 69	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1})$
71	70	simpld	$⊢ φ \to (x \in A ⟼ ℜ (B)) \in 𝐿^{1}$
72	1 2 68 71 32	iblabslem	$⊢ φ \to ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0)) \in MblFn \land \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0))) \in ℝ)$
73	72	simpld	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0)) \in MblFn$
74	41	fmpttd	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0)) : ℝ ⟶ [0, +∞)$
75	72	simprd	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0))) \in ℝ$
76		eqid	$⊢ (x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0)) = (x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0))$
77	70	simprd	$⊢ φ \to (x \in A ⟼ ℑ (B)) \in 𝐿^{1}$
78	1 2 76 77 42	iblabslem	$⊢ φ \to ((x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0)) \in MblFn \land \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0))) \in ℝ)$
79	78	simpld	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0)) \in MblFn$
80	49	fmpttd	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0)) : ℝ ⟶ [0, +∞)$
81	78	simprd	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0))) \in ℝ$
82	73 74 75 79 80 81	itg2add	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0)) +_{f} (x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0))) = \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0))) + \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0)))$
83	67 82	eqtrd	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0))) = \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0))) + \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0)))$
84	75 81	readdcld	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\|, 0))) + \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℑ (B)\|, 0))) \in ℝ$
85	83 84	eqeltrd	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0))) \in ℝ$
86	34 44	readdcld	$⊢ (φ \land x \in A) \to \|ℜ (B)\| + \|ℑ (B)\| \in ℝ$
87	86	rexrd	$⊢ (φ \land x \in A) \to \|ℜ (B)\| + \|ℑ (B)\| \in ℝ^{*}$
88	34 44 35 45	addge0d	$⊢ (φ \land x \in A) \to 0 \leq \|ℜ (B)\| + \|ℑ (B)\|$
89		elxrge0	$⊢ \|ℜ (B)\| + \|ℑ (B)\| \in [0, +∞] \leftrightarrow (\|ℜ (B)\| + \|ℑ (B)\| \in ℝ^{*} \land 0 \leq \|ℜ (B)\| + \|ℑ (B)\|)$
90	87 88 89	sylanbrc	$⊢ (φ \land x \in A) \to \|ℜ (B)\| + \|ℑ (B)\| \in [0, +∞]$
91	90 26	ifclda	$⊢ φ \to if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0) \in [0, +∞]$
92	91	adantr	$⊢ (φ \land x \in ℝ) \to if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0) \in [0, +∞]$
93	92	fmpttd	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)) : ℝ ⟶ [0, +∞]$
94		ax-icn	$⊢ i \in ℂ$
95		mulcl	$⊢ (i \in ℂ \land ℑ (B) \in ℂ) \to i ℑ (B) \in ℂ$
96	94 43 95	sylancr	$⊢ (φ \land x \in A) \to i ℑ (B) \in ℂ$
97	33 96	abstrid	$⊢ (φ \land x \in A) \to \|ℜ (B) + i ℑ (B)\| \leq \|ℜ (B)\| + \|i ℑ (B)\|$
98	7	replimd	$⊢ (φ \land x \in A) \to B = ℜ (B) + i ℑ (B)$
99	98	fveq2d	$⊢ (φ \land x \in A) \to \|B\| = \|ℜ (B) + i ℑ (B)\|$
100		absmul	$⊢ (i \in ℂ \land ℑ (B) \in ℂ) \to \|i ℑ (B)\| = \|i\| \|ℑ (B)\|$
101	94 43 100	sylancr	$⊢ (φ \land x \in A) \to \|i ℑ (B)\| = \|i\| \|ℑ (B)\|$
102		absi	$⊢ \|i\| = 1$
103	102	oveq1i	$⊢ \|i\| \|ℑ (B)\| = 1 \|ℑ (B)\|$
104	44	recnd	$⊢ (φ \land x \in A) \to \|ℑ (B)\| \in ℂ$
105	104	mulid2d	$⊢ (φ \land x \in A) \to 1 \|ℑ (B)\| = \|ℑ (B)\|$
106	103 105	syl5eq	$⊢ (φ \land x \in A) \to \|i\| \|ℑ (B)\| = \|ℑ (B)\|$
107	101 106	eqtr2d	$⊢ (φ \land x \in A) \to \|ℑ (B)\| = \|i ℑ (B)\|$
108	107	oveq2d	$⊢ (φ \land x \in A) \to \|ℜ (B)\| + \|ℑ (B)\| = \|ℜ (B)\| + \|i ℑ (B)\|$
109	97 99 108	3brtr4d	$⊢ (φ \land x \in A) \to \|B\| \leq \|ℜ (B)\| + \|ℑ (B)\|$
110		iftrue	$⊢ x \in A \to if (x \in A, \|B\|, 0) = \|B\|$
111	110	adantl	$⊢ (φ \land x \in A) \to if (x \in A, \|B\|, 0) = \|B\|$
112	56	adantl	$⊢ (φ \land x \in A) \to if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0) = \|ℜ (B)\| + \|ℑ (B)\|$
113	109 111 112	3brtr4d	$⊢ (φ \land x \in A) \to if (x \in A, \|B\|, 0) \leq if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)$
114	113	ex	$⊢ φ \to (x \in A \to if (x \in A, \|B\|, 0) \leq if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0))$
115		0le0	$⊢ 0 \leq 0$
116	115	a1i	$⊢ \neg x \in A \to 0 \leq 0$
117		iffalse	$⊢ \neg x \in A \to if (x \in A, \|B\|, 0) = 0$
118	116 117 62	3brtr4d	$⊢ \neg x \in A \to if (x \in A, \|B\|, 0) \leq if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)$
119	114 118	pm2.61d1	$⊢ φ \to if (x \in A, \|B\|, 0) \leq if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)$
120	119	ralrimivw	$⊢ φ \to \forall x \in ℝ if (x \in A, \|B\|, 0) \leq if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)$
121		eqidd	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|B\|, 0)) = (x \in ℝ ⟼ if (x \in A, \|B\|, 0))$
122		eqidd	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)) = (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0))$
123	31 28 92 121 122	ofrfval2	$⊢ φ \to ((x \in ℝ ⟼ if (x \in A, \|B\|, 0)) \leq_{f} (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)) \leftrightarrow \forall x \in ℝ if (x \in A, \|B\|, 0) \leq if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0))$
124	120 123	mpbird	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, \|B\|, 0)) \leq_{f} (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0))$
125		itg2le	$⊢ ((x \in ℝ ⟼ if (x \in A, \|B\|, 0)) : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)) : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in A, \|B\|, 0)) \leq_{f} (x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0))) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, \|B\|, 0))) \leq \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)))$
126	29 93 124 125	syl3anc	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if (x \in A, \|B\|, 0))) \leq \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)))$
127		itg2lecl	$⊢ ((x \in ℝ ⟼ if (x \in A, \|B\|, 0)) : ℝ ⟶ [0, +∞] \land \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if (x \in A, \|B\|, 0))) \leq \int^{2} ((x \in ℝ ⟼ if (x \in A, \|ℜ (B)\| + \|ℑ (B)\|, 0)))) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, \|B\|, 0))) \in ℝ$
128	29 85 126 127	syl3anc	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if (x \in A, \|B\|, 0))) \in ℝ$
129	20 22	iblpos	$⊢ φ \to ((x \in A ⟼ \|B\|) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ \|B\|) \in MblFn \land \int^{2} ((x \in ℝ ⟼ if (x \in A, \|B\|, 0))) \in ℝ))$
130	19 128 129	mpbir2and	$⊢ φ \to (x \in A ⟼ \|B\|) \in 𝐿^{1}$

Metamath Proof Explorer

Theorem iblabs

Proof