Metamath Proof Explorer


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 x φ
smfrec.s φ S SAlg
smfrec.a φ A V
smfrec.b φ x A B
smfrec.m φ x A B SMblFn S
smfrec.e C = x A | B 0
Assertion smfrec φ x C 1 B SMblFn S

Proof

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