ftc1anclem1

Description: Lemma for ftc1anc - the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf , but this proof avoids ax-cc . (Contributed by Brendan Leahy, 18-Jun-2018)

		Ref	Expression
	Assertion	ftc1anclem1	$⊢ (F : A ⟶ ℝ \land F \in MblFn) \to abs \circ F \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		ffvelrn	$⊢ (F : A ⟶ ℝ \land t \in A) \to F (t) \in ℝ$
2	1	recnd	$⊢ (F : A ⟶ ℝ \land t \in A) \to F (t) \in ℂ$
3		id	$⊢ F : A ⟶ ℝ \to F : A ⟶ ℝ$
4	3	feqmptd	$⊢ F : A ⟶ ℝ \to F = (t \in A ⟼ F (t))$
5		absf	$⊢ abs : ℂ ⟶ ℝ$
6	5	a1i	$⊢ F : A ⟶ ℝ \to abs : ℂ ⟶ ℝ$
7	6	feqmptd	$⊢ F : A ⟶ ℝ \to abs = (x \in ℂ ⟼ \|x\|)$
8		fveq2	$⊢ x = F (t) \to \|x\| = \|F (t)\|$
9	2 4 7 8	fmptco	$⊢ F : A ⟶ ℝ \to abs \circ F = (t \in A ⟼ \|F (t)\|)$
10	9	adantr	$⊢ (F : A ⟶ ℝ \land F \in MblFn) \to abs \circ F = (t \in A ⟼ \|F (t)\|)$
11	2	abscld	$⊢ (F : A ⟶ ℝ \land t \in A) \to \|F (t)\| \in ℝ$
12	11	fmpttd	$⊢ F : A ⟶ ℝ \to (t \in A ⟼ \|F (t)\|) : A ⟶ ℝ$
13	12	adantr	$⊢ (F : A ⟶ ℝ \land F \in MblFn) \to (t \in A ⟼ \|F (t)\|) : A ⟶ ℝ$
14		fdm	$⊢ F : A ⟶ ℝ \to dom F = A$
15	14	adantr	$⊢ (F : A ⟶ ℝ \land F \in MblFn) \to dom F = A$
16		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
17	16	adantl	$⊢ (F : A ⟶ ℝ \land F \in MblFn) \to dom F \in dom vol$
18	15 17	eqeltrrd	$⊢ (F : A ⟶ ℝ \land F \in MblFn) \to A \in dom vol$
19		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
20		elioopnf	$⊢ x \in ℝ^{*} \to (\|F (t)\| \in (x, +∞) \leftrightarrow (\|F (t)\| \in ℝ \land x < \|F (t)\|))$
21	19 20	syl	$⊢ x \in ℝ \to (\|F (t)\| \in (x, +∞) \leftrightarrow (\|F (t)\| \in ℝ \land x < \|F (t)\|))$
22	11	biantrurd	$⊢ (F : A ⟶ ℝ \land t \in A) \to (x < \|F (t)\| \leftrightarrow (\|F (t)\| \in ℝ \land x < \|F (t)\|))$
23	22	bicomd	$⊢ (F : A ⟶ ℝ \land t \in A) \to ((\|F (t)\| \in ℝ \land x < \|F (t)\|) \leftrightarrow x < \|F (t)\|)$
24	21 23	sylan9bbr	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (\|F (t)\| \in (x, +∞) \leftrightarrow x < \|F (t)\|)$
25		ltnle	$⊢ (x \in ℝ \land \|F (t)\| \in ℝ) \to (x < \|F (t)\| \leftrightarrow \neg \|F (t)\| \leq x)$
26	25	ancoms	$⊢ (\|F (t)\| \in ℝ \land x \in ℝ) \to (x < \|F (t)\| \leftrightarrow \neg \|F (t)\| \leq x)$
27	11 26	sylan	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (x < \|F (t)\| \leftrightarrow \neg \|F (t)\| \leq x)$
28		absle	$⊢ (F (t) \in ℝ \land x \in ℝ) \to (\|F (t)\| \leq x \leftrightarrow (- x \leq F (t) \land F (t) \leq x))$
29	1 28	sylan	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (\|F (t)\| \leq x \leftrightarrow (- x \leq F (t) \land F (t) \leq x))$
30		renegcl	$⊢ x \in ℝ \to - x \in ℝ$
31		lenlt	$⊢ (- x \in ℝ \land F (t) \in ℝ) \to (- x \leq F (t) \leftrightarrow \neg F (t) < - x)$
32	30 1 31	syl2anr	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (- x \leq F (t) \leftrightarrow \neg F (t) < - x)$
33	1	biantrurd	$⊢ (F : A ⟶ ℝ \land t \in A) \to (F (t) < - x \leftrightarrow (F (t) \in ℝ \land F (t) < - x))$
34	30	rexrd	$⊢ x \in ℝ \to - x \in ℝ^{*}$
35		elioomnf	$⊢ - x \in ℝ^{*} \to (F (t) \in (−∞, - x) \leftrightarrow (F (t) \in ℝ \land F (t) < - x))$
36	34 35	syl	$⊢ x \in ℝ \to (F (t) \in (−∞, - x) \leftrightarrow (F (t) \in ℝ \land F (t) < - x))$
37	36	bicomd	$⊢ x \in ℝ \to ((F (t) \in ℝ \land F (t) < - x) \leftrightarrow F (t) \in (−∞, - x))$
38	33 37	sylan9bb	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (F (t) < - x \leftrightarrow F (t) \in (−∞, - x))$
39	38	notbid	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (\neg F (t) < - x \leftrightarrow \neg F (t) \in (−∞, - x))$
40	32 39	bitrd	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (- x \leq F (t) \leftrightarrow \neg F (t) \in (−∞, - x))$
41		lenlt	$⊢ (F (t) \in ℝ \land x \in ℝ) \to (F (t) \leq x \leftrightarrow \neg x < F (t))$
42	1 41	sylan	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (F (t) \leq x \leftrightarrow \neg x < F (t))$
43	1	biantrurd	$⊢ (F : A ⟶ ℝ \land t \in A) \to (x < F (t) \leftrightarrow (F (t) \in ℝ \land x < F (t)))$
44		elioopnf	$⊢ x \in ℝ^{*} \to (F (t) \in (x, +∞) \leftrightarrow (F (t) \in ℝ \land x < F (t)))$
45	19 44	syl	$⊢ x \in ℝ \to (F (t) \in (x, +∞) \leftrightarrow (F (t) \in ℝ \land x < F (t)))$
46	45	bicomd	$⊢ x \in ℝ \to ((F (t) \in ℝ \land x < F (t)) \leftrightarrow F (t) \in (x, +∞))$
47	43 46	sylan9bb	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (x < F (t) \leftrightarrow F (t) \in (x, +∞))$
48	47	notbid	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (\neg x < F (t) \leftrightarrow \neg F (t) \in (x, +∞))$
49	42 48	bitrd	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (F (t) \leq x \leftrightarrow \neg F (t) \in (x, +∞))$
50	40 49	anbi12d	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to ((- x \leq F (t) \land F (t) \leq x) \leftrightarrow (\neg F (t) \in (−∞, - x) \land \neg F (t) \in (x, +∞)))$
51	29 50	bitrd	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (\|F (t)\| \leq x \leftrightarrow (\neg F (t) \in (−∞, - x) \land \neg F (t) \in (x, +∞)))$
52	51	notbid	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (\neg \|F (t)\| \leq x \leftrightarrow \neg (\neg F (t) \in (−∞, - x) \land \neg F (t) \in (x, +∞)))$
53		elun	$⊢ F (t) \in ((−∞, - x) \cup (x, +∞)) \leftrightarrow (F (t) \in (−∞, - x) \lor F (t) \in (x, +∞))$
54		oran	$⊢ (F (t) \in (−∞, - x) \lor F (t) \in (x, +∞)) \leftrightarrow \neg (\neg F (t) \in (−∞, - x) \land \neg F (t) \in (x, +∞))$
55	53 54	bitri	$⊢ F (t) \in ((−∞, - x) \cup (x, +∞)) \leftrightarrow \neg (\neg F (t) \in (−∞, - x) \land \neg F (t) \in (x, +∞))$
56	52 55	bitr4di	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (\neg \|F (t)\| \leq x \leftrightarrow F (t) \in ((−∞, - x) \cup (x, +∞)))$
57	24 27 56	3bitrd	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (\|F (t)\| \in (x, +∞) \leftrightarrow F (t) \in ((−∞, - x) \cup (x, +∞)))$
58	57	an32s	$⊢ ((F : A ⟶ ℝ \land x \in ℝ) \land t \in A) \to (\|F (t)\| \in (x, +∞) \leftrightarrow F (t) \in ((−∞, - x) \cup (x, +∞)))$
59	58	rabbidva	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to \{t \in A \| \|F (t)\| \in (x, +∞)\} = \{t \in A \| F (t) \in ((−∞, - x) \cup (x, +∞))\}$
60		eqid	$⊢ (t \in A ⟼ \|F (t)\|) = (t \in A ⟼ \|F (t)\|)$
61	60	mptpreima	$⊢ {(t \in A ⟼ \|F (t)\|)}^{-1} [(x, +∞)] = \{t \in A \| \|F (t)\| \in (x, +∞)\}$
62		eqid	$⊢ (t \in A ⟼ F (t)) = (t \in A ⟼ F (t))$
63	62	mptpreima	$⊢ {(t \in A ⟼ F (t))}^{-1} [(−∞, - x) \cup (x, +∞)] = \{t \in A \| F (t) \in ((−∞, - x) \cup (x, +∞))\}$
64	59 61 63	3eqtr4g	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to {(t \in A ⟼ \|F (t)\|)}^{-1} [(x, +∞)] = {(t \in A ⟼ F (t))}^{-1} [(−∞, - x) \cup (x, +∞)]$
65		simpl	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to F : A ⟶ ℝ$
66	65	feqmptd	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to F = (t \in A ⟼ F (t))$
67	66	cnveqd	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to F^{-1} = {(t \in A ⟼ F (t))}^{-1}$
68	67	imaeq1d	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to F^{-1} [(−∞, - x) \cup (x, +∞)] = {(t \in A ⟼ F (t))}^{-1} [(−∞, - x) \cup (x, +∞)]$
69	64 68	eqtr4d	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to {(t \in A ⟼ \|F (t)\|)}^{-1} [(x, +∞)] = F^{-1} [(−∞, - x) \cup (x, +∞)]$
70		imaundi	$⊢ F^{-1} [(−∞, - x) \cup (x, +∞)] = F^{-1} [(−∞, - x)] \cup F^{-1} [(x, +∞)]$
71	69 70	eqtrdi	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to {(t \in A ⟼ \|F (t)\|)}^{-1} [(x, +∞)] = F^{-1} [(−∞, - x)] \cup F^{-1} [(x, +∞)]$
72	71	adantlr	$⊢ ((F : A ⟶ ℝ \land F \in MblFn) \land x \in ℝ) \to {(t \in A ⟼ \|F (t)\|)}^{-1} [(x, +∞)] = F^{-1} [(−∞, - x)] \cup F^{-1} [(x, +∞)]$
73		mbfima	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to F^{-1} [(−∞, - x)] \in dom vol$
74		mbfima	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to F^{-1} [(x, +∞)] \in dom vol$
75		unmbl	$⊢ (F^{-1} [(−∞, - x)] \in dom vol \land F^{-1} [(x, +∞)] \in dom vol) \to F^{-1} [(−∞, - x)] \cup F^{-1} [(x, +∞)] \in dom vol$
76	73 74 75	syl2anc	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to F^{-1} [(−∞, - x)] \cup F^{-1} [(x, +∞)] \in dom vol$
77	76	ancoms	$⊢ (F : A ⟶ ℝ \land F \in MblFn) \to F^{-1} [(−∞, - x)] \cup F^{-1} [(x, +∞)] \in dom vol$
78	77	adantr	$⊢ ((F : A ⟶ ℝ \land F \in MblFn) \land x \in ℝ) \to F^{-1} [(−∞, - x)] \cup F^{-1} [(x, +∞)] \in dom vol$
79	72 78	eqeltrd	$⊢ ((F : A ⟶ ℝ \land F \in MblFn) \land x \in ℝ) \to {(t \in A ⟼ \|F (t)\|)}^{-1} [(x, +∞)] \in dom vol$
80		abslt	$⊢ (F (t) \in ℝ \land x \in ℝ) \to (\|F (t)\| < x \leftrightarrow (- x < F (t) \land F (t) < x))$
81	1 80	sylan	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (\|F (t)\| < x \leftrightarrow (- x < F (t) \land F (t) < x))$
82		elioomnf	$⊢ x \in ℝ^{*} \to (\|F (t)\| \in (−∞, x) \leftrightarrow (\|F (t)\| \in ℝ \land \|F (t)\| < x))$
83	19 82	syl	$⊢ x \in ℝ \to (\|F (t)\| \in (−∞, x) \leftrightarrow (\|F (t)\| \in ℝ \land \|F (t)\| < x))$
84	11	biantrurd	$⊢ (F : A ⟶ ℝ \land t \in A) \to (\|F (t)\| < x \leftrightarrow (\|F (t)\| \in ℝ \land \|F (t)\| < x))$
85	84	bicomd	$⊢ (F : A ⟶ ℝ \land t \in A) \to ((\|F (t)\| \in ℝ \land \|F (t)\| < x) \leftrightarrow \|F (t)\| < x)$
86	83 85	sylan9bbr	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (\|F (t)\| \in (−∞, x) \leftrightarrow \|F (t)\| < x)$
87	34 19	jca	$⊢ x \in ℝ \to (- x \in ℝ^{} \land x \in ℝ^{})$
88	1	rexrd	$⊢ (F : A ⟶ ℝ \land t \in A) \to F (t) \in ℝ^{*}$
89		elioo5	$⊢ (- x \in ℝ^{} \land x \in ℝ^{} \land F (t) \in ℝ^{*}) \to (F (t) \in (- x, x) \leftrightarrow (- x < F (t) \land F (t) < x))$
90	89	3expa	$⊢ ((- x \in ℝ^{} \land x \in ℝ^{}) \land F (t) \in ℝ^{*}) \to (F (t) \in (- x, x) \leftrightarrow (- x < F (t) \land F (t) < x))$
91	87 88 90	syl2anr	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (F (t) \in (- x, x) \leftrightarrow (- x < F (t) \land F (t) < x))$
92	81 86 91	3bitr4d	$⊢ ((F : A ⟶ ℝ \land t \in A) \land x \in ℝ) \to (\|F (t)\| \in (−∞, x) \leftrightarrow F (t) \in (- x, x))$
93	92	an32s	$⊢ ((F : A ⟶ ℝ \land x \in ℝ) \land t \in A) \to (\|F (t)\| \in (−∞, x) \leftrightarrow F (t) \in (- x, x))$
94	93	rabbidva	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to \{t \in A \| \|F (t)\| \in (−∞, x)\} = \{t \in A \| F (t) \in (- x, x)\}$
95	60	mptpreima	$⊢ {(t \in A ⟼ \|F (t)\|)}^{-1} [(−∞, x)] = \{t \in A \| \|F (t)\| \in (−∞, x)\}$
96	62	mptpreima	$⊢ {(t \in A ⟼ F (t))}^{-1} [(- x, x)] = \{t \in A \| F (t) \in (- x, x)\}$
97	94 95 96	3eqtr4g	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to {(t \in A ⟼ \|F (t)\|)}^{-1} [(−∞, x)] = {(t \in A ⟼ F (t))}^{-1} [(- x, x)]$
98	67	imaeq1d	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to F^{-1} [(- x, x)] = {(t \in A ⟼ F (t))}^{-1} [(- x, x)]$
99	97 98	eqtr4d	$⊢ (F : A ⟶ ℝ \land x \in ℝ) \to {(t \in A ⟼ \|F (t)\|)}^{-1} [(−∞, x)] = F^{-1} [(- x, x)]$
100	99	adantlr	$⊢ ((F : A ⟶ ℝ \land F \in MblFn) \land x \in ℝ) \to {(t \in A ⟼ \|F (t)\|)}^{-1} [(−∞, x)] = F^{-1} [(- x, x)]$
101		mbfima	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to F^{-1} [(- x, x)] \in dom vol$
102	101	ancoms	$⊢ (F : A ⟶ ℝ \land F \in MblFn) \to F^{-1} [(- x, x)] \in dom vol$
103	102	adantr	$⊢ ((F : A ⟶ ℝ \land F \in MblFn) \land x \in ℝ) \to F^{-1} [(- x, x)] \in dom vol$
104	100 103	eqeltrd	$⊢ ((F : A ⟶ ℝ \land F \in MblFn) \land x \in ℝ) \to {(t \in A ⟼ \|F (t)\|)}^{-1} [(−∞, x)] \in dom vol$
105	13 18 79 104	ismbf2d	$⊢ (F : A ⟶ ℝ \land F \in MblFn) \to (t \in A ⟼ \|F (t)\|) \in MblFn$
106	10 105	eqeltrd	$⊢ (F : A ⟶ ℝ \land F \in MblFn) \to abs \circ F \in MblFn$

Metamath Proof Explorer

Theorem ftc1anclem1

Proof