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 x φ
smfdiv.s φ S SAlg
smfdiv.a φ A V
smfdiv.b φ x A B
smfdiv.c φ C W
smfdiv.d φ x C D
smfdiv.m φ x A B SMblFn S
smfdiv.n φ x C D SMblFn S
smfdiv.e E = x C | D 0
Assertion smfdiv φ x A E B D SMblFn S

Proof

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