itg2itg1

Description: The integral of a nonnegative simple function using S.2 is the same as its value under S.1 . (Contributed by Mario Carneiro, 28-Jun-2014)

		Ref	Expression
	Assertion	itg2itg1	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to \int^{2} (F) = \int^{1} (F)$

Proof

Step	Hyp	Ref	Expression
1		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
2		xrge0f	$⊢ (F : ℝ ⟶ ℝ \land 0_{𝑝} \leq_{f} F) \to F : ℝ ⟶ [0, +∞]$
3	1 2	sylan	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to F : ℝ ⟶ [0, +∞]$
4		itg2cl	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) \in ℝ^{*}$
5	3 4	syl	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to \int^{2} (F) \in ℝ^{*}$
6		itg1cl	$⊢ F \in dom \int^{1} \to \int^{1} (F) \in ℝ$
7	6	adantr	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to \int^{1} (F) \in ℝ$
8	7	rexrd	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to \int^{1} (F) \in ℝ^{*}$
9		itg1le	$⊢ (g \in dom \int^{1} \land F \in dom \int^{1} \land g \leq_{f} F) \to \int^{1} (g) \leq \int^{1} (F)$
10	9	3expia	$⊢ (g \in dom \int^{1} \land F \in dom \int^{1}) \to (g \leq_{f} F \to \int^{1} (g) \leq \int^{1} (F))$
11	10	ancoms	$⊢ (F \in dom \int^{1} \land g \in dom \int^{1}) \to (g \leq_{f} F \to \int^{1} (g) \leq \int^{1} (F))$
12	11	ralrimiva	$⊢ F \in dom \int^{1} \to \forall g \in dom \int^{1} (g \leq_{f} F \to \int^{1} (g) \leq \int^{1} (F))$
13	12	adantr	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to \forall g \in dom \int^{1} (g \leq_{f} F \to \int^{1} (g) \leq \int^{1} (F))$
14		itg2leub	$⊢ (F : ℝ ⟶ [0, +∞] \land \int^{1} (F) \in ℝ^{*}) \to (\int^{2} (F) \leq \int^{1} (F) \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} F \to \int^{1} (g) \leq \int^{1} (F)))$
15	3 8 14	syl2anc	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to (\int^{2} (F) \leq \int^{1} (F) \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} F \to \int^{1} (g) \leq \int^{1} (F)))$
16	13 15	mpbird	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to \int^{2} (F) \leq \int^{1} (F)$
17		simpl	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to F \in dom \int^{1}$
18		reex	$⊢ ℝ \in V$
19	18	a1i	$⊢ F \in dom \int^{1} \to ℝ \in V$
20		leid	$⊢ x \in ℝ \to x \leq x$
21	20	adantl	$⊢ (F \in dom \int^{1} \land x \in ℝ) \to x \leq x$
22	19 1 21	caofref	$⊢ F \in dom \int^{1} \to F \leq_{f} F$
23	22	adantr	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to F \leq_{f} F$
24		itg2ub	$⊢ (F : ℝ ⟶ [0, +∞] \land F \in dom \int^{1} \land F \leq_{f} F) \to \int^{1} (F) \leq \int^{2} (F)$
25	3 17 23 24	syl3anc	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to \int^{1} (F) \leq \int^{2} (F)$
26	5 8 16 25	xrletrid	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to \int^{2} (F) = \int^{1} (F)$

Metamath Proof Explorer

Theorem itg2itg1

Proof