i1fd

Description: A simplified set of assumptions to show that a given function is simple. (Contributed by Mario Carneiro, 26-Jun-2014)

	Ref	Expression
Hypotheses	i1fd.1	$⊢ φ \to F : ℝ ⟶ ℝ$
	i1fd.2	$⊢ φ \to ran F \in Fin$
	i1fd.3	$⊢ (φ \land x \in (ran F ∖ \{0\})) \to F^{-1} [\{x\}] \in dom vol$
	i1fd.4	$⊢ (φ \land x \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{x\}]) \in ℝ$
Assertion	i1fd	$⊢ φ \to F \in dom \int^{1}$

Proof

Step	Hyp	Ref	Expression
1		i1fd.1	$⊢ φ \to F : ℝ ⟶ ℝ$
2		i1fd.2	$⊢ φ \to ran F \in Fin$
3		i1fd.3	$⊢ (φ \land x \in (ran F ∖ \{0\})) \to F^{-1} [\{x\}] \in dom vol$
4		i1fd.4	$⊢ (φ \land x \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{x\}]) \in ℝ$
5	1	ad2antrr	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to F : ℝ ⟶ ℝ$
6		ffun	$⊢ F : ℝ ⟶ ℝ \to Fun F$
7		funcnvcnv	$⊢ Fun F \to Fun {F^{-1}}^{-1}$
8		imadif	$⊢ Fun {F^{-1}}^{-1} \to F^{-1} [ℝ ∖ (ℝ ∖ x)] = F^{-1} [ℝ] ∖ F^{-1} [ℝ ∖ x]$
9	5 6 7 8	4syl	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to F^{-1} [ℝ ∖ (ℝ ∖ x)] = F^{-1} [ℝ] ∖ F^{-1} [ℝ ∖ x]$
10		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
11		frn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to ran (.) \subseteq 𝒫 ℝ$
12	10 11	ax-mp	$⊢ ran (.) \subseteq 𝒫 ℝ$
13	12	sseli	$⊢ x \in ran (.) \to x \in 𝒫 ℝ$
14	13	elpwid	$⊢ x \in ran (.) \to x \subseteq ℝ$
15	14	ad2antlr	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to x \subseteq ℝ$
16		dfss4	$⊢ x \subseteq ℝ \leftrightarrow ℝ ∖ (ℝ ∖ x) = x$
17	15 16	sylib	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to ℝ ∖ (ℝ ∖ x) = x$
18	17	imaeq2d	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to F^{-1} [ℝ ∖ (ℝ ∖ x)] = F^{-1} [x]$
19	9 18	eqtr3d	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to F^{-1} [ℝ] ∖ F^{-1} [ℝ ∖ x] = F^{-1} [x]$
20		fimacnv	$⊢ F : ℝ ⟶ ℝ \to F^{-1} [ℝ] = ℝ$
21	5 20	syl	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to F^{-1} [ℝ] = ℝ$
22		rembl	$⊢ ℝ \in dom vol$
23	21 22	eqeltrdi	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to F^{-1} [ℝ] \in dom vol$
24	1	adantr	$⊢ (φ \land \neg 0 \in y) \to F : ℝ ⟶ ℝ$
25		inpreima	$⊢ Fun F \to F^{-1} [y \cap ran F] = F^{-1} [y] \cap F^{-1} [ran F]$
26		iunid	$⊢ ⋃_{x \in y \cap ran F} \{x\} = y \cap ran F$
27	26	imaeq2i	$⊢ F^{-1} [⋃_{x \in y \cap ran F} \{x\}] = F^{-1} [y \cap ran F]$
28		imaiun	$⊢ F^{-1} [⋃_{x \in y \cap ran F} \{x\}] = ⋃_{x \in y \cap ran F} F^{-1} [\{x\}]$
29	27 28	eqtr3i	$⊢ F^{-1} [y \cap ran F] = ⋃_{x \in y \cap ran F} F^{-1} [\{x\}]$
30		cnvimass	$⊢ F^{-1} [y] \subseteq dom F$
31		cnvimarndm	$⊢ F^{-1} [ran F] = dom F$
32	30 31	sseqtrri	$⊢ F^{-1} [y] \subseteq F^{-1} [ran F]$
33		dfss2	$⊢ F^{-1} [y] \subseteq F^{-1} [ran F] \leftrightarrow F^{-1} [y] \cap F^{-1} [ran F] = F^{-1} [y]$
34	32 33	mpbi	$⊢ F^{-1} [y] \cap F^{-1} [ran F] = F^{-1} [y]$
35	25 29 34	3eqtr3g	$⊢ Fun F \to ⋃_{x \in y \cap ran F} F^{-1} [\{x\}] = F^{-1} [y]$
36	24 6 35	3syl	$⊢ (φ \land \neg 0 \in y) \to ⋃_{x \in y \cap ran F} F^{-1} [\{x\}] = F^{-1} [y]$
37	2	adantr	$⊢ (φ \land \neg 0 \in y) \to ran F \in Fin$
38		inss2	$⊢ y \cap ran F \subseteq ran F$
39		ssfi	$⊢ (ran F \in Fin \land y \cap ran F \subseteq ran F) \to y \cap ran F \in Fin$
40	37 38 39	sylancl	$⊢ (φ \land \neg 0 \in y) \to y \cap ran F \in Fin$
41		simpll	$⊢ ((φ \land \neg 0 \in y) \land x \in (y \cap ran F)) \to φ$
42		elinel1	$⊢ 0 \in (y \cap ran F) \to 0 \in y$
43	42	con3i	$⊢ \neg 0 \in y \to \neg 0 \in (y \cap ran F)$
44	43	adantl	$⊢ (φ \land \neg 0 \in y) \to \neg 0 \in (y \cap ran F)$
45		disjsn	$⊢ (y \cap ran F) \cap \{0\} = \emptyset \leftrightarrow \neg 0 \in (y \cap ran F)$
46	44 45	sylibr	$⊢ (φ \land \neg 0 \in y) \to (y \cap ran F) \cap \{0\} = \emptyset$
47		reldisj	$⊢ y \cap ran F \subseteq ran F \to ((y \cap ran F) \cap \{0\} = \emptyset \leftrightarrow y \cap ran F \subseteq ran F ∖ \{0\})$
48	38 47	ax-mp	$⊢ (y \cap ran F) \cap \{0\} = \emptyset \leftrightarrow y \cap ran F \subseteq ran F ∖ \{0\}$
49	46 48	sylib	$⊢ (φ \land \neg 0 \in y) \to y \cap ran F \subseteq ran F ∖ \{0\}$
50	49	sselda	$⊢ ((φ \land \neg 0 \in y) \land x \in (y \cap ran F)) \to x \in (ran F ∖ \{0\})$
51	41 50 3	syl2anc	$⊢ ((φ \land \neg 0 \in y) \land x \in (y \cap ran F)) \to F^{-1} [\{x\}] \in dom vol$
52	51	ralrimiva	$⊢ (φ \land \neg 0 \in y) \to \forall x \in (y \cap ran F) F^{-1} [\{x\}] \in dom vol$
53		finiunmbl	$⊢ (y \cap ran F \in Fin \land \forall x \in (y \cap ran F) F^{-1} [\{x\}] \in dom vol) \to ⋃_{x \in y \cap ran F} F^{-1} [\{x\}] \in dom vol$
54	40 52 53	syl2anc	$⊢ (φ \land \neg 0 \in y) \to ⋃_{x \in y \cap ran F} F^{-1} [\{x\}] \in dom vol$
55	36 54	eqeltrrd	$⊢ (φ \land \neg 0 \in y) \to F^{-1} [y] \in dom vol$
56	55	ex	$⊢ φ \to (\neg 0 \in y \to F^{-1} [y] \in dom vol)$
57	56	alrimiv	$⊢ φ \to \forall y (\neg 0 \in y \to F^{-1} [y] \in dom vol)$
58	57	ad2antrr	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to \forall y (\neg 0 \in y \to F^{-1} [y] \in dom vol)$
59		elndif	$⊢ 0 \in x \to \neg 0 \in (ℝ ∖ x)$
60	59	adantl	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to \neg 0 \in (ℝ ∖ x)$
61		reex	$⊢ ℝ \in V$
62	61	difexi	$⊢ ℝ ∖ x \in V$
63		eleq2	$⊢ y = ℝ ∖ x \to (0 \in y \leftrightarrow 0 \in (ℝ ∖ x))$
64	63	notbid	$⊢ y = ℝ ∖ x \to (\neg 0 \in y \leftrightarrow \neg 0 \in (ℝ ∖ x))$
65		imaeq2	$⊢ y = ℝ ∖ x \to F^{-1} [y] = F^{-1} [ℝ ∖ x]$
66	65	eleq1d	$⊢ y = ℝ ∖ x \to (F^{-1} [y] \in dom vol \leftrightarrow F^{-1} [ℝ ∖ x] \in dom vol)$
67	64 66	imbi12d	$⊢ y = ℝ ∖ x \to ((\neg 0 \in y \to F^{-1} [y] \in dom vol) \leftrightarrow (\neg 0 \in (ℝ ∖ x) \to F^{-1} [ℝ ∖ x] \in dom vol))$
68	62 67	spcv	$⊢ \forall y (\neg 0 \in y \to F^{-1} [y] \in dom vol) \to (\neg 0 \in (ℝ ∖ x) \to F^{-1} [ℝ ∖ x] \in dom vol)$
69	58 60 68	sylc	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to F^{-1} [ℝ ∖ x] \in dom vol$
70		difmbl	$⊢ (F^{-1} [ℝ] \in dom vol \land F^{-1} [ℝ ∖ x] \in dom vol) \to F^{-1} [ℝ] ∖ F^{-1} [ℝ ∖ x] \in dom vol$
71	23 69 70	syl2anc	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to F^{-1} [ℝ] ∖ F^{-1} [ℝ ∖ x] \in dom vol$
72	19 71	eqeltrrd	$⊢ ((φ \land x \in ran (.)) \land 0 \in x) \to F^{-1} [x] \in dom vol$
73		eleq2	$⊢ y = x \to (0 \in y \leftrightarrow 0 \in x)$
74	73	notbid	$⊢ y = x \to (\neg 0 \in y \leftrightarrow \neg 0 \in x)$
75		imaeq2	$⊢ y = x \to F^{-1} [y] = F^{-1} [x]$
76	75	eleq1d	$⊢ y = x \to (F^{-1} [y] \in dom vol \leftrightarrow F^{-1} [x] \in dom vol)$
77	74 76	imbi12d	$⊢ y = x \to ((\neg 0 \in y \to F^{-1} [y] \in dom vol) \leftrightarrow (\neg 0 \in x \to F^{-1} [x] \in dom vol))$
78	77	spvv	$⊢ \forall y (\neg 0 \in y \to F^{-1} [y] \in dom vol) \to (\neg 0 \in x \to F^{-1} [x] \in dom vol)$
79	57 78	syl	$⊢ φ \to (\neg 0 \in x \to F^{-1} [x] \in dom vol)$
80	79	imp	$⊢ (φ \land \neg 0 \in x) \to F^{-1} [x] \in dom vol$
81	80	adantlr	$⊢ ((φ \land x \in ran (.)) \land \neg 0 \in x) \to F^{-1} [x] \in dom vol$
82	72 81	pm2.61dan	$⊢ (φ \land x \in ran (.)) \to F^{-1} [x] \in dom vol$
83	82	ralrimiva	$⊢ φ \to \forall x \in ran (.) F^{-1} [x] \in dom vol$
84		ismbf	$⊢ F : ℝ ⟶ ℝ \to (F \in MblFn \leftrightarrow \forall x \in ran (.) F^{-1} [x] \in dom vol)$
85	1 84	syl	$⊢ φ \to (F \in MblFn \leftrightarrow \forall x \in ran (.) F^{-1} [x] \in dom vol)$
86	83 85	mpbird	$⊢ φ \to F \in MblFn$
87		mblvol	$⊢ F^{-1} [y] \in dom vol \to vol (F^{-1} [y]) = {vol}^{*} (F^{-1} [y])$
88	55 87	syl	$⊢ (φ \land \neg 0 \in y) \to vol (F^{-1} [y]) = {vol}^{*} (F^{-1} [y])$
89		mblss	$⊢ F^{-1} [y] \in dom vol \to F^{-1} [y] \subseteq ℝ$
90	55 89	syl	$⊢ (φ \land \neg 0 \in y) \to F^{-1} [y] \subseteq ℝ$
91		mblvol	$⊢ F^{-1} [\{x\}] \in dom vol \to vol (F^{-1} [\{x\}]) = {vol}^{*} (F^{-1} [\{x\}])$
92	51 91	syl	$⊢ ((φ \land \neg 0 \in y) \land x \in (y \cap ran F)) \to vol (F^{-1} [\{x\}]) = {vol}^{*} (F^{-1} [\{x\}])$
93	41 50 4	syl2anc	$⊢ ((φ \land \neg 0 \in y) \land x \in (y \cap ran F)) \to vol (F^{-1} [\{x\}]) \in ℝ$
94	92 93	eqeltrrd	$⊢ ((φ \land \neg 0 \in y) \land x \in (y \cap ran F)) \to {vol}^{*} (F^{-1} [\{x\}]) \in ℝ$
95	40 94	fsumrecl	$⊢ (φ \land \neg 0 \in y) \to \sum_{x \in y \cap ran F} {vol}^{*} (F^{-1} [\{x\}]) \in ℝ$
96	36	fveq2d	$⊢ (φ \land \neg 0 \in y) \to {vol}^{} (⋃_{x \in y \cap ran F} F^{-1} [\{x\}]) = {vol}^{} (F^{-1} [y])$
97		mblss	$⊢ F^{-1} [\{x\}] \in dom vol \to F^{-1} [\{x\}] \subseteq ℝ$
98	51 97	syl	$⊢ ((φ \land \neg 0 \in y) \land x \in (y \cap ran F)) \to F^{-1} [\{x\}] \subseteq ℝ$
99	98 94	jca	$⊢ ((φ \land \neg 0 \in y) \land x \in (y \cap ran F)) \to (F^{-1} [\{x\}] \subseteq ℝ \land {vol}^{*} (F^{-1} [\{x\}]) \in ℝ)$
100	99	ralrimiva	$⊢ (φ \land \neg 0 \in y) \to \forall x \in (y \cap ran F) (F^{-1} [\{x\}] \subseteq ℝ \land {vol}^{*} (F^{-1} [\{x\}]) \in ℝ)$
101		ovolfiniun	$⊢ (y \cap ran F \in Fin \land \forall x \in (y \cap ran F) (F^{-1} [\{x\}] \subseteq ℝ \land {vol}^{} (F^{-1} [\{x\}]) \in ℝ)) \to {vol}^{} (⋃_{x \in y \cap ran F} F^{-1} [\{x\}]) \leq \sum_{x \in y \cap ran F} {vol}^{*} (F^{-1} [\{x\}])$
102	40 100 101	syl2anc	$⊢ (φ \land \neg 0 \in y) \to {vol}^{} (⋃_{x \in y \cap ran F} F^{-1} [\{x\}]) \leq \sum_{x \in y \cap ran F} {vol}^{} (F^{-1} [\{x\}])$
103	96 102	eqbrtrrd	$⊢ (φ \land \neg 0 \in y) \to {vol}^{} (F^{-1} [y]) \leq \sum_{x \in y \cap ran F} {vol}^{} (F^{-1} [\{x\}])$
104		ovollecl	$⊢ (F^{-1} [y] \subseteq ℝ \land \sum_{x \in y \cap ran F} {vol}^{} (F^{-1} [\{x\}]) \in ℝ \land {vol}^{} (F^{-1} [y]) \leq \sum_{x \in y \cap ran F} {vol}^{} (F^{-1} [\{x\}])) \to {vol}^{} (F^{-1} [y]) \in ℝ$
105	90 95 103 104	syl3anc	$⊢ (φ \land \neg 0 \in y) \to {vol}^{*} (F^{-1} [y]) \in ℝ$
106	88 105	eqeltrd	$⊢ (φ \land \neg 0 \in y) \to vol (F^{-1} [y]) \in ℝ$
107	106	ex	$⊢ φ \to (\neg 0 \in y \to vol (F^{-1} [y]) \in ℝ)$
108	107	alrimiv	$⊢ φ \to \forall y (\neg 0 \in y \to vol (F^{-1} [y]) \in ℝ)$
109		neldifsn	$⊢ \neg 0 \in (ℝ ∖ \{0\})$
110	61	difexi	$⊢ ℝ ∖ \{0\} \in V$
111		eleq2	$⊢ y = ℝ ∖ \{0\} \to (0 \in y \leftrightarrow 0 \in (ℝ ∖ \{0\}))$
112	111	notbid	$⊢ y = ℝ ∖ \{0\} \to (\neg 0 \in y \leftrightarrow \neg 0 \in (ℝ ∖ \{0\}))$
113		imaeq2	$⊢ y = ℝ ∖ \{0\} \to F^{-1} [y] = F^{-1} [ℝ ∖ \{0\}]$
114	113	fveq2d	$⊢ y = ℝ ∖ \{0\} \to vol (F^{-1} [y]) = vol (F^{-1} [ℝ ∖ \{0\}])$
115	114	eleq1d	$⊢ y = ℝ ∖ \{0\} \to (vol (F^{-1} [y]) \in ℝ \leftrightarrow vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ)$
116	112 115	imbi12d	$⊢ y = ℝ ∖ \{0\} \to ((\neg 0 \in y \to vol (F^{-1} [y]) \in ℝ) \leftrightarrow (\neg 0 \in (ℝ ∖ \{0\}) \to vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ))$
117	110 116	spcv	$⊢ \forall y (\neg 0 \in y \to vol (F^{-1} [y]) \in ℝ) \to (\neg 0 \in (ℝ ∖ \{0\}) \to vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ)$
118	108 109 117	mpisyl	$⊢ φ \to vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ$
119	1 2 118	3jca	$⊢ φ \to (F : ℝ ⟶ ℝ \land ran F \in Fin \land vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ)$
120		isi1f	$⊢ F \in dom \int^{1} \leftrightarrow (F \in MblFn \land (F : ℝ ⟶ ℝ \land ran F \in Fin \land vol (F^{-1} [ℝ ∖ \{0\}]) \in ℝ))$
121	86 119 120	sylanbrc	$⊢ φ \to F \in dom \int^{1}$

Metamath Proof Explorer

Theorem i1fd

Proof