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 𝑥 𝜑
smfdiv.s ( 𝜑𝑆 ∈ SAlg )
smfdiv.a ( 𝜑𝐴𝑉 )
smfdiv.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
smfdiv.c ( 𝜑𝐶𝑊 )
smfdiv.d ( ( 𝜑𝑥𝐶 ) → 𝐷 ∈ ℝ )
smfdiv.m ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
smfdiv.n ( 𝜑 → ( 𝑥𝐶𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
smfdiv.e 𝐸 = { 𝑥𝐶𝐷 ≠ 0 }
Assertion smfdiv ( 𝜑 → ( 𝑥 ∈ ( 𝐴𝐸 ) ↦ ( 𝐵 / 𝐷 ) ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 smfdiv.x 𝑥 𝜑
2 smfdiv.s ( 𝜑𝑆 ∈ SAlg )
3 smfdiv.a ( 𝜑𝐴𝑉 )
4 smfdiv.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
5 smfdiv.c ( 𝜑𝐶𝑊 )
6 smfdiv.d ( ( 𝜑𝑥𝐶 ) → 𝐷 ∈ ℝ )
7 smfdiv.m ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
8 smfdiv.n ( 𝜑 → ( 𝑥𝐶𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
9 smfdiv.e 𝐸 = { 𝑥𝐶𝐷 ≠ 0 }
10 elinel1 ( 𝑥 ∈ ( 𝐴𝐸 ) → 𝑥𝐴 )
11 10 adantl ( ( 𝜑𝑥 ∈ ( 𝐴𝐸 ) ) → 𝑥𝐴 )
12 11 4 syldan ( ( 𝜑𝑥 ∈ ( 𝐴𝐸 ) ) → 𝐵 ∈ ℝ )
13 12 recnd ( ( 𝜑𝑥 ∈ ( 𝐴𝐸 ) ) → 𝐵 ∈ ℂ )
14 ssrab2 { 𝑥𝐶𝐷 ≠ 0 } ⊆ 𝐶
15 9 14 eqsstri 𝐸𝐶
16 elinel2 ( 𝑥 ∈ ( 𝐴𝐸 ) → 𝑥𝐸 )
17 15 16 sseldi ( 𝑥 ∈ ( 𝐴𝐸 ) → 𝑥𝐶 )
18 17 adantl ( ( 𝜑𝑥 ∈ ( 𝐴𝐸 ) ) → 𝑥𝐶 )
19 18 6 syldan ( ( 𝜑𝑥 ∈ ( 𝐴𝐸 ) ) → 𝐷 ∈ ℝ )
20 19 recnd ( ( 𝜑𝑥 ∈ ( 𝐴𝐸 ) ) → 𝐷 ∈ ℂ )
21 9 eleq2i ( 𝑥𝐸𝑥 ∈ { 𝑥𝐶𝐷 ≠ 0 } )
22 21 biimpi ( 𝑥𝐸𝑥 ∈ { 𝑥𝐶𝐷 ≠ 0 } )
23 rabidim2 ( 𝑥 ∈ { 𝑥𝐶𝐷 ≠ 0 } → 𝐷 ≠ 0 )
24 22 23 syl ( 𝑥𝐸𝐷 ≠ 0 )
25 16 24 syl ( 𝑥 ∈ ( 𝐴𝐸 ) → 𝐷 ≠ 0 )
26 25 adantl ( ( 𝜑𝑥 ∈ ( 𝐴𝐸 ) ) → 𝐷 ≠ 0 )
27 13 20 26 divrecd ( ( 𝜑𝑥 ∈ ( 𝐴𝐸 ) ) → ( 𝐵 / 𝐷 ) = ( 𝐵 · ( 1 / 𝐷 ) ) )
28 1 27 mpteq2da ( 𝜑 → ( 𝑥 ∈ ( 𝐴𝐸 ) ↦ ( 𝐵 / 𝐷 ) ) = ( 𝑥 ∈ ( 𝐴𝐸 ) ↦ ( 𝐵 · ( 1 / 𝐷 ) ) ) )
29 1red ( ( 𝜑𝑥𝐸 ) → 1 ∈ ℝ )
30 15 sseli ( 𝑥𝐸𝑥𝐶 )
31 30 adantl ( ( 𝜑𝑥𝐸 ) → 𝑥𝐶 )
32 31 6 syldan ( ( 𝜑𝑥𝐸 ) → 𝐷 ∈ ℝ )
33 24 adantl ( ( 𝜑𝑥𝐸 ) → 𝐷 ≠ 0 )
34 29 32 33 redivcld ( ( 𝜑𝑥𝐸 ) → ( 1 / 𝐷 ) ∈ ℝ )
35 1 2 5 6 8 9 smfrec ( 𝜑 → ( 𝑥𝐸 ↦ ( 1 / 𝐷 ) ) ∈ ( SMblFn ‘ 𝑆 ) )
36 1 2 3 4 34 7 35 smfmul ( 𝜑 → ( 𝑥 ∈ ( 𝐴𝐸 ) ↦ ( 𝐵 · ( 1 / 𝐷 ) ) ) ∈ ( SMblFn ‘ 𝑆 ) )
37 28 36 eqeltrd ( 𝜑 → ( 𝑥 ∈ ( 𝐴𝐸 ) ↦ ( 𝐵 / 𝐷 ) ) ∈ ( SMblFn ‘ 𝑆 ) )