Metamath Proof Explorer

Theorem smfdiv

Description: The fraction of two sigma-measurable functions is measurable. Proposition 121E (e) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfdiv.x 
|- F/ x ph
smfdiv.s 
|- ( ph -> S e. SAlg )
smfdiv.a 
|- ( ph -> A e. V )
smfdiv.b 
|- ( ( ph /\ x e. A ) -> B e. RR )
smfdiv.c 
|- ( ph -> C e. W )
smfdiv.d 
|- ( ( ph /\ x e. C ) -> D e. RR )
smfdiv.m 
|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
smfdiv.n 
|- ( ph -> ( x e. C |-> D ) e. ( SMblFn ` S ) )
smfdiv.e 
|- E = { x e. C | D =/= 0 }
Assertion smfdiv 
|- ( ph -> ( x e. ( A i^i E ) |-> ( B / D ) ) e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfdiv.x 
 |-  F/ x ph
2 smfdiv.s 
 |-  ( ph -> S e. SAlg )
3 smfdiv.a 
 |-  ( ph -> A e. V )
4 smfdiv.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
5 smfdiv.c 
 |-  ( ph -> C e. W )
6 smfdiv.d 
 |-  ( ( ph /\ x e. C ) -> D e. RR )
7 smfdiv.m 
 |-  ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
8 smfdiv.n 
 |-  ( ph -> ( x e. C |-> D ) e. ( SMblFn ` S ) )
9 smfdiv.e 
 |-  E = { x e. C | D =/= 0 }
10 elinel1 
 |-  ( x e. ( A i^i E ) -> x e. A )
11 10 adantl 
 |-  ( ( ph /\ x e. ( A i^i E ) ) -> x e. A )
12 11 4 syldan 
 |-  ( ( ph /\ x e. ( A i^i E ) ) -> B e. RR )
13 12 recnd 
 |-  ( ( ph /\ x e. ( A i^i E ) ) -> B e. CC )
14 ssrab2 
 |-  { x e. C | D =/= 0 } C_ C
15 9 14 eqsstri 
 |-  E C_ C
16 elinel2 
 |-  ( x e. ( A i^i E ) -> x e. E )
17 15 16 sseldi 
 |-  ( x e. ( A i^i E ) -> x e. C )
18 17 adantl 
 |-  ( ( ph /\ x e. ( A i^i E ) ) -> x e. C )
19 18 6 syldan 
 |-  ( ( ph /\ x e. ( A i^i E ) ) -> D e. RR )
20 19 recnd 
 |-  ( ( ph /\ x e. ( A i^i E ) ) -> D e. CC )
21 9 eleq2i 
 |-  ( x e. E <-> x e. { x e. C | D =/= 0 } )
22 21 biimpi 
 |-  ( x e. E -> x e. { x e. C | D =/= 0 } )
23 rabidim2 
 |-  ( x e. { x e. C | D =/= 0 } -> D =/= 0 )
24 22 23 syl 
 |-  ( x e. E -> D =/= 0 )
25 16 24 syl 
 |-  ( x e. ( A i^i E ) -> D =/= 0 )
26 25 adantl 
 |-  ( ( ph /\ x e. ( A i^i E ) ) -> D =/= 0 )
27 13 20 26 divrecd 
 |-  ( ( ph /\ x e. ( A i^i E ) ) -> ( B / D ) = ( B x. ( 1 / D ) ) )
28 1 27 mpteq2da 
 |-  ( ph -> ( x e. ( A i^i E ) |-> ( B / D ) ) = ( x e. ( A i^i E ) |-> ( B x. ( 1 / D ) ) ) )
29 1red 
 |-  ( ( ph /\ x e. E ) -> 1 e. RR )
30 15 sseli 
 |-  ( x e. E -> x e. C )
31 30 adantl 
 |-  ( ( ph /\ x e. E ) -> x e. C )
32 31 6 syldan 
 |-  ( ( ph /\ x e. E ) -> D e. RR )
33 24 adantl 
 |-  ( ( ph /\ x e. E ) -> D =/= 0 )
34 29 32 33 redivcld 
 |-  ( ( ph /\ x e. E ) -> ( 1 / D ) e. RR )
35 1 2 5 6 8 9 smfrec 
 |-  ( ph -> ( x e. E |-> ( 1 / D ) ) e. ( SMblFn ` S ) )
36 1 2 3 4 34 7 35 smfmul 
 |-  ( ph -> ( x e. ( A i^i E ) |-> ( B x. ( 1 / D ) ) ) e. ( SMblFn ` S ) )
37 28 36 eqeltrd 
 |-  ( ph -> ( x e. ( A i^i E ) |-> ( B / D ) ) e. ( SMblFn ` S ) )