itgabsnc

Description: Choice-free analogue of itgabs . (Contributed by Brendan Leahy, 19-Nov-2017) (Revised by Brendan Leahy, 19-Jun-2018)

	Ref	Expression
Hypotheses	itgabsnc.1	$⊢ (φ \land x \in A) \to B \in V$
	itgabsnc.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
	itgabsnc.m1	$⊢ φ \to (x \in A ⟼ \|B\|) \in MblFn$
	itgabsnc.m2	$⊢ φ \to (y \in A ⟼ \overline{\int_{A} B d x} ⦋ y / x ⦌ B) \in MblFn$
Assertion	itgabsnc	$⊢ φ \to \|\int_{A} B d x\| \leq \int_{A} \|B\| d x$

Proof

Step	Hyp	Ref	Expression
1		itgabsnc.1	$⊢ (φ \land x \in A) \to B \in V$
2		itgabsnc.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
3		itgabsnc.m1	$⊢ φ \to (x \in A ⟼ \|B\|) \in MblFn$
4		itgabsnc.m2	$⊢ φ \to (y \in A ⟼ \overline{\int_{A} B d x} ⦋ y / x ⦌ B) \in MblFn$
5	1 2	itgcl	$⊢ φ \to \int_{A} B d x \in ℂ$
6	5	cjcld	$⊢ φ \to \overline{\int_{A} B d x} \in ℂ$
7		iblmbf	$⊢ (x \in A ⟼ B) \in 𝐿^{1} \to (x \in A ⟼ B) \in MblFn$
8	2 7	syl	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
9	8 1	mbfmptcl	$⊢ (φ \land x \in A) \to B \in ℂ$
10	9	ralrimiva	$⊢ φ \to \forall x \in A B \in ℂ$
11		nfv	$⊢ Ⅎ y B \in ℂ$
12		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
13	12	nfel1	$⊢ Ⅎ x ⦋ y / x ⦌ B \in ℂ$
14		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
15	14	eleq1d	$⊢ x = y \to (B \in ℂ \leftrightarrow ⦋ y / x ⦌ B \in ℂ)$
16	11 13 15	cbvralw	$⊢ \forall x \in A B \in ℂ \leftrightarrow \forall y \in A ⦋ y / x ⦌ B \in ℂ$
17	10 16	sylib	$⊢ φ \to \forall y \in A ⦋ y / x ⦌ B \in ℂ$
18	17	r19.21bi	$⊢ (φ \land y \in A) \to ⦋ y / x ⦌ B \in ℂ$
19		nfcv	$⊢ \underline{Ⅎ} y B$
20	19 12 14	cbvmpt	$⊢ (x \in A ⟼ B) = (y \in A ⟼ ⦋ y / x ⦌ B)$
21	20 2	eqeltrrid	$⊢ φ \to (y \in A ⟼ ⦋ y / x ⦌ B) \in 𝐿^{1}$
22	6 18 21 4	iblmulc2nc	$⊢ φ \to (y \in A ⟼ \overline{\int_{A} B d x} ⦋ y / x ⦌ B) \in 𝐿^{1}$
23	6	adantr	$⊢ (φ \land y \in A) \to \overline{\int_{A} B d x} \in ℂ$
24	23 18	mulcld	$⊢ (φ \land y \in A) \to \overline{\int_{A} B d x} ⦋ y / x ⦌ B \in ℂ$
25	24	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}))$
26	22 25	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})$
27	26	simpld	$⊢ φ \to (y \in A ⟼ ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B)) \in 𝐿^{1}$
28	23 18	absmuld	$⊢ (φ \land y \in A) \to \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\| = \|\overline{\int_{A} B d x}\| \|⦋ y / x ⦌ B\|$
29	28	mpteq2dva	$⊢ φ \to (y \in A ⟼ \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\|) = (y \in A ⟼ \|\overline{\int_{A} B d x}\| \|⦋ y / x ⦌ B\|)$
30	8 1	mbfdm2	$⊢ φ \to A \in dom vol$
31	23	abscld	$⊢ (φ \land y \in A) \to \|\overline{\int_{A} B d x}\| \in ℝ$
32	18	abscld	$⊢ (φ \land y \in A) \to \|⦋ y / x ⦌ B\| \in ℝ$
33		fconstmpt	$⊢ A \times \{\|\overline{\int_{A} B d x}\|\} = (y \in A ⟼ \|\overline{\int_{A} B d x}\|)$
34	33	a1i	$⊢ φ \to A \times \{\|\overline{\int_{A} B d x}\|\} = (y \in A ⟼ \|\overline{\int_{A} B d x}\|)$
35		nfcv	$⊢ \underline{Ⅎ} y \|B\|$
36		nfcv	$⊢ \underline{Ⅎ} x abs$
37	36 12	nffv	$⊢ \underline{Ⅎ} x \|⦋ y / x ⦌ B\|$
38	14	fveq2d	$⊢ x = y \to \|B\| = \|⦋ y / x ⦌ B\|$
39	35 37 38	cbvmpt	$⊢ (x \in A ⟼ \|B\|) = (y \in A ⟼ \|⦋ y / x ⦌ B\|)$
40	39	a1i	$⊢ φ \to (x \in A ⟼ \|B\|) = (y \in A ⟼ \|⦋ y / x ⦌ B\|)$
41	30 31 32 34 40	offval2	$⊢ φ \to (A \times \{\|\overline{\int_{A} B d x}\|\}) \times_{f} (x \in A ⟼ \|B\|) = (y \in A ⟼ \|\overline{\int_{A} B d x}\| \|⦋ y / x ⦌ B\|)$
42	29 41	eqtr4d	$⊢ φ \to (y \in A ⟼ \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\|) = (A \times \{\|\overline{\int_{A} B d x}\|\}) \times_{f} (x \in A ⟼ \|B\|)$
43	6	abscld	$⊢ φ \to \|\overline{\int_{A} B d x}\| \in ℝ$
44	9	abscld	$⊢ (φ \land x \in A) \to \|B\| \in ℝ$
45	44	recnd	$⊢ (φ \land x \in A) \to \|B\| \in ℂ$
46	45	fmpttd	$⊢ φ \to (x \in A ⟼ \|B\|) : A ⟶ ℂ$
47	3 43 46	mbfmulc2re	$⊢ φ \to (A \times \{\|\overline{\int_{A} B d x}\|\}) \times_{f} (x \in A ⟼ \|B\|) \in MblFn$
48	42 47	eqeltrd	$⊢ φ \to (y \in A ⟼ \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\|) \in MblFn$
49	24 22 48	iblabsnc	$⊢ φ \to (y \in A ⟼ \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\|) \in 𝐿^{1}$
50	24	recld	$⊢ (φ \land y \in A) \to ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B) \in ℝ$
51	24	abscld	$⊢ (φ \land y \in A) \to \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\| \in ℝ$
52	24	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\|$
53	27 49 50 51 52	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$
54	5	abscld	$⊢ φ \to \|\int_{A} B d x\| \in ℝ$
55	54	recnd	$⊢ φ \to \|\int_{A} B d x\| \in ℂ$
56	55	sqvald	$⊢ φ \to {\|\int_{A} B d x\|}^{2} = \|\int_{A} B d x\| \|\int_{A} B d x\|$
57	5	absvalsqd	$⊢ φ \to {\|\int_{A} B d x\|}^{2} = \int_{A} B d x \overline{\int_{A} B d x}$
58	5 6	mulcomd	$⊢ φ \to \int_{A} B d x \overline{\int_{A} B d x} = \overline{\int_{A} B d x} \int_{A} B d x$
59	14 19 12	cbvitg	$⊢ \int_{A} B d x = \int_{A} ⦋ y / x ⦌ B d y$
60	59	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$
61	6 18 21 4	itgmulc2nc	$⊢ φ \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$
62	60 61	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$
63	57 58 62	3eqtrd	$⊢ φ \to {\|\int_{A} B d x\|}^{2} = \int_{A} \overline{\int_{A} B d x} ⦋ y / x ⦌ B d y$
64	63	fveq2d	$⊢ φ \to ℜ ({\|\int_{A} B d x\|}^{2}) = ℜ (\int_{A} \overline{\int_{A} B d x} ⦋ y / x ⦌ B d y)$
65	54	resqcld	$⊢ φ \to {\|\int_{A} B d x\|}^{2} \in ℝ$
66	65	rered	$⊢ φ \to ℜ ({\|\int_{A} B d x\|}^{2}) = {\|\int_{A} B d x\|}^{2}$
67		ovexd	$⊢ (φ \land y \in A) \to \overline{\int_{A} B d x} ⦋ y / x ⦌ B \in V$
68	67 22	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$
69	64 66 68	3eqtr3d	$⊢ φ \to {\|\int_{A} B d x\|}^{2} = \int_{A} ℜ (\overline{\int_{A} B d x} ⦋ y / x ⦌ B) d y$
70	56 69	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$
71	38 35 37	cbvitg	$⊢ \int_{A} \|B\| d x = \int_{A} \|⦋ y / x ⦌ B\| d y$
72	71	oveq2i	$⊢ \|\int_{A} B d x\| \int_{A} \|B\| d x = \|\int_{A} B d x\| \int_{A} \|⦋ y / x ⦌ B\| d y$
73	1 2 3	iblabsnc	$⊢ φ \to (x \in A ⟼ \|B\|) \in 𝐿^{1}$
74	39 73	eqeltrrid	$⊢ φ \to (y \in A ⟼ \|⦋ y / x ⦌ B\|) \in 𝐿^{1}$
75	54	adantr	$⊢ (φ \land y \in A) \to \|\int_{A} B d x\| \in ℝ$
76		fconstmpt	$⊢ A \times \{\|\int_{A} B d x\|\} = (y \in A ⟼ \|\int_{A} B d x\|)$
77	76	a1i	$⊢ φ \to A \times \{\|\int_{A} B d x\|\} = (y \in A ⟼ \|\int_{A} B d x\|)$
78	30 75 32 77 40	offval2	$⊢ φ \to (A \times \{\|\int_{A} B d x\|\}) \times_{f} (x \in A ⟼ \|B\|) = (y \in A ⟼ \|\int_{A} B d x\| \|⦋ y / x ⦌ B\|)$
79	3 54 46	mbfmulc2re	$⊢ φ \to (A \times \{\|\int_{A} B d x\|\}) \times_{f} (x \in A ⟼ \|B\|) \in MblFn$
80	78 79	eqeltrrd	$⊢ φ \to (y \in A ⟼ \|\int_{A} B d x\| \|⦋ y / x ⦌ B\|) \in MblFn$
81	55 32 74 80	itgmulc2nc	$⊢ φ \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$
82	5	adantr	$⊢ (φ \land y \in A) \to \int_{A} B d x \in ℂ$
83	82	abscjd	$⊢ (φ \land y \in A) \to \|\overline{\int_{A} B d x}\| = \|\int_{A} B d x\|$
84	83	oveq1d	$⊢ (φ \land y \in A) \to \|\overline{\int_{A} B d x}\| \|⦋ y / x ⦌ B\| = \|\int_{A} B d x\| \|⦋ y / x ⦌ B\|$
85	28 84	eqtrd	$⊢ (φ \land y \in A) \to \|\overline{\int_{A} B d x} ⦋ y / x ⦌ B\| = \|\int_{A} B d x\| \|⦋ y / x ⦌ B\|$
86	85	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$
87	81 86	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$
88	72 87	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$
89	53 70 88	3brtr4d	$⊢ φ \to \|\int_{A} B d x\| \|\int_{A} B d x\| \leq \|\int_{A} B d x\| \int_{A} \|B\| d x$
90	89	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$
91	54	adantr	$⊢ (φ \land 0 < \|\int_{A} B d x\|) \to \|\int_{A} B d x\| \in ℝ$
92	44 73	itgrecl	$⊢ φ \to \int_{A} \|B\| d x \in ℝ$
93	92	adantr	$⊢ (φ \land 0 < \|\int_{A} B d x\|) \to \int_{A} \|B\| d x \in ℝ$
94		simpr	$⊢ (φ \land 0 < \|\int_{A} B d x\|) \to 0 < \|\int_{A} B d x\|$
95		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)$
96	91 93 91 94 95	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)$
97	90 96	mpbird	$⊢ (φ \land 0 < \|\int_{A} B d x\|) \to \|\int_{A} B d x\| \leq \int_{A} \|B\| d x$
98	97	ex	$⊢ φ \to (0 < \|\int_{A} B d x\| \to \|\int_{A} B d x\| \leq \int_{A} \|B\| d x)$
99	9	absge0d	$⊢ (φ \land x \in A) \to 0 \leq \|B\|$
100	73 44 99	itgge0	$⊢ φ \to 0 \leq \int_{A} \|B\| d x$
101		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)$
102	100 101	syl5ibcom	$⊢ φ \to (0 = \|\int_{A} B d x\| \to \|\int_{A} B d x\| \leq \int_{A} \|B\| d x)$
103	5	absge0d	$⊢ φ \to 0 \leq \|\int_{A} B d x\|$
104		0re	$⊢ 0 \in ℝ$
105		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\|))$
106	104 54 105	sylancr	$⊢ φ \to (0 \leq \|\int_{A} B d x\| \leftrightarrow (0 < \|\int_{A} B d x\| \lor 0 = \|\int_{A} B d x\|))$
107	103 106	mpbid	$⊢ φ \to (0 < \|\int_{A} B d x\| \lor 0 = \|\int_{A} B d x\|)$
108	98 102 107	mpjaod	$⊢ φ \to \|\int_{A} B d x\| \leq \int_{A} \|B\| d x$

Metamath Proof Explorer

Theorem itgabsnc

Proof