itg11

Description: The integral of an indicator function is the volume of the set. (Contributed by Mario Carneiro, 18-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

		Ref	Expression
	Hypothesis	i1f1.1	$⊢ F = (x \in ℝ ⟼ if (x \in A, 1, 0))$
	Assertion	itg11	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to \int^{1} (F) = vol (A)$

Proof

Step	Hyp	Ref	Expression
1		i1f1.1	$⊢ F = (x \in ℝ ⟼ if (x \in A, 1, 0))$
2		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
3		0mbl	$⊢ \emptyset \in dom vol$
4		mblvol	$⊢ \emptyset \in dom vol \to vol (\emptyset) = {vol}^{*} (\emptyset)$
5	3 4	ax-mp	$⊢ vol (\emptyset) = {vol}^{*} (\emptyset)$
6		itg10	$⊢ \int^{1} (ℝ \times \{0\}) = 0$
7	2 5 6	3eqtr4ri	$⊢ \int^{1} (ℝ \times \{0\}) = vol (\emptyset)$
8		noel	$⊢ \neg x \in \emptyset$
9		eleq2	$⊢ A = \emptyset \to (x \in A \leftrightarrow x \in \emptyset)$
10	8 9	mtbiri	$⊢ A = \emptyset \to \neg x \in A$
11	10	iffalsed	$⊢ A = \emptyset \to if (x \in A, 1, 0) = 0$
12	11	mpteq2dv	$⊢ A = \emptyset \to (x \in ℝ ⟼ if (x \in A, 1, 0)) = (x \in ℝ ⟼ 0)$
13		fconstmpt	$⊢ ℝ \times \{0\} = (x \in ℝ ⟼ 0)$
14	12 1 13	3eqtr4g	$⊢ A = \emptyset \to F = ℝ \times \{0\}$
15	14	fveq2d	$⊢ A = \emptyset \to \int^{1} (F) = \int^{1} (ℝ \times \{0\})$
16		fveq2	$⊢ A = \emptyset \to vol (A) = vol (\emptyset)$
17	7 15 16	3eqtr4a	$⊢ A = \emptyset \to \int^{1} (F) = vol (A)$
18	17	a1i	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to (A = \emptyset \to \int^{1} (F) = vol (A))$
19		n0	$⊢ A \neq \emptyset \leftrightarrow \exists y y \in A$
20	1	i1f1	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to F \in dom \int^{1}$
21	20	adantr	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to F \in dom \int^{1}$
22		itg1val	$⊢ F \in dom \int^{1} \to \int^{1} (F) = \sum_{z \in ran F ∖ \{0\}} z vol (F^{-1} [\{z\}])$
23	21 22	syl	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to \int^{1} (F) = \sum_{z \in ran F ∖ \{0\}} z vol (F^{-1} [\{z\}])$
24	1	i1f1lem	$⊢ (F : ℝ ⟶ \{0, 1\} \land (A \in dom vol \to F^{-1} [\{1\}] = A))$
25	24	simpli	$⊢ F : ℝ ⟶ \{0, 1\}$
26		frn	$⊢ F : ℝ ⟶ \{0, 1\} \to ran F \subseteq \{0, 1\}$
27	25 26	ax-mp	$⊢ ran F \subseteq \{0, 1\}$
28		ssdif	$⊢ ran F \subseteq \{0, 1\} \to ran F ∖ \{0\} \subseteq \{0, 1\} ∖ \{0\}$
29	27 28	ax-mp	$⊢ ran F ∖ \{0\} \subseteq \{0, 1\} ∖ \{0\}$
30		difprsnss	$⊢ \{0, 1\} ∖ \{0\} \subseteq \{1\}$
31	29 30	sstri	$⊢ ran F ∖ \{0\} \subseteq \{1\}$
32	31	a1i	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to ran F ∖ \{0\} \subseteq \{1\}$
33		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
34	33	adantr	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to A \subseteq ℝ$
35	34	sselda	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to y \in ℝ$
36		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
37	36	ifbid	$⊢ x = y \to if (x \in A, 1, 0) = if (y \in A, 1, 0)$
38		1ex	$⊢ 1 \in V$
39		c0ex	$⊢ 0 \in V$
40	38 39	ifex	$⊢ if (y \in A, 1, 0) \in V$
41	37 1 40	fvmpt	$⊢ y \in ℝ \to F (y) = if (y \in A, 1, 0)$
42	35 41	syl	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to F (y) = if (y \in A, 1, 0)$
43		iftrue	$⊢ y \in A \to if (y \in A, 1, 0) = 1$
44	43	adantl	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to if (y \in A, 1, 0) = 1$
45	42 44	eqtrd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to F (y) = 1$
46		ffn	$⊢ F : ℝ ⟶ \{0, 1\} \to F Fn ℝ$
47	25 46	ax-mp	$⊢ F Fn ℝ$
48		fnfvelrn	$⊢ (F Fn ℝ \land y \in ℝ) \to F (y) \in ran F$
49	47 35 48	sylancr	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to F (y) \in ran F$
50	45 49	eqeltrrd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to 1 \in ran F$
51		ax-1ne0	$⊢ 1 \neq 0$
52		eldifsn	$⊢ 1 \in (ran F ∖ \{0\}) \leftrightarrow (1 \in ran F \land 1 \neq 0)$
53	50 51 52	sylanblrc	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to 1 \in (ran F ∖ \{0\})$
54	53	snssd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to \{1\} \subseteq ran F ∖ \{0\}$
55	32 54	eqssd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to ran F ∖ \{0\} = \{1\}$
56	55	sumeq1d	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to \sum_{z \in ran F ∖ \{0\}} z vol (F^{-1} [\{z\}]) = \sum_{z \in \{1\}} z vol (F^{-1} [\{z\}])$
57		1re	$⊢ 1 \in ℝ$
58	24	simpri	$⊢ A \in dom vol \to F^{-1} [\{1\}] = A$
59	58	ad2antrr	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to F^{-1} [\{1\}] = A$
60	59	fveq2d	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to vol (F^{-1} [\{1\}]) = vol (A)$
61	60	oveq2d	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to 1 vol (F^{-1} [\{1\}]) = 1 vol (A)$
62		simplr	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to vol (A) \in ℝ$
63	62	recnd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to vol (A) \in ℂ$
64	63	mulid2d	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to 1 vol (A) = vol (A)$
65	61 64	eqtrd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to 1 vol (F^{-1} [\{1\}]) = vol (A)$
66	65 63	eqeltrd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to 1 vol (F^{-1} [\{1\}]) \in ℂ$
67		id	$⊢ z = 1 \to z = 1$
68		sneq	$⊢ z = 1 \to \{z\} = \{1\}$
69	68	imaeq2d	$⊢ z = 1 \to F^{-1} [\{z\}] = F^{-1} [\{1\}]$
70	69	fveq2d	$⊢ z = 1 \to vol (F^{-1} [\{z\}]) = vol (F^{-1} [\{1\}])$
71	67 70	oveq12d	$⊢ z = 1 \to z vol (F^{-1} [\{z\}]) = 1 vol (F^{-1} [\{1\}])$
72	71	sumsn	$⊢ (1 \in ℝ \land 1 vol (F^{-1} [\{1\}]) \in ℂ) \to \sum_{z \in \{1\}} z vol (F^{-1} [\{z\}]) = 1 vol (F^{-1} [\{1\}])$
73	57 66 72	sylancr	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to \sum_{z \in \{1\}} z vol (F^{-1} [\{z\}]) = 1 vol (F^{-1} [\{1\}])$
74	73 65	eqtrd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to \sum_{z \in \{1\}} z vol (F^{-1} [\{z\}]) = vol (A)$
75	56 74	eqtrd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to \sum_{z \in ran F ∖ \{0\}} z vol (F^{-1} [\{z\}]) = vol (A)$
76	23 75	eqtrd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in A) \to \int^{1} (F) = vol (A)$
77	76	ex	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to (y \in A \to \int^{1} (F) = vol (A))$
78	77	exlimdv	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to (\exists y y \in A \to \int^{1} (F) = vol (A))$
79	19 78	syl5bi	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to (A \neq \emptyset \to \int^{1} (F) = vol (A))$
80	18 79	pm2.61dne	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to \int^{1} (F) = vol (A)$

Metamath Proof Explorer

Theorem itg11

Proof