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	sselid	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) → 𝑥 ∈ 𝐶 )
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 ‘ 𝑆 ) )