itg1ge0

Description: Closure of the integral on positive simple functions. (Contributed by Mario Carneiro, 19-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$
2		difss	$⊢ ran F ∖ \{0\} \subseteq ran F$
3		ssfi	$⊢ (ran F \in Fin \land ran F ∖ \{0\} \subseteq ran F) \to ran F ∖ \{0\} \in Fin$
4	1 2 3	sylancl	$⊢ F \in dom \int^{1} \to ran F ∖ \{0\} \in Fin$
5	4	adantr	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to ran F ∖ \{0\} \in Fin$
6		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
7	6	adantr	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to F : ℝ ⟶ ℝ$
8	7	frnd	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to ran F \subseteq ℝ$
9	8	ssdifssd	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to ran F ∖ \{0\} \subseteq ℝ$
10	9	sselda	$⊢ ((F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \land x \in (ran F ∖ \{0\})) \to x \in ℝ$
11		i1fima2sn	$⊢ (F \in dom \int^{1} \land x \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{x\}]) \in ℝ$
12	11	adantlr	$⊢ ((F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \land x \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{x\}]) \in ℝ$
13	10 12	remulcld	$⊢ ((F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \land x \in (ran F ∖ \{0\})) \to x vol (F^{-1} [\{x\}]) \in ℝ$
14		eldifi	$⊢ x \in (ran F ∖ \{0\}) \to x \in ran F$
15		0cn	$⊢ 0 \in ℂ$
16		fnconstg	$⊢ 0 \in ℂ \to (ℂ \times \{0\}) Fn ℂ$
17	15 16	ax-mp	$⊢ (ℂ \times \{0\}) Fn ℂ$
18		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
19	18	fneq1i	$⊢ 0_{𝑝} Fn ℂ \leftrightarrow (ℂ \times \{0\}) Fn ℂ$
20	17 19	mpbir	$⊢ 0_{𝑝} Fn ℂ$
21	20	a1i	$⊢ F \in dom \int^{1} \to 0_{𝑝} Fn ℂ$
22	6	ffnd	$⊢ F \in dom \int^{1} \to F Fn ℝ$
23		cnex	$⊢ ℂ \in V$
24	23	a1i	$⊢ F \in dom \int^{1} \to ℂ \in V$
25		reex	$⊢ ℝ \in V$
26	25	a1i	$⊢ F \in dom \int^{1} \to ℝ \in V$
27		ax-resscn	$⊢ ℝ \subseteq ℂ$
28		sseqin2	$⊢ ℝ \subseteq ℂ \leftrightarrow ℂ \cap ℝ = ℝ$
29	27 28	mpbi	$⊢ ℂ \cap ℝ = ℝ$
30		0pval	$⊢ y \in ℂ \to 0_{𝑝} (y) = 0$
31	30	adantl	$⊢ (F \in dom \int^{1} \land y \in ℂ) \to 0_{𝑝} (y) = 0$
32		eqidd	$⊢ (F \in dom \int^{1} \land y \in ℝ) \to F (y) = F (y)$
33	21 22 24 26 29 31 32	ofrfval	$⊢ F \in dom \int^{1} \to (0_{𝑝} \leq_{f} F \leftrightarrow \forall y \in ℝ 0 \leq F (y))$
34	33	biimpa	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to \forall y \in ℝ 0 \leq F (y)$
35	22	adantr	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to F Fn ℝ$
36		breq2	$⊢ x = F (y) \to (0 \leq x \leftrightarrow 0 \leq F (y))$
37	36	ralrn	$⊢ F Fn ℝ \to (\forall x \in ran F 0 \leq x \leftrightarrow \forall y \in ℝ 0 \leq F (y))$
38	35 37	syl	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to (\forall x \in ran F 0 \leq x \leftrightarrow \forall y \in ℝ 0 \leq F (y))$
39	34 38	mpbird	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to \forall x \in ran F 0 \leq x$
40	39	r19.21bi	$⊢ ((F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \land x \in ran F) \to 0 \leq x$
41	14 40	sylan2	$⊢ ((F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \land x \in (ran F ∖ \{0\})) \to 0 \leq x$
42		i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [\{x\}] \in dom vol$
43	42	ad2antrr	$⊢ ((F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \land x \in (ran F ∖ \{0\})) \to F^{-1} [\{x\}] \in dom vol$
44		mblss	$⊢ F^{-1} [\{x\}] \in dom vol \to F^{-1} [\{x\}] \subseteq ℝ$
45		ovolge0	$⊢ F^{-1} [\{x\}] \subseteq ℝ \to 0 \leq {vol}^{*} (F^{-1} [\{x\}])$
46	44 45	syl	$⊢ F^{-1} [\{x\}] \in dom vol \to 0 \leq {vol}^{*} (F^{-1} [\{x\}])$
47		mblvol	$⊢ F^{-1} [\{x\}] \in dom vol \to vol (F^{-1} [\{x\}]) = {vol}^{*} (F^{-1} [\{x\}])$
48	46 47	breqtrrd	$⊢ F^{-1} [\{x\}] \in dom vol \to 0 \leq vol (F^{-1} [\{x\}])$
49	43 48	syl	$⊢ ((F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \land x \in (ran F ∖ \{0\})) \to 0 \leq vol (F^{-1} [\{x\}])$
50	10 12 41 49	mulge0d	$⊢ ((F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \land x \in (ran F ∖ \{0\})) \to 0 \leq x vol (F^{-1} [\{x\}])$
51	5 13 50	fsumge0	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to 0 \leq \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}])$
52		itg1val	$⊢ F \in dom \int^{1} \to \int^{1} (F) = \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}])$
53	52	adantr	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to \int^{1} (F) = \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}])$
54	51 53	breqtrrd	$⊢ (F \in dom \int^{1} \land 0_{𝑝} \leq_{f} F) \to 0 \leq \int^{1} (F)$

Metamath Proof Explorer

Theorem itg1ge0

Proof