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 
|- F/ x ph
smfrec.s 
|- ( ph -> S e. SAlg )
smfrec.a 
|- ( ph -> A e. V )
smfrec.b 
|- ( ( ph /\ x e. A ) -> B e. RR )
smfrec.m 
|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
smfrec.e 
|- C = { x e. A | B =/= 0 }
Assertion smfrec 
|- ( ph -> ( x e. C |-> ( 1 / B ) ) e. ( SMblFn ` S ) )

Proof

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