itgabs

Description: The triangle inequality for integrals. (Contributed by Mario Carneiro, 25-Aug-2014)

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

Proof

Step	Hyp	Ref	Expression
1		itgabs.1	$⊢ (φ \land x \in A) \to B \in V$
2		itgabs.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
3	1 2	itgcl	$⊢ φ \to \int_{A} B d x \in ℂ$
4	3	cjcld	$⊢ φ \to \overline{\int_{A} B d x} \in ℂ$
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	7	ralrimiva	$⊢ φ \to \forall x \in A B \in ℂ$
9		nfv	$⊢ Ⅎ y B \in ℂ$
10		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
11	10	nfel1	$⊢ Ⅎ x ⦋ y / x ⦌ B \in ℂ$
12		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
13	12	eleq1d	$⊢ x = y \to (B \in ℂ \leftrightarrow ⦋ y / x ⦌ B \in ℂ)$
14	9 11 13	cbvralw	$⊢ \forall x \in A B \in ℂ \leftrightarrow \forall y \in A ⦋ y / x ⦌ B \in ℂ$
15	8 14	sylib	$⊢ φ \to \forall y \in A ⦋ y / x ⦌ B \in ℂ$
16	15	r19.21bi	$⊢ (φ \land y \in A) \to ⦋ y / x ⦌ B \in ℂ$
17		nfcv	$⊢ \underline{Ⅎ} y B$
18	17 10 12	cbvmpt	$⊢ (x \in A ⟼ B) = (y \in A ⟼ ⦋ y / x ⦌ B)$
19	18 2	eqeltrrid	$⊢ φ \to (y \in A ⟼ ⦋ y / x ⦌ B) \in 𝐿^{1}$
20	4 16 19	iblmulc2	$⊢ φ \to (y \in A ⟼ \overline{\int_{A} B d x} ⦋ y / x ⦌ B) \in 𝐿^{1}$
21	4	adantr	$⊢ (φ \land y \in A) \to \overline{\int_{A} B d x} \in ℂ$
22	21 16	mulcld	$⊢ (φ \land y \in A) \to \overline{\int_{A} B d x} ⦋ y / x ⦌ B \in ℂ$
23	22	iblcn	$⊢ φ \to ((y \in A ⟼ \overline{\int_{A} B d x} ⦋ y / x ⦌ B) \in 𝐿^{1} \leftrightarrow ((y \in A ⟼ ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B)) \in 𝐿^{1} \land (y \in A ⟼ ℑ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B)) \in 𝐿^{1}))$
24	20 23	mpbid	$⊢ φ \to ((y \in A ⟼ ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B)) \in 𝐿^{1} \land (y \in A ⟼ ℑ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B)) \in 𝐿^{1})$
25	24	simpld	$⊢ φ \to (y \in A ⟼ ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B)) \in 𝐿^{1}$
26		ovexd	$⊢ (φ \land y \in A) \to \overline{\int_{A} B d x} ⦋ y / x ⦌ B \in V$
27	26 20	iblabs	$⊢ φ \to (y \in A ⟼ \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\|) \in 𝐿^{1}$
28	22	recld	$⊢ (φ \land y \in A) \to ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B) \in ℝ$
29	22	abscld	$⊢ (φ \land y \in A) \to \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\| \in ℝ$
30	22	releabsd	$⊢ (φ \land y \in A) \to ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B) \leq \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\|$
31	25 27 28 29 30	itgle	$⊢ φ \to \int_{A} ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B) d y \leq \int_{A} \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\| d y$
32	3	abscld	$⊢ φ \to \|\int_{A} B d x\| \in ℝ$
33	32	recnd	$⊢ φ \to \|\int_{A} B d x\| \in ℂ$
34	33	sqvald	$⊢ φ \to {\|\int_{A} B d x\|}^{2} = \|\int_{A} B d x\| \|\int_{A} B d x\|$
35	3	absvalsqd	$⊢ φ \to {\|\int_{A} B d x\|}^{2} = \int_{A} B d x \overline{\int_{A} B d x}$
36	3 4	mulcomd	$⊢ φ \to \int_{A} B d x \overline{\int_{A} B d x} = \overline{\int_{A} B d x} \int_{A} B d x$
37	12 17 10	cbvitg	$⊢ \int_{A} B d x = \int_{A} ⦋ y / x ⦌ B d y$
38	37	oveq2i	$⊢ \overline{\int_{A} B d x} \int_{A} B d x = \overline{\int_{A} B d x} \int_{A} ⦋ y / x ⦌ B d y$
39	4 16 19	itgmulc2	$⊢ φ \to \overline{\int_{A} B d x} \int_{A} ⦋ y / x ⦌ B d y = \int_{A} \overline{\int_{A} B d x} ⦋ y / x ⦌ B d y$
40	38 39	syl5eq	$⊢ φ \to \overline{\int_{A} B d x} \int_{A} B d x = \int_{A} \overline{\int_{A} B d x} ⦋ y / x ⦌ B d y$
41	35 36 40	3eqtrd	$⊢ φ \to {\|\int_{A} B d x\|}^{2} = \int_{A} \overline{\int_{A} B d x} ⦋ y / x ⦌ B d y$
42	41	fveq2d	$⊢ φ \to ℜ ({\|\int_{A} B d x\|}^{2}) = ℜ (\int_{A} \overline{\int_{A} B d x} ⦋ y / x ⦌ B d y)$
43	32	resqcld	$⊢ φ \to {\|\int_{A} B d x\|}^{2} \in ℝ$
44	43	rered	$⊢ φ \to ℜ ({\|\int_{A} B d x\|}^{2}) = {\|\int_{A} B d x\|}^{2}$
45	26 20	itgre	$⊢ φ \to ℜ (\int_{A} \overline{\int_{A} B d x} ⦋ y / x ⦌ B d y) = \int_{A} ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B) d y$
46	42 44 45	3eqtr3d	$⊢ φ \to {\|\int_{A} B d x\|}^{2} = \int_{A} ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B) d y$
47	34 46	eqtr3d	$⊢ φ \to \|\int_{A} B d x\| \|\int_{A} B d x\| = \int_{A} ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B) d y$
48	12	fveq2d	$⊢ x = y \to \|B\| = \|⦋ y / x ⦌ B\|$
49		nfcv	$⊢ \underline{Ⅎ} y \|B\|$
50		nfcv	$⊢ \underline{Ⅎ} x abs$
51	50 10	nffv	$⊢ \underline{Ⅎ} x \|⦋ y / x ⦌ B\|$
52	48 49 51	cbvitg	$⊢ \int_{A} \|B\| d x = \int_{A} \|⦋ y / x ⦌ B\| d y$
53	52	oveq2i	$⊢ \|\int_{A} B d x\| \int_{A} \|B\| d x = \|\int_{A} B d x\| \int_{A} \|⦋ y / x ⦌ B\| d y$
54	16	abscld	$⊢ (φ \land y \in A) \to \|⦋ y / x ⦌ B\| \in ℝ$
55	16 19	iblabs	$⊢ φ \to (y \in A ⟼ \|⦋ y / x ⦌ B\|) \in 𝐿^{1}$
56	33 54 55	itgmulc2	$⊢ φ \to \|\int_{A} B d x\| \int_{A} \|⦋ y / x ⦌ B\| d y = \int_{A} \|\int_{A} B d x\| \|⦋ y / x ⦌ B\| d y$
57	21 16	absmuld	$⊢ (φ \land y \in A) \to \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\| = \|\overline{\int_{A} B d x}\| \|⦋ y / x ⦌ B\|$
58	3	adantr	$⊢ (φ \land y \in A) \to \int_{A} B d x \in ℂ$
59	58	abscjd	$⊢ (φ \land y \in A) \to \|\overline{\int_{A} B d x}\| = \|\int_{A} B d x\|$
60	59	oveq1d	$⊢ (φ \land y \in A) \to \|\overline{\int_{A} B d x}\| \|⦋ y / x ⦌ B\| = \|\int_{A} B d x\| \|⦋ y / x ⦌ B\|$
61	57 60	eqtrd	$⊢ (φ \land y \in A) \to \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\| = \|\int_{A} B d x\| \|⦋ y / x ⦌ B\|$
62	61	itgeq2dv	$⊢ φ \to \int_{A} \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\| d y = \int_{A} \|\int_{A} B d x\| \|⦋ y / x ⦌ B\| d y$
63	56 62	eqtr4d	$⊢ φ \to \|\int_{A} B d x\| \int_{A} \|⦋ y / x ⦌ B\| d y = \int_{A} \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\| d y$
64	53 63	syl5eq	$⊢ φ \to \|\int_{A} B d x\| \int_{A} \|B\| d x = \int_{A} \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\| d y$
65	31 47 64	3brtr4d	$⊢ φ \to \|\int_{A} B d x\| \|\int_{A} B d x\| \leq \|\int_{A} B d x\| \int_{A} \|B\| d x$
66	65	adantr	$⊢ (φ \land 0 < \|\int_{A} B d x\|) \to \|\int_{A} B d x\| \|\int_{A} B d x\| \leq \|\int_{A} B d x\| \int_{A} \|B\| d x$
67	32	adantr	$⊢ (φ \land 0 < \|\int_{A} B d x\|) \to \|\int_{A} B d x\| \in ℝ$
68	7	abscld	$⊢ (φ \land x \in A) \to \|B\| \in ℝ$
69	1 2	iblabs	$⊢ φ \to (x \in A ⟼ \|B\|) \in 𝐿^{1}$
70	68 69	itgrecl	$⊢ φ \to \int_{A} \|B\| d x \in ℝ$
71	70	adantr	$⊢ (φ \land 0 < \|\int_{A} B d x\|) \to \int_{A} \|B\| d x \in ℝ$
72		simpr	$⊢ (φ \land 0 < \|\int_{A} B d x\|) \to 0 < \|\int_{A} B d x\|$
73		lemul2	$⊢ (\|\int_{A} B d x\| \in ℝ \land \int_{A} \|B\| d x \in ℝ \land (\|\int_{A} B d x\| \in ℝ \land 0 < \|\int_{A} B d x\|)) \to (\|\int_{A} B d x\| \leq \int_{A} \|B\| d x \leftrightarrow \|\int_{A} B d x\| \|\int_{A} B d x\| \leq \|\int_{A} B d x\| \int_{A} \|B\| d x)$
74	67 71 67 72 73	syl112anc	$⊢ (φ \land 0 < \|\int_{A} B d x\|) \to (\|\int_{A} B d x\| \leq \int_{A} \|B\| d x \leftrightarrow \|\int_{A} B d x\| \|\int_{A} B d x\| \leq \|\int_{A} B d x\| \int_{A} \|B\| d x)$
75	66 74	mpbird	$⊢ (φ \land 0 < \|\int_{A} B d x\|) \to \|\int_{A} B d x\| \leq \int_{A} \|B\| d x$
76	75	ex	$⊢ φ \to (0 < \|\int_{A} B d x\| \to \|\int_{A} B d x\| \leq \int_{A} \|B\| d x)$
77	7	absge0d	$⊢ (φ \land x \in A) \to 0 \leq \|B\|$
78	69 68 77	itgge0	$⊢ φ \to 0 \leq \int_{A} \|B\| d x$
79		breq1	$⊢ 0 = \|\int_{A} B d x\| \to (0 \leq \int_{A} \|B\| d x \leftrightarrow \|\int_{A} B d x\| \leq \int_{A} \|B\| d x)$
80	78 79	syl5ibcom	$⊢ φ \to (0 = \|\int_{A} B d x\| \to \|\int_{A} B d x\| \leq \int_{A} \|B\| d x)$
81	3	absge0d	$⊢ φ \to 0 \leq \|\int_{A} B d x\|$
82		0re	$⊢ 0 \in ℝ$
83		leloe	$⊢ (0 \in ℝ \land \|\int_{A} B d x\| \in ℝ) \to (0 \leq \|\int_{A} B d x\| \leftrightarrow (0 < \|\int_{A} B d x\| \lor 0 = \|\int_{A} B d x\|))$
84	82 32 83	sylancr	$⊢ φ \to (0 \leq \|\int_{A} B d x\| \leftrightarrow (0 < \|\int_{A} B d x\| \lor 0 = \|\int_{A} B d x\|))$
85	81 84	mpbid	$⊢ φ \to (0 < \|\int_{A} B d x\| \lor 0 = \|\int_{A} B d x\|)$
86	76 80 85	mpjaod	$⊢ φ \to \|\int_{A} B d x\| \leq \int_{A} \|B\| d x$

Metamath Proof Explorer

Theorem itgabs

Proof