i1f1

Description: Base case simple functions are indicator functions of measurable sets. (Contributed by Mario Carneiro, 18-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		i1f1.1	$⊢ F = (x \in ℝ ⟼ if (x \in A, 1, 0))$
2	1	i1f1lem	$⊢ (F : ℝ ⟶ \{0, 1\} \land (A \in dom vol \to F^{-1} [\{1\}] = A))$
3	2	simpli	$⊢ F : ℝ ⟶ \{0, 1\}$
4		0re	$⊢ 0 \in ℝ$
5		1re	$⊢ 1 \in ℝ$
6		prssi	$⊢ (0 \in ℝ \land 1 \in ℝ) \to \{0, 1\} \subseteq ℝ$
7	4 5 6	mp2an	$⊢ \{0, 1\} \subseteq ℝ$
8		fss	$⊢ (F : ℝ ⟶ \{0, 1\} \land \{0, 1\} \subseteq ℝ) \to F : ℝ ⟶ ℝ$
9	3 7 8	mp2an	$⊢ F : ℝ ⟶ ℝ$
10	9	a1i	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to F : ℝ ⟶ ℝ$
11		prfi	$⊢ \{0, 1\} \in Fin$
12		1elpr01	$⊢ 1 \in \{0, 1\}$
13		0elpr01	$⊢ 0 \in \{0, 1\}$
14	12 13	ifcli	$⊢ if (x \in A, 1, 0) \in \{0, 1\}$
15	14	a1i	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land x \in ℝ) \to if (x \in A, 1, 0) \in \{0, 1\}$
16	15 1	fmptd	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to F : ℝ ⟶ \{0, 1\}$
17		frn	$⊢ F : ℝ ⟶ \{0, 1\} \to ran F \subseteq \{0, 1\}$
18	16 17	syl	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to ran F \subseteq \{0, 1\}$
19		ssfi	$⊢ (\{0, 1\} \in Fin \land ran F \subseteq \{0, 1\}) \to ran F \in Fin$
20	11 18 19	sylancr	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to ran F \in Fin$
21	3 17	ax-mp	$⊢ ran F \subseteq \{0, 1\}$
22		df-pr	$⊢ \{0, 1\} = \{0\} \cup \{1\}$
23	22	equncomi	$⊢ \{0, 1\} = \{1\} \cup \{0\}$
24	21 23	sseqtri	$⊢ ran F \subseteq \{1\} \cup \{0\}$
25		ssdif	$⊢ ran F \subseteq \{1\} \cup \{0\} \to ran F ∖ \{0\} \subseteq (\{1\} \cup \{0\}) ∖ \{0\}$
26	24 25	ax-mp	$⊢ ran F ∖ \{0\} \subseteq (\{1\} \cup \{0\}) ∖ \{0\}$
27		difun2	$⊢ (\{1\} \cup \{0\}) ∖ \{0\} = \{1\} ∖ \{0\}$
28		difss	$⊢ \{1\} ∖ \{0\} \subseteq \{1\}$
29	27 28	eqsstri	$⊢ (\{1\} \cup \{0\}) ∖ \{0\} \subseteq \{1\}$
30	26 29	sstri	$⊢ ran F ∖ \{0\} \subseteq \{1\}$
31	30	sseli	$⊢ y \in (ran F ∖ \{0\}) \to y \in \{1\}$
32		elsni	$⊢ y \in \{1\} \to y = 1$
33	31 32	syl	$⊢ y \in (ran F ∖ \{0\}) \to y = 1$
34	33	sneqd	$⊢ y \in (ran F ∖ \{0\}) \to \{y\} = \{1\}$
35	34	imaeq2d	$⊢ y \in (ran F ∖ \{0\}) \to F^{-1} [\{y\}] = F^{-1} [\{1\}]$
36	2	simpri	$⊢ A \in dom vol \to F^{-1} [\{1\}] = A$
37	36	adantr	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to F^{-1} [\{1\}] = A$
38	35 37	sylan9eqr	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in (ran F ∖ \{0\})) \to F^{-1} [\{y\}] = A$
39		simpll	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in (ran F ∖ \{0\})) \to A \in dom vol$
40	38 39	eqeltrd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in (ran F ∖ \{0\})) \to F^{-1} [\{y\}] \in dom vol$
41	38	fveq2d	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{y\}]) = vol (A)$
42		simplr	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in (ran F ∖ \{0\})) \to vol (A) \in ℝ$
43	41 42	eqeltrd	$⊢ ((A \in dom vol \land vol (A) \in ℝ) \land y \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{y\}]) \in ℝ$
44	10 20 40 43	i1fd	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to F \in dom \int^{1}$

Metamath Proof Explorer

Theorem i1f1

Proof