smfrec

Description: The reciprocal of a sigma-measurable functions is sigma-measurable. First part of Proposition 121E (e) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfrec.x	$⊢ Ⅎ x φ$
	smfrec.s	$⊢ φ \to S \in SAlg$
	smfrec.a	$⊢ φ \to A \in V$
	smfrec.b	$⊢ (φ \land x \in A) \to B \in ℝ$
	smfrec.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
	smfrec.e	$⊢ C = \{x \in A \| B \neq 0\}$
Assertion	smfrec	$⊢ φ \to (x \in C ⟼ \frac{1}{B}) \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfrec.x	$⊢ Ⅎ x φ$
2		smfrec.s	$⊢ φ \to S \in SAlg$
3		smfrec.a	$⊢ φ \to A \in V$
4		smfrec.b	$⊢ (φ \land x \in A) \to B \in ℝ$
5		smfrec.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
6		smfrec.e	$⊢ C = \{x \in A \| B \neq 0\}$
7		nfv	$⊢ Ⅎ a φ$
8		ssrab2	$⊢ \{x \in A \| B \neq 0\} \subseteq A$
9	6 8	eqsstri	$⊢ C \subseteq A$
10		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
11	1 10 4	dmmptdf	$⊢ φ \to dom (x \in A ⟼ B) = A$
12	11	eqcomd	$⊢ φ \to A = dom (x \in A ⟼ B)$
13		eqid	$⊢ dom (x \in A ⟼ B) = dom (x \in A ⟼ B)$
14	2 5 13	smfdmss	$⊢ φ \to dom (x \in A ⟼ B) \subseteq ⋃ S$
15	12 14	eqsstrd	$⊢ φ \to A \subseteq ⋃ S$
16	9 15	sstrid	$⊢ φ \to C \subseteq ⋃ S$
17		1red	$⊢ (φ \land x \in C) \to 1 \in ℝ$
18	9	sseli	$⊢ x \in C \to x \in A$
19	18	adantl	$⊢ (φ \land x \in C) \to x \in A$
20	19 4	syldan	$⊢ (φ \land x \in C) \to B \in ℝ$
21	6	eleq2i	$⊢ x \in C \leftrightarrow x \in \{x \in A \| B \neq 0\}$
22	21	biimpi	$⊢ x \in C \to x \in \{x \in A \| B \neq 0\}$
23		rabidim2	$⊢ x \in \{x \in A \| B \neq 0\} \to B \neq 0$
24	22 23	syl	$⊢ x \in C \to B \neq 0$
25	24	adantl	$⊢ (φ \land x \in C) \to B \neq 0$
26	17 20 25	redivcld	$⊢ (φ \land x \in C) \to \frac{1}{B} \in ℝ$
27		nfv	$⊢ Ⅎ x a \in ℝ$
28	1 27	nfan	$⊢ Ⅎ x (φ \land a \in ℝ)$
29		nfv	$⊢ Ⅎ x 0 < a$
30	28 29	nfan	$⊢ Ⅎ x ((φ \land a \in ℝ) \land 0 < a)$
31	20	ad4ant14	$⊢ (((φ \land a \in ℝ) \land 0 < a) \land x \in C) \to B \in ℝ$
32	24	adantl	$⊢ (((φ \land a \in ℝ) \land 0 < a) \land x \in C) \to B \neq 0$
33		simpl	$⊢ (a \in ℝ \land 0 < a) \to a \in ℝ$
34		simpr	$⊢ (a \in ℝ \land 0 < a) \to 0 < a$
35	33 34	elrpd	$⊢ (a \in ℝ \land 0 < a) \to a \in ℝ^{+}$
36	35	adantll	$⊢ ((φ \land a \in ℝ) \land 0 < a) \to a \in ℝ^{+}$
37	30 31 32 36	pimrecltpos	$⊢ ((φ \land a \in ℝ) \land 0 < a) \to \{x \in C \| \frac{1}{B} < a\} = \{x \in C \| \frac{1}{a} < B\} \cup \{x \in C \| B < 0\}$
38	6 3	rabexd	$⊢ φ \to C \in V$
39		eqid	$⊢ S ↾_{𝑡} C = S ↾_{𝑡} C$
40	2 38 39	subsalsal	$⊢ φ \to S ↾_{𝑡} C \in SAlg$
41	40	ad2antrr	$⊢ ((φ \land a \in ℝ) \land 0 < a) \to S ↾_{𝑡} C \in SAlg$
42	2	adantr	$⊢ (φ \land a \in ℝ) \to S \in SAlg$
43	42	adantr	$⊢ ((φ \land a \in ℝ) \land 0 < a) \to S \in SAlg$
44	9	a1i	$⊢ φ \to C \subseteq A$
45	2 5 44	sssmfmpt	$⊢ φ \to (x \in C ⟼ B) \in SMblFn (S)$
46	45	adantr	$⊢ (φ \land a \in ℝ) \to (x \in C ⟼ B) \in SMblFn (S)$
47	46	adantr	$⊢ ((φ \land a \in ℝ) \land 0 < a) \to (x \in C ⟼ B) \in SMblFn (S)$
48	35	rprecred	$⊢ (a \in ℝ \land 0 < a) \to \frac{1}{a} \in ℝ$
49	48	adantll	$⊢ ((φ \land a \in ℝ) \land 0 < a) \to \frac{1}{a} \in ℝ$
50	30 43 31 47 49	smfpimgtmpt	$⊢ ((φ \land a \in ℝ) \land 0 < a) \to \{x \in C \| \frac{1}{a} < B\} \in (S ↾_{𝑡} C)$
51		0red	$⊢ φ \to 0 \in ℝ$
52	1 2 20 45 51	smfpimltmpt	$⊢ φ \to \{x \in C \| B < 0\} \in (S ↾_{𝑡} C)$
53	52	ad2antrr	$⊢ ((φ \land a \in ℝ) \land 0 < a) \to \{x \in C \| B < 0\} \in (S ↾_{𝑡} C)$
54	41 50 53	saluncld	$⊢ ((φ \land a \in ℝ) \land 0 < a) \to \{x \in C \| \frac{1}{a} < B\} \cup \{x \in C \| B < 0\} \in (S ↾_{𝑡} C)$
55	37 54	eqeltrd	$⊢ ((φ \land a \in ℝ) \land 0 < a) \to \{x \in C \| \frac{1}{B} < a\} \in (S ↾_{𝑡} C)$
56		nfv	$⊢ Ⅎ x a = 0$
57	1 56	nfan	$⊢ Ⅎ x (φ \land a = 0)$
58		breq2	$⊢ a = 0 \to (\frac{1}{B} < a \leftrightarrow \frac{1}{B} < 0)$
59	58	ad2antlr	$⊢ ((φ \land a = 0) \land x \in C) \to (\frac{1}{B} < a \leftrightarrow \frac{1}{B} < 0)$
60	20 25	reclt0	$⊢ (φ \land x \in C) \to (B < 0 \leftrightarrow \frac{1}{B} < 0)$
61	60	bicomd	$⊢ (φ \land x \in C) \to (\frac{1}{B} < 0 \leftrightarrow B < 0)$
62	61	adantlr	$⊢ ((φ \land a = 0) \land x \in C) \to (\frac{1}{B} < 0 \leftrightarrow B < 0)$
63	59 62	bitrd	$⊢ ((φ \land a = 0) \land x \in C) \to (\frac{1}{B} < a \leftrightarrow B < 0)$
64	57 63	rabbida	$⊢ (φ \land a = 0) \to \{x \in C \| \frac{1}{B} < a\} = \{x \in C \| B < 0\}$
65	52	adantr	$⊢ (φ \land a = 0) \to \{x \in C \| B < 0\} \in (S ↾_{𝑡} C)$
66	64 65	eqeltrd	$⊢ (φ \land a = 0) \to \{x \in C \| \frac{1}{B} < a\} \in (S ↾_{𝑡} C)$
67	66	ad4ant14	$⊢ (((φ \land a \in ℝ) \land \neg 0 < a) \land a = 0) \to \{x \in C \| \frac{1}{B} < a\} \in (S ↾_{𝑡} C)$
68		simpll	$⊢ (((φ \land a \in ℝ) \land \neg 0 < a) \land \neg a = 0) \to (φ \land a \in ℝ)$
69		simpll	$⊢ ((a \in ℝ \land \neg 0 < a) \land \neg a = 0) \to a \in ℝ$
70		0red	$⊢ ((a \in ℝ \land \neg 0 < a) \land \neg a = 0) \to 0 \in ℝ$
71		neqne	$⊢ \neg a = 0 \to a \neq 0$
72	71	adantl	$⊢ ((a \in ℝ \land \neg 0 < a) \land \neg a = 0) \to a \neq 0$
73		simplr	$⊢ ((a \in ℝ \land \neg 0 < a) \land \neg a = 0) \to \neg 0 < a$
74	69 70 72 73	lttri5d	$⊢ ((a \in ℝ \land \neg 0 < a) \land \neg a = 0) \to a < 0$
75	74	adantlll	$⊢ (((φ \land a \in ℝ) \land \neg 0 < a) \land \neg a = 0) \to a < 0$
76		nfv	$⊢ Ⅎ x a < 0$
77	28 76	nfan	$⊢ Ⅎ x ((φ \land a \in ℝ) \land a < 0)$
78	4	adantlr	$⊢ ((φ \land a \in ℝ) \land x \in A) \to B \in ℝ$
79	18 78	sylan2	$⊢ ((φ \land a \in ℝ) \land x \in C) \to B \in ℝ$
80	79	adantlr	$⊢ (((φ \land a \in ℝ) \land a < 0) \land x \in C) \to B \in ℝ$
81	24	adantl	$⊢ (((φ \land a \in ℝ) \land a < 0) \land x \in C) \to B \neq 0$
82		simpr	$⊢ (φ \land a \in ℝ) \to a \in ℝ$
83	82	adantr	$⊢ ((φ \land a \in ℝ) \land a < 0) \to a \in ℝ$
84		simpr	$⊢ ((φ \land a \in ℝ) \land a < 0) \to a < 0$
85	77 80 81 83 84	pimrecltneg	$⊢ ((φ \land a \in ℝ) \land a < 0) \to \{x \in C \| \frac{1}{B} < a\} = \{x \in C \| B \in (\frac{1}{a}, 0)\}$
86	42	adantr	$⊢ ((φ \land a \in ℝ) \land a < 0) \to S \in SAlg$
87	38	ad2antrr	$⊢ ((φ \land a \in ℝ) \land a < 0) \to C \in V$
88	46	adantr	$⊢ ((φ \land a \in ℝ) \land a < 0) \to (x \in C ⟼ B) \in SMblFn (S)$
89		1red	$⊢ (a \in ℝ \land a < 0) \to 1 \in ℝ$
90		simpl	$⊢ (a \in ℝ \land a < 0) \to a \in ℝ$
91		lt0ne0	$⊢ (a \in ℝ \land a < 0) \to a \neq 0$
92	89 90 91	redivcld	$⊢ (a \in ℝ \land a < 0) \to \frac{1}{a} \in ℝ$
93	92	adantll	$⊢ ((φ \land a \in ℝ) \land a < 0) \to \frac{1}{a} \in ℝ$
94	93	rexrd	$⊢ ((φ \land a \in ℝ) \land a < 0) \to \frac{1}{a} \in ℝ^{*}$
95	51	ad2antrr	$⊢ ((φ \land a \in ℝ) \land a < 0) \to 0 \in ℝ$
96	95	rexrd	$⊢ ((φ \land a \in ℝ) \land a < 0) \to 0 \in ℝ^{*}$
97	77 86 87 80 88 94 96	smfpimioompt	$⊢ ((φ \land a \in ℝ) \land a < 0) \to \{x \in C \| B \in (\frac{1}{a}, 0)\} \in (S ↾_{𝑡} C)$
98	85 97	eqeltrd	$⊢ ((φ \land a \in ℝ) \land a < 0) \to \{x \in C \| \frac{1}{B} < a\} \in (S ↾_{𝑡} C)$
99	68 75 98	syl2anc	$⊢ (((φ \land a \in ℝ) \land \neg 0 < a) \land \neg a = 0) \to \{x \in C \| \frac{1}{B} < a\} \in (S ↾_{𝑡} C)$
100	67 99	pm2.61dan	$⊢ ((φ \land a \in ℝ) \land \neg 0 < a) \to \{x \in C \| \frac{1}{B} < a\} \in (S ↾_{𝑡} C)$
101	55 100	pm2.61dan	$⊢ (φ \land a \in ℝ) \to \{x \in C \| \frac{1}{B} < a\} \in (S ↾_{𝑡} C)$
102	1 7 2 16 26 101	issmfdmpt	$⊢ φ \to (x \in C ⟼ \frac{1}{B}) \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfrec

Proof