i1fima2

Description: Any preimage of a simple function not containing zero has finite measure. (Contributed by Mario Carneiro, 26-Jun-2014)

		Ref	Expression
	Assertion	i1fima2	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to vol (F^{-1} [A]) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [A] \in dom vol$
2	1	adantr	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to F^{-1} [A] \in dom vol$
3		mblvol	$⊢ F^{-1} [A] \in dom vol \to vol (F^{-1} [A]) = {vol}^{*} (F^{-1} [A])$
4	2 3	syl	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to vol (F^{-1} [A]) = {vol}^{*} (F^{-1} [A])$
5		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
6	5	adantr	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to F : ℝ ⟶ ℝ$
7		ffun	$⊢ F : ℝ ⟶ ℝ \to Fun F$
8		inpreima	$⊢ Fun F \to F^{-1} [A \cap ran F] = F^{-1} [A] \cap F^{-1} [ran F]$
9	6 7 8	3syl	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to F^{-1} [A \cap ran F] = F^{-1} [A] \cap F^{-1} [ran F]$
10		cnvimass	$⊢ F^{-1} [A] \subseteq dom F$
11		cnvimarndm	$⊢ F^{-1} [ran F] = dom F$
12	10 11	sseqtrri	$⊢ F^{-1} [A] \subseteq F^{-1} [ran F]$
13		dfss2	$⊢ F^{-1} [A] \subseteq F^{-1} [ran F] \leftrightarrow F^{-1} [A] \cap F^{-1} [ran F] = F^{-1} [A]$
14	12 13	mpbi	$⊢ F^{-1} [A] \cap F^{-1} [ran F] = F^{-1} [A]$
15	9 14	eqtr2di	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to F^{-1} [A] = F^{-1} [A \cap ran F]$
16		elinel1	$⊢ 0 \in (A \cap ran F) \to 0 \in A$
17	16	con3i	$⊢ \neg 0 \in A \to \neg 0 \in (A \cap ran F)$
18	17	adantl	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to \neg 0 \in (A \cap ran F)$
19		disjsn	$⊢ (A \cap ran F) \cap \{0\} = \emptyset \leftrightarrow \neg 0 \in (A \cap ran F)$
20	18 19	sylibr	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to (A \cap ran F) \cap \{0\} = \emptyset$
21		inss2	$⊢ A \cap ran F \subseteq ran F$
22	5	frnd	$⊢ F \in dom \int^{1} \to ran F \subseteq ℝ$
23	21 22	sstrid	$⊢ F \in dom \int^{1} \to A \cap ran F \subseteq ℝ$
24	23	adantr	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to A \cap ran F \subseteq ℝ$
25		reldisj	$⊢ A \cap ran F \subseteq ℝ \to ((A \cap ran F) \cap \{0\} = \emptyset \leftrightarrow A \cap ran F \subseteq ℝ ∖ \{0\})$
26	24 25	syl	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to ((A \cap ran F) \cap \{0\} = \emptyset \leftrightarrow A \cap ran F \subseteq ℝ ∖ \{0\})$
27	20 26	mpbid	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to A \cap ran F \subseteq ℝ ∖ \{0\}$
28		imass2	$⊢ A \cap ran F \subseteq ℝ ∖ \{0\} \to F^{-1} [A \cap ran F] \subseteq F^{-1} [ℝ ∖ \{0\}]$
29	27 28	syl	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to F^{-1} [A \cap ran F] \subseteq F^{-1} [ℝ ∖ \{0\}]$
30	15 29	eqsstrd	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to F^{-1} [A] \subseteq F^{-1} [ℝ ∖ \{0\}]$
31		i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [ℝ ∖ \{0\}] \in dom vol$
32	31	adantr	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to F^{-1} [ℝ ∖ \{0\}] \in dom vol$
33		mblss	$⊢ F^{-1} [ℝ ∖ \{0\}] \in dom vol \to F^{-1} [ℝ ∖ \{0\}] \subseteq ℝ$
34	32 33	syl	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to F^{-1} [ℝ ∖ \{0\}] \subseteq ℝ$
35		mblvol	$⊢ F^{-1} [ℝ ∖ \{0\}] \in dom vol \to vol (F^{-1} [ℝ ∖ \{0\}]) = {vol}^{*} (F^{-1} [ℝ ∖ \{0\}])$
36	32 35	syl	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to vol (F^{-1} [ℝ ∖ \{0\}]) = {vol}^{*} (F^{-1} [ℝ ∖ \{0\}])$
37		isi1f	$⊢ F \in dom \int^{1} \leftrightarrow (F \in MblFn \land (F : ℝ ⟶ ℝ \land ran F \in Fin \land vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ))$
38	37	simprbi	$⊢ F \in dom \int^{1} \to (F : ℝ ⟶ ℝ \land ran F \in Fin \land vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ)$
39	38	simp3d	$⊢ F \in dom \int^{1} \to vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ$
40	39	adantr	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ$
41	36 40	eqeltrrd	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to {vol}^{*} (F^{-1} [ℝ ∖ \{0\}]) \in ℝ$
42		ovolsscl	$⊢ (F^{-1} [A] \subseteq F^{-1} [ℝ ∖ \{0\}] \land F^{-1} [ℝ ∖ \{0\}] \subseteq ℝ \land {vol}^{} (F^{-1} [ℝ ∖ \{0\}]) \in ℝ) \to {vol}^{} (F^{-1} [A]) \in ℝ$
43	30 34 41 42	syl3anc	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to {vol}^{*} (F^{-1} [A]) \in ℝ$
44	4 43	eqeltrd	$⊢ (F \in dom \int^{1} \land \neg 0 \in A) \to vol (F^{-1} [A]) \in ℝ$

Metamath Proof Explorer

Theorem i1fima2

Proof