itg2lea

Description: Approximate version of itg2le . If F <_ G for almost all x , then S.2 F <_ S.2 G . (Contributed by Mario Carneiro, 11-Aug-2014)

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

Proof

Step	Hyp	Ref	Expression
1		itg2lea.1	$⊢ φ \to F : ℝ ⟶ [0, +∞]$
2		itg2lea.2	$⊢ φ \to G : ℝ ⟶ [0, +∞]$
3		itg2lea.3	$⊢ φ \to A \subseteq ℝ$
4		itg2lea.4	$⊢ φ \to {vol}^{*} (A) = 0$
5		itg2lea.5	$⊢ (φ \land x \in (ℝ ∖ A)) \to F (x) \leq G (x)$
6	2	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to G : ℝ ⟶ [0, +∞]$
7		simprl	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to f \in dom \int^{1}$
8	3	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to A \subseteq ℝ$
9	4	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to {vol}^{*} (A) = 0$
10		i1ff	$⊢ f \in dom \int^{1} \to f : ℝ ⟶ ℝ$
11	10	ad2antrl	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to f : ℝ ⟶ ℝ$
12		eldifi	$⊢ x \in (ℝ ∖ A) \to x \in ℝ$
13		ffvelrn	$⊢ (f : ℝ ⟶ ℝ \land x \in ℝ) \to f (x) \in ℝ$
14	11 12 13	syl2an	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in (ℝ ∖ A)) \to f (x) \in ℝ$
15	14	rexrd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in (ℝ ∖ A)) \to f (x) \in ℝ^{*}$
16		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
17	1	adantr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to F : ℝ ⟶ [0, +∞]$
18		ffvelrn	$⊢ (F : ℝ ⟶ [0, +∞] \land x \in ℝ) \to F (x) \in [0, +∞]$
19	17 12 18	syl2an	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in (ℝ ∖ A)) \to F (x) \in [0, +∞]$
20	16 19	sseldi	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in (ℝ ∖ A)) \to F (x) \in ℝ^{*}$
21		ffvelrn	$⊢ (G : ℝ ⟶ [0, +∞] \land x \in ℝ) \to G (x) \in [0, +∞]$
22	6 12 21	syl2an	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in (ℝ ∖ A)) \to G (x) \in [0, +∞]$
23	16 22	sseldi	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in (ℝ ∖ A)) \to G (x) \in ℝ^{*}$
24		simprr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to f \leq_{f} F$
25	11	ffnd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to f Fn ℝ$
26	17	ffnd	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to F Fn ℝ$
27		reex	$⊢ ℝ \in V$
28	27	a1i	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to ℝ \in V$
29		inidm	$⊢ ℝ \cap ℝ = ℝ$
30		eqidd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in ℝ) \to f (x) = f (x)$
31		eqidd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in ℝ) \to F (x) = F (x)$
32	25 26 28 28 29 30 31	ofrfval	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to (f \leq_{f} F \leftrightarrow \forall x \in ℝ f (x) \leq F (x))$
33	24 32	mpbid	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \forall x \in ℝ f (x) \leq F (x)$
34	33	r19.21bi	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in ℝ) \to f (x) \leq F (x)$
35	12 34	sylan2	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in (ℝ ∖ A)) \to f (x) \leq F (x)$
36	5	adantlr	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in (ℝ ∖ A)) \to F (x) \leq G (x)$
37	15 20 23 35 36	xrletrd	$⊢ ((φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \land x \in (ℝ ∖ A)) \to f (x) \leq G (x)$
38	6 7 8 9 37	itg2uba	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} F)) \to \int^{1} (f) \leq \int^{2} (G)$
39	38	expr	$⊢ (φ \land f \in dom \int^{1}) \to (f \leq_{f} F \to \int^{1} (f) \leq \int^{2} (G))$
40	39	ralrimiva	$⊢ φ \to \forall f \in dom \int^{1} (f \leq_{f} F \to \int^{1} (f) \leq \int^{2} (G))$
41		itg2cl	$⊢ G : ℝ ⟶ [0, +∞] \to \int^{2} (G) \in ℝ^{*}$
42	2 41	syl	$⊢ φ \to \int^{2} (G) \in ℝ^{*}$
43		itg2leub	$⊢ (F : ℝ ⟶ [0, +∞] \land \int^{2} (G) \in ℝ^{*}) \to (\int^{2} (F) \leq \int^{2} (G) \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} F \to \int^{1} (f) \leq \int^{2} (G)))$
44	1 42 43	syl2anc	$⊢ φ \to (\int^{2} (F) \leq \int^{2} (G) \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} F \to \int^{1} (f) \leq \int^{2} (G)))$
45	40 44	mpbird	$⊢ φ \to \int^{2} (F) \leq \int^{2} (G)$

Metamath Proof Explorer

Theorem itg2lea

Proof