itg2uba

Description: Approximate version of itg2ub . If F approximately dominates G , then S.1 G <_ S.2 F . (Contributed by Mario Carneiro, 11-Aug-2014)

	Ref	Expression
Hypotheses	itg2uba.1	$⊢ φ \to F : ℝ ⟶ [0, +∞]$
	itg2uba.2	$⊢ φ \to G \in dom \int^{1}$
	itg2uba.3	$⊢ φ \to A \subseteq ℝ$
	itg2uba.4	$⊢ φ \to {vol}^{*} (A) = 0$
	itg2uba.5	$⊢ (φ \land x \in (ℝ ∖ A)) \to G (x) \leq F (x)$
Assertion	itg2uba	$⊢ φ \to \int^{1} (G) \leq \int^{2} (F)$

Proof

Step	Hyp	Ref	Expression
1		itg2uba.1	$⊢ φ \to F : ℝ ⟶ [0, +∞]$
2		itg2uba.2	$⊢ φ \to G \in dom \int^{1}$
3		itg2uba.3	$⊢ φ \to A \subseteq ℝ$
4		itg2uba.4	$⊢ φ \to {vol}^{*} (A) = 0$
5		itg2uba.5	$⊢ (φ \land x \in (ℝ ∖ A)) \to G (x) \leq F (x)$
6		itg1cl	$⊢ G \in dom \int^{1} \to \int^{1} (G) \in ℝ$
7	2 6	syl	$⊢ φ \to \int^{1} (G) \in ℝ$
8	7	rexrd	$⊢ φ \to \int^{1} (G) \in ℝ^{*}$
9		nulmbl	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) = 0) \to A \in dom vol$
10	3 4 9	syl2anc	$⊢ φ \to A \in dom vol$
11		cmmbl	$⊢ A \in dom vol \to ℝ ∖ A \in dom vol$
12	10 11	syl	$⊢ φ \to ℝ ∖ A \in dom vol$
13		ifnot	$⊢ if (\neg x \in A, G (x), 0) = if (x \in A, 0, G (x))$
14		eldif	$⊢ x \in (ℝ ∖ A) \leftrightarrow (x \in ℝ \land \neg x \in A)$
15	14	baibr	$⊢ x \in ℝ \to (\neg x \in A \leftrightarrow x \in (ℝ ∖ A))$
16	15	ifbid	$⊢ x \in ℝ \to if (\neg x \in A, G (x), 0) = if (x \in (ℝ ∖ A), G (x), 0)$
17	13 16	eqtr3id	$⊢ x \in ℝ \to if (x \in A, 0, G (x)) = if (x \in (ℝ ∖ A), G (x), 0)$
18	17	mpteq2ia	$⊢ (x \in ℝ ⟼ if (x \in A, 0, G (x))) = (x \in ℝ ⟼ if (x \in (ℝ ∖ A), G (x), 0))$
19	18	i1fres	$⊢ (G \in dom \int^{1} \land ℝ ∖ A \in dom vol) \to (x \in ℝ ⟼ if (x \in A, 0, G (x))) \in dom \int^{1}$
20	2 12 19	syl2anc	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, 0, G (x))) \in dom \int^{1}$
21		itg1cl	$⊢ (x \in ℝ ⟼ if (x \in A, 0, G (x))) \in dom \int^{1} \to \int^{1} ((x \in ℝ ⟼ if (x \in A, 0, G (x)))) \in ℝ$
22	20 21	syl	$⊢ φ \to \int^{1} ((x \in ℝ ⟼ if (x \in A, 0, G (x)))) \in ℝ$
23	22	rexrd	$⊢ φ \to \int^{1} ((x \in ℝ ⟼ if (x \in A, 0, G (x)))) \in ℝ^{*}$
24		itg2cl	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) \in ℝ^{*}$
25	1 24	syl	$⊢ φ \to \int^{2} (F) \in ℝ^{*}$
26		i1ff	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℝ$
27	2 26	syl	$⊢ φ \to G : ℝ ⟶ ℝ$
28		eldifi	$⊢ y \in (ℝ ∖ A) \to y \in ℝ$
29		ffvelcdm	$⊢ (G : ℝ ⟶ ℝ \land y \in ℝ) \to G (y) \in ℝ$
30	27 28 29	syl2an	$⊢ (φ \land y \in (ℝ ∖ A)) \to G (y) \in ℝ$
31	30	leidd	$⊢ (φ \land y \in (ℝ ∖ A)) \to G (y) \leq G (y)$
32		eldif	$⊢ y \in (ℝ ∖ A) \leftrightarrow (y \in ℝ \land \neg y \in A)$
33		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
34		fveq2	$⊢ x = y \to G (x) = G (y)$
35	33 34	ifbieq2d	$⊢ x = y \to if (x \in A, 0, G (x)) = if (y \in A, 0, G (y))$
36		eqid	$⊢ (x \in ℝ ⟼ if (x \in A, 0, G (x))) = (x \in ℝ ⟼ if (x \in A, 0, G (x)))$
37		c0ex	$⊢ 0 \in V$
38		fvex	$⊢ G (y) \in V$
39	37 38	ifex	$⊢ if (y \in A, 0, G (y)) \in V$
40	35 36 39	fvmpt	$⊢ y \in ℝ \to (x \in ℝ ⟼ if (x \in A, 0, G (x))) (y) = if (y \in A, 0, G (y))$
41		iffalse	$⊢ \neg y \in A \to if (y \in A, 0, G (y)) = G (y)$
42	40 41	sylan9eq	$⊢ (y \in ℝ \land \neg y \in A) \to (x \in ℝ ⟼ if (x \in A, 0, G (x))) (y) = G (y)$
43	32 42	sylbi	$⊢ y \in (ℝ ∖ A) \to (x \in ℝ ⟼ if (x \in A, 0, G (x))) (y) = G (y)$
44	43	adantl	$⊢ (φ \land y \in (ℝ ∖ A)) \to (x \in ℝ ⟼ if (x \in A, 0, G (x))) (y) = G (y)$
45	31 44	breqtrrd	$⊢ (φ \land y \in (ℝ ∖ A)) \to G (y) \leq (x \in ℝ ⟼ if (x \in A, 0, G (x))) (y)$
46	2 3 4 20 45	itg1lea	$⊢ φ \to \int^{1} (G) \leq \int^{1} ((x \in ℝ ⟼ if (x \in A, 0, G (x))))$
47		iftrue	$⊢ x \in A \to if (x \in A, 0, G (x)) = 0$
48	47	adantl	$⊢ ((φ \land x \in ℝ) \land x \in A) \to if (x \in A, 0, G (x)) = 0$
49	1	ffvelcdmda	$⊢ (φ \land x \in ℝ) \to F (x) \in [0, +∞]$
50		elxrge0	$⊢ F (x) \in [0, +∞] \leftrightarrow (F (x) \in ℝ^{*} \land 0 \leq F (x))$
51	49 50	sylib	$⊢ (φ \land x \in ℝ) \to (F (x) \in ℝ^{*} \land 0 \leq F (x))$
52	51	simprd	$⊢ (φ \land x \in ℝ) \to 0 \leq F (x)$
53	52	adantr	$⊢ ((φ \land x \in ℝ) \land x \in A) \to 0 \leq F (x)$
54	48 53	eqbrtrd	$⊢ ((φ \land x \in ℝ) \land x \in A) \to if (x \in A, 0, G (x)) \leq F (x)$
55		iffalse	$⊢ \neg x \in A \to if (x \in A, 0, G (x)) = G (x)$
56	55	adantl	$⊢ ((φ \land x \in ℝ) \land \neg x \in A) \to if (x \in A, 0, G (x)) = G (x)$
57	14 5	sylan2br	$⊢ (φ \land (x \in ℝ \land \neg x \in A)) \to G (x) \leq F (x)$
58	57	anassrs	$⊢ ((φ \land x \in ℝ) \land \neg x \in A) \to G (x) \leq F (x)$
59	56 58	eqbrtrd	$⊢ ((φ \land x \in ℝ) \land \neg x \in A) \to if (x \in A, 0, G (x)) \leq F (x)$
60	54 59	pm2.61dan	$⊢ (φ \land x \in ℝ) \to if (x \in A, 0, G (x)) \leq F (x)$
61	60	ralrimiva	$⊢ φ \to \forall x \in ℝ if (x \in A, 0, G (x)) \leq F (x)$
62		reex	$⊢ ℝ \in V$
63	62	a1i	$⊢ φ \to ℝ \in V$
64		fvex	$⊢ G (x) \in V$
65	37 64	ifex	$⊢ if (x \in A, 0, G (x)) \in V$
66	65	a1i	$⊢ (φ \land x \in ℝ) \to if (x \in A, 0, G (x)) \in V$
67		fvexd	$⊢ (φ \land x \in ℝ) \to F (x) \in V$
68		eqidd	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, 0, G (x))) = (x \in ℝ ⟼ if (x \in A, 0, G (x)))$
69	1	feqmptd	$⊢ φ \to F = (x \in ℝ ⟼ F (x))$
70	63 66 67 68 69	ofrfval2	$⊢ φ \to ((x \in ℝ ⟼ if (x \in A, 0, G (x))) \leq_{f} F \leftrightarrow \forall x \in ℝ if (x \in A, 0, G (x)) \leq F (x))$
71	61 70	mpbird	$⊢ φ \to (x \in ℝ ⟼ if (x \in A, 0, G (x))) \leq_{f} F$
72		itg2ub	$⊢ (F : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in A, 0, G (x))) \in dom \int^{1} \land (x \in ℝ ⟼ if (x \in A, 0, G (x))) \leq_{f} F) \to \int^{1} ((x \in ℝ ⟼ if (x \in A, 0, G (x)))) \leq \int^{2} (F)$
73	1 20 71 72	syl3anc	$⊢ φ \to \int^{1} ((x \in ℝ ⟼ if (x \in A, 0, G (x)))) \leq \int^{2} (F)$
74	8 23 25 46 73	xrletrd	$⊢ φ \to \int^{1} (G) \leq \int^{2} (F)$

Metamath Proof Explorer

Theorem itg2uba

Proof