i1fres

Description: The "restriction" of a simple function to a measurable subset is simple. (It's not actually a restriction because it is zero instead of undefined outside A .) (Contributed by Mario Carneiro, 29-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		i1fres.1	$⊢ G = (x \in ℝ ⟼ if (x \in A, F (x), 0))$
2		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
3	2	adantr	$⊢ (F \in dom \int^{1} \land A \in dom vol) \to F : ℝ ⟶ ℝ$
4	3	ffnd	$⊢ (F \in dom \int^{1} \land A \in dom vol) \to F Fn ℝ$
5		fnfvelrn	$⊢ (F Fn ℝ \land x \in ℝ) \to F (x) \in ran F$
6	4 5	sylan	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land x \in ℝ) \to F (x) \in ran F$
7		i1f0rn	$⊢ F \in dom \int^{1} \to 0 \in ran F$
8	7	ad2antrr	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land x \in ℝ) \to 0 \in ran F$
9	6 8	ifcld	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land x \in ℝ) \to if (x \in A, F (x), 0) \in ran F$
10	9 1	fmptd	$⊢ (F \in dom \int^{1} \land A \in dom vol) \to G : ℝ ⟶ ran F$
11	3	frnd	$⊢ (F \in dom \int^{1} \land A \in dom vol) \to ran F \subseteq ℝ$
12	10 11	fssd	$⊢ (F \in dom \int^{1} \land A \in dom vol) \to G : ℝ ⟶ ℝ$
13		i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$
14	13	adantr	$⊢ (F \in dom \int^{1} \land A \in dom vol) \to ran F \in Fin$
15	10	frnd	$⊢ (F \in dom \int^{1} \land A \in dom vol) \to ran G \subseteq ran F$
16	14 15	ssfid	$⊢ (F \in dom \int^{1} \land A \in dom vol) \to ran G \in Fin$
17		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
18		fveq2	$⊢ x = z \to F (x) = F (z)$
19	17 18	ifbieq1d	$⊢ x = z \to if (x \in A, F (x), 0) = if (z \in A, F (z), 0)$
20		fvex	$⊢ F (z) \in V$
21		c0ex	$⊢ 0 \in V$
22	20 21	ifex	$⊢ if (z \in A, F (z), 0) \in V$
23	19 1 22	fvmpt	$⊢ z \in ℝ \to G (z) = if (z \in A, F (z), 0)$
24	23	adantl	$⊢ (((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \land z \in ℝ) \to G (z) = if (z \in A, F (z), 0)$
25	24	eqeq1d	$⊢ (((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \land z \in ℝ) \to (G (z) = y \leftrightarrow if (z \in A, F (z), 0) = y)$
26		eldifsni	$⊢ y \in (ran G ∖ \{0\}) \to y \neq 0$
27	26	ad2antlr	$⊢ (((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \land z \in ℝ) \to y \neq 0$
28	27	necomd	$⊢ (((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \land z \in ℝ) \to 0 \neq y$
29		iffalse	$⊢ \neg z \in A \to if (z \in A, F (z), 0) = 0$
30	29	neeq1d	$⊢ \neg z \in A \to (if (z \in A, F (z), 0) \neq y \leftrightarrow 0 \neq y)$
31	28 30	syl5ibrcom	$⊢ (((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \land z \in ℝ) \to (\neg z \in A \to if (z \in A, F (z), 0) \neq y)$
32	31	necon4bd	$⊢ (((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \land z \in ℝ) \to (if (z \in A, F (z), 0) = y \to z \in A)$
33	32	pm4.71rd	$⊢ (((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \land z \in ℝ) \to (if (z \in A, F (z), 0) = y \leftrightarrow (z \in A \land if (z \in A, F (z), 0) = y))$
34	25 33	bitrd	$⊢ (((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \land z \in ℝ) \to (G (z) = y \leftrightarrow (z \in A \land if (z \in A, F (z), 0) = y))$
35		iftrue	$⊢ z \in A \to if (z \in A, F (z), 0) = F (z)$
36	35	eqeq1d	$⊢ z \in A \to (if (z \in A, F (z), 0) = y \leftrightarrow F (z) = y)$
37	36	pm5.32i	$⊢ (z \in A \land if (z \in A, F (z), 0) = y) \leftrightarrow (z \in A \land F (z) = y)$
38	34 37	bitrdi	$⊢ (((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \land z \in ℝ) \to (G (z) = y \leftrightarrow (z \in A \land F (z) = y))$
39	38	pm5.32da	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to ((z \in ℝ \land G (z) = y) \leftrightarrow (z \in ℝ \land (z \in A \land F (z) = y)))$
40		an12	$⊢ (z \in ℝ \land (z \in A \land F (z) = y)) \leftrightarrow (z \in A \land (z \in ℝ \land F (z) = y))$
41	39 40	bitrdi	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to ((z \in ℝ \land G (z) = y) \leftrightarrow (z \in A \land (z \in ℝ \land F (z) = y)))$
42	10	ffnd	$⊢ (F \in dom \int^{1} \land A \in dom vol) \to G Fn ℝ$
43	42	adantr	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to G Fn ℝ$
44		fniniseg	$⊢ G Fn ℝ \to (z \in G^{-1} [\{y\}] \leftrightarrow (z \in ℝ \land G (z) = y))$
45	43 44	syl	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to (z \in G^{-1} [\{y\}] \leftrightarrow (z \in ℝ \land G (z) = y))$
46	4	adantr	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to F Fn ℝ$
47		fniniseg	$⊢ F Fn ℝ \to (z \in F^{-1} [\{y\}] \leftrightarrow (z \in ℝ \land F (z) = y))$
48	46 47	syl	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to (z \in F^{-1} [\{y\}] \leftrightarrow (z \in ℝ \land F (z) = y))$
49	48	anbi2d	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to ((z \in A \land z \in F^{-1} [\{y\}]) \leftrightarrow (z \in A \land (z \in ℝ \land F (z) = y)))$
50	41 45 49	3bitr4d	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to (z \in G^{-1} [\{y\}] \leftrightarrow (z \in A \land z \in F^{-1} [\{y\}]))$
51		elin	$⊢ z \in (A \cap F^{-1} [\{y\}]) \leftrightarrow (z \in A \land z \in F^{-1} [\{y\}])$
52	50 51	bitr4di	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to (z \in G^{-1} [\{y\}] \leftrightarrow z \in (A \cap F^{-1} [\{y\}]))$
53	52	eqrdv	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to G^{-1} [\{y\}] = A \cap F^{-1} [\{y\}]$
54		simplr	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to A \in dom vol$
55		i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [\{y\}] \in dom vol$
56	55	ad2antrr	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to F^{-1} [\{y\}] \in dom vol$
57		inmbl	$⊢ (A \in dom vol \land F^{-1} [\{y\}] \in dom vol) \to A \cap F^{-1} [\{y\}] \in dom vol$
58	54 56 57	syl2anc	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to A \cap F^{-1} [\{y\}] \in dom vol$
59	53 58	eqeltrd	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to G^{-1} [\{y\}] \in dom vol$
60	53	fveq2d	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to vol (G^{-1} [\{y\}]) = vol (A \cap F^{-1} [\{y\}])$
61		mblvol	$⊢ A \cap F^{-1} [\{y\}] \in dom vol \to vol (A \cap F^{-1} [\{y\}]) = {vol}^{*} (A \cap F^{-1} [\{y\}])$
62	58 61	syl	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to vol (A \cap F^{-1} [\{y\}]) = {vol}^{*} (A \cap F^{-1} [\{y\}])$
63	60 62	eqtrd	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to vol (G^{-1} [\{y\}]) = {vol}^{*} (A \cap F^{-1} [\{y\}])$
64		inss2	$⊢ A \cap F^{-1} [\{y\}] \subseteq F^{-1} [\{y\}]$
65		mblss	$⊢ F^{-1} [\{y\}] \in dom vol \to F^{-1} [\{y\}] \subseteq ℝ$
66	56 65	syl	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to F^{-1} [\{y\}] \subseteq ℝ$
67		mblvol	$⊢ F^{-1} [\{y\}] \in dom vol \to vol (F^{-1} [\{y\}]) = {vol}^{*} (F^{-1} [\{y\}])$
68	56 67	syl	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to vol (F^{-1} [\{y\}]) = {vol}^{*} (F^{-1} [\{y\}])$
69		i1fima2sn	$⊢ (F \in dom \int^{1} \land y \in (ran G ∖ \{0\})) \to vol (F^{-1} [\{y\}]) \in ℝ$
70	69	adantlr	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to vol (F^{-1} [\{y\}]) \in ℝ$
71	68 70	eqeltrrd	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to {vol}^{*} (F^{-1} [\{y\}]) \in ℝ$
72		ovolsscl	$⊢ (A \cap F^{-1} [\{y\}] \subseteq F^{-1} [\{y\}] \land F^{-1} [\{y\}] \subseteq ℝ \land {vol}^{} (F^{-1} [\{y\}]) \in ℝ) \to {vol}^{} (A \cap F^{-1} [\{y\}]) \in ℝ$
73	64 66 71 72	mp3an2i	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to {vol}^{*} (A \cap F^{-1} [\{y\}]) \in ℝ$
74	63 73	eqeltrd	$⊢ ((F \in dom \int^{1} \land A \in dom vol) \land y \in (ran G ∖ \{0\})) \to vol (G^{-1} [\{y\}]) \in ℝ$
75	12 16 59 74	i1fd	$⊢ (F \in dom \int^{1} \land A \in dom vol) \to G \in dom \int^{1}$

Metamath Proof Explorer

Theorem i1fres

Proof