Theorem 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	⊢ Ⅎ 𝑥 𝜑
	smfrec.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfrec.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	smfrec.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	smfrec.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
	smfrec.e	⊢ 𝐶 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0 }
Assertion	smfrec	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 1 / 𝐵 ) ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

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