Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smfrec Structured version   Visualization version   GIF version

Theorem smfrec 44578
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.)
Hypotheses
Ref Expression
smfrec.x 𝑥𝜑
smfrec.s (𝜑𝑆 ∈ SAlg)
smfrec.a (𝜑𝐴𝑉)
smfrec.b ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)
smfrec.m (𝜑 → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))
smfrec.e 𝐶 = {𝑥𝐴𝐵 ≠ 0}
Assertion
Ref Expression
smfrec (𝜑 → (𝑥𝐶 ↦ (1 / 𝐵)) ∈ (SMblFn‘𝑆))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑆(𝑥)   𝑉(𝑥)

Proof of Theorem smfrec
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 smfrec.x . 2 𝑥𝜑
2 nfv 1916 . 2 𝑎𝜑
3 smfrec.s . 2 (𝜑𝑆 ∈ SAlg)
4 smfrec.e . . . 4 𝐶 = {𝑥𝐴𝐵 ≠ 0}
5 ssrab2 4024 . . . 4 {𝑥𝐴𝐵 ≠ 0} ⊆ 𝐴
64, 5eqsstri 3965 . . 3 𝐶𝐴
7 eqid 2737 . . . . . 6 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
8 smfrec.b . . . . . 6 ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)
91, 7, 8dmmptdf 43005 . . . . 5 (𝜑 → dom (𝑥𝐴𝐵) = 𝐴)
109eqcomd 2743 . . . 4 (𝜑𝐴 = dom (𝑥𝐴𝐵))
11 smfrec.m . . . . 5 (𝜑 → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))
12 eqid 2737 . . . . 5 dom (𝑥𝐴𝐵) = dom (𝑥𝐴𝐵)
133, 11, 12smfdmss 44522 . . . 4 (𝜑 → dom (𝑥𝐴𝐵) ⊆ 𝑆)
1410, 13eqsstrd 3969 . . 3 (𝜑𝐴 𝑆)
156, 14sstrid 3942 . 2 (𝜑𝐶 𝑆)
16 1red 11056 . . 3 ((𝜑𝑥𝐶) → 1 ∈ ℝ)
176sseli 3927 . . . . 5 (𝑥𝐶𝑥𝐴)
1817adantl 482 . . . 4 ((𝜑𝑥𝐶) → 𝑥𝐴)
1918, 8syldan 591 . . 3 ((𝜑𝑥𝐶) → 𝐵 ∈ ℝ)
204eleq2i 2829 . . . . . 6 (𝑥𝐶𝑥 ∈ {𝑥𝐴𝐵 ≠ 0})
2120biimpi 215 . . . . 5 (𝑥𝐶𝑥 ∈ {𝑥𝐴𝐵 ≠ 0})
22 rabidim2 42886 . . . . 5 (𝑥 ∈ {𝑥𝐴𝐵 ≠ 0} → 𝐵 ≠ 0)
2321, 22syl 17 . . . 4 (𝑥𝐶𝐵 ≠ 0)
2423adantl 482 . . 3 ((𝜑𝑥𝐶) → 𝐵 ≠ 0)
2516, 19, 24redivcld 11883 . 2 ((𝜑𝑥𝐶) → (1 / 𝐵) ∈ ℝ)
26 nfv 1916 . . . . . . 7 𝑥 𝑎 ∈ ℝ
271, 26nfan 1901 . . . . . 6 𝑥(𝜑𝑎 ∈ ℝ)
28 nfv 1916 . . . . . 6 𝑥0 < 𝑎
2927, 28nfan 1901 . . . . 5 𝑥((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎)
3019ad4ant14 749 . . . . 5 ((((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) ∧ 𝑥𝐶) → 𝐵 ∈ ℝ)
3123adantl 482 . . . . 5 ((((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) ∧ 𝑥𝐶) → 𝐵 ≠ 0)
32 simpl 483 . . . . . . 7 ((𝑎 ∈ ℝ ∧ 0 < 𝑎) → 𝑎 ∈ ℝ)
33 simpr 485 . . . . . . 7 ((𝑎 ∈ ℝ ∧ 0 < 𝑎) → 0 < 𝑎)
3432, 33elrpd 12849 . . . . . 6 ((𝑎 ∈ ℝ ∧ 0 < 𝑎) → 𝑎 ∈ ℝ+)
3534adantll 711 . . . . 5 (((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) → 𝑎 ∈ ℝ+)
3629, 30, 31, 35pimrecltpos 44497 . . . 4 (((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥𝐶 ∣ (1 / 𝐵) < 𝑎} = ({𝑥𝐶 ∣ (1 / 𝑎) < 𝐵} ∪ {𝑥𝐶𝐵 < 0}))
37 smfrec.a . . . . . . . 8 (𝜑𝐴𝑉)
384, 37rabexd 5272 . . . . . . 7 (𝜑𝐶 ∈ V)
39 eqid 2737 . . . . . . 7 (𝑆t 𝐶) = (𝑆t 𝐶)
403, 38, 39subsalsal 44148 . . . . . 6 (𝜑 → (𝑆t 𝐶) ∈ SAlg)
4140ad2antrr 723 . . . . 5 (((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) → (𝑆t 𝐶) ∈ SAlg)
423adantr 481 . . . . . . 7 ((𝜑𝑎 ∈ ℝ) → 𝑆 ∈ SAlg)
4342adantr 481 . . . . . 6 (((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) → 𝑆 ∈ SAlg)
446a1i 11 . . . . . . . . 9 (𝜑𝐶𝐴)
453, 11, 44sssmfmpt 44539 . . . . . . . 8 (𝜑 → (𝑥𝐶𝐵) ∈ (SMblFn‘𝑆))
4645adantr 481 . . . . . . 7 ((𝜑𝑎 ∈ ℝ) → (𝑥𝐶𝐵) ∈ (SMblFn‘𝑆))
4746adantr 481 . . . . . 6 (((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) → (𝑥𝐶𝐵) ∈ (SMblFn‘𝑆))
4834rprecred 12863 . . . . . . 7 ((𝑎 ∈ ℝ ∧ 0 < 𝑎) → (1 / 𝑎) ∈ ℝ)
4948adantll 711 . . . . . 6 (((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) → (1 / 𝑎) ∈ ℝ)
5029, 43, 30, 47, 49smfpimgtmpt 44570 . . . . 5 (((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥𝐶 ∣ (1 / 𝑎) < 𝐵} ∈ (𝑆t 𝐶))
51 0red 11058 . . . . . . 7 (𝜑 → 0 ∈ ℝ)
521, 3, 19, 45, 51smfpimltmpt 44535 . . . . . 6 (𝜑 → {𝑥𝐶𝐵 < 0} ∈ (𝑆t 𝐶))
5352ad2antrr 723 . . . . 5 (((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥𝐶𝐵 < 0} ∈ (𝑆t 𝐶))
5441, 50, 53saluncld 44137 . . . 4 (((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) → ({𝑥𝐶 ∣ (1 / 𝑎) < 𝐵} ∪ {𝑥𝐶𝐵 < 0}) ∈ (𝑆t 𝐶))
5536, 54eqeltrd 2838 . . 3 (((𝜑𝑎 ∈ ℝ) ∧ 0 < 𝑎) → {𝑥𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆t 𝐶))
56 nfv 1916 . . . . . . . 8 𝑥 𝑎 = 0
571, 56nfan 1901 . . . . . . 7 𝑥(𝜑𝑎 = 0)
58 breq2 5091 . . . . . . . . 9 (𝑎 = 0 → ((1 / 𝐵) < 𝑎 ↔ (1 / 𝐵) < 0))
5958ad2antlr 724 . . . . . . . 8 (((𝜑𝑎 = 0) ∧ 𝑥𝐶) → ((1 / 𝐵) < 𝑎 ↔ (1 / 𝐵) < 0))
6019, 24reclt0 43180 . . . . . . . . . 10 ((𝜑𝑥𝐶) → (𝐵 < 0 ↔ (1 / 𝐵) < 0))
6160bicomd 222 . . . . . . . . 9 ((𝜑𝑥𝐶) → ((1 / 𝐵) < 0 ↔ 𝐵 < 0))
6261adantlr 712 . . . . . . . 8 (((𝜑𝑎 = 0) ∧ 𝑥𝐶) → ((1 / 𝐵) < 0 ↔ 𝐵 < 0))
6359, 62bitrd 278 . . . . . . 7 (((𝜑𝑎 = 0) ∧ 𝑥𝐶) → ((1 / 𝐵) < 𝑎𝐵 < 0))
6457, 63rabbida 3429 . . . . . 6 ((𝜑𝑎 = 0) → {𝑥𝐶 ∣ (1 / 𝐵) < 𝑎} = {𝑥𝐶𝐵 < 0})
6552adantr 481 . . . . . 6 ((𝜑𝑎 = 0) → {𝑥𝐶𝐵 < 0} ∈ (𝑆t 𝐶))
6664, 65eqeltrd 2838 . . . . 5 ((𝜑𝑎 = 0) → {𝑥𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆t 𝐶))
6766ad4ant14 749 . . . 4 ((((𝜑𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ 𝑎 = 0) → {𝑥𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆t 𝐶))
68 simpll 764 . . . . 5 ((((𝜑𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → (𝜑𝑎 ∈ ℝ))
69 simpll 764 . . . . . . 7 (((𝑎 ∈ ℝ ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 ∈ ℝ)
70 0red 11058 . . . . . . 7 (((𝑎 ∈ ℝ ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → 0 ∈ ℝ)
71 neqne 2949 . . . . . . . 8 𝑎 = 0 → 𝑎 ≠ 0)
7271adantl 482 . . . . . . 7 (((𝑎 ∈ ℝ ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 ≠ 0)
73 simplr 766 . . . . . . 7 (((𝑎 ∈ ℝ ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → ¬ 0 < 𝑎)
7469, 70, 72, 73lttri5d 43087 . . . . . 6 (((𝑎 ∈ ℝ ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 < 0)
7574adantlll 715 . . . . 5 ((((𝜑𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → 𝑎 < 0)
76 nfv 1916 . . . . . . . 8 𝑥 𝑎 < 0
7727, 76nfan 1901 . . . . . . 7 𝑥((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0)
788adantlr 712 . . . . . . . . 9 (((𝜑𝑎 ∈ ℝ) ∧ 𝑥𝐴) → 𝐵 ∈ ℝ)
7917, 78sylan2 593 . . . . . . . 8 (((𝜑𝑎 ∈ ℝ) ∧ 𝑥𝐶) → 𝐵 ∈ ℝ)
8079adantlr 712 . . . . . . 7 ((((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) ∧ 𝑥𝐶) → 𝐵 ∈ ℝ)
8123adantl 482 . . . . . . 7 ((((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) ∧ 𝑥𝐶) → 𝐵 ≠ 0)
82 simpr 485 . . . . . . . 8 ((𝜑𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
8382adantr 481 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝑎 ∈ ℝ)
84 simpr 485 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝑎 < 0)
8577, 80, 81, 83, 84pimrecltneg 44513 . . . . . 6 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → {𝑥𝐶 ∣ (1 / 𝐵) < 𝑎} = {𝑥𝐶𝐵 ∈ ((1 / 𝑎)(,)0)})
8642adantr 481 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝑆 ∈ SAlg)
8738ad2antrr 723 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 𝐶 ∈ V)
8846adantr 481 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → (𝑥𝐶𝐵) ∈ (SMblFn‘𝑆))
89 1red 11056 . . . . . . . . . 10 ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → 1 ∈ ℝ)
90 simpl 483 . . . . . . . . . 10 ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → 𝑎 ∈ ℝ)
91 lt0ne0 11521 . . . . . . . . . 10 ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → 𝑎 ≠ 0)
9289, 90, 91redivcld 11883 . . . . . . . . 9 ((𝑎 ∈ ℝ ∧ 𝑎 < 0) → (1 / 𝑎) ∈ ℝ)
9392adantll 711 . . . . . . . 8 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → (1 / 𝑎) ∈ ℝ)
9493rexrd 11105 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → (1 / 𝑎) ∈ ℝ*)
9551ad2antrr 723 . . . . . . . 8 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 0 ∈ ℝ)
9695rexrd 11105 . . . . . . 7 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → 0 ∈ ℝ*)
9777, 86, 87, 80, 88, 94, 96smfpimioompt 44575 . . . . . 6 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → {𝑥𝐶𝐵 ∈ ((1 / 𝑎)(,)0)} ∈ (𝑆t 𝐶))
9885, 97eqeltrd 2838 . . . . 5 (((𝜑𝑎 ∈ ℝ) ∧ 𝑎 < 0) → {𝑥𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆t 𝐶))
9968, 75, 98syl2anc 584 . . . 4 ((((𝜑𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) ∧ ¬ 𝑎 = 0) → {𝑥𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆t 𝐶))
10067, 99pm2.61dan 810 . . 3 (((𝜑𝑎 ∈ ℝ) ∧ ¬ 0 < 𝑎) → {𝑥𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆t 𝐶))
10155, 100pm2.61dan 810 . 2 ((𝜑𝑎 ∈ ℝ) → {𝑥𝐶 ∣ (1 / 𝐵) < 𝑎} ∈ (𝑆t 𝐶))
1021, 2, 3, 15, 25, 101issmfdmpt 44537 1 (𝜑 → (𝑥𝐶 ↦ (1 / 𝐵)) ∈ (SMblFn‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1540  wnf 1784  wcel 2105  wne 2941  {crab 3404  Vcvv 3441  cun 3895  wss 3897   cuni 4850   class class class wbr 5087  cmpt 5170  dom cdm 5608  cfv 6466  (class class class)co 7317  cr 10950  0cc0 10951  1c1 10952   < clt 11089   / cdiv 11712  +crp 12810  (,)cioo 13159  t crest 17208  SAlgcsalg 44099  SMblFncsmblfn 44484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-inf2 9477  ax-cc 10271  ax-ac2 10299  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028  ax-pre-sup 11029
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-se 5564  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-isom 6475  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-om 7760  df-1st 7878  df-2nd 7879  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-er 8548  df-map 8667  df-pm 8668  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-sup 9278  df-inf 9279  df-card 9775  df-acn 9778  df-ac 9952  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-div 11713  df-nn 12054  df-n0 12314  df-z 12400  df-uz 12663  df-q 12769  df-rp 12811  df-ioo 13163  df-ico 13165  df-fl 13592  df-rest 17210  df-salg 44100  df-smblfn 44485
This theorem is referenced by:  smfdiv  44586
  Copyright terms: Public domain W3C validator