Theorem smfmul

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

	Ref	Expression
Hypotheses	smfmul.x	⊢ Ⅎ 𝑥 𝜑
	smfmul.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfmul.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	smfmul.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	smfmul.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐷 ∈ ℝ )
	smfmul.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
	smfmul.n	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
Assertion	smfmul	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ ( 𝐵 · 𝐷 ) ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		smfmul.x	⊢ Ⅎ 𝑥 𝜑
2		smfmul.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfmul.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		smfmul.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
5		smfmul.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐷 ∈ ℝ )
6		smfmul.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
7		smfmul.n	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
8		nfv	⊢ Ⅎ 𝑎 𝜑
9		elinel1	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) → 𝑥 ∈ 𝐴 )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝑥 ∈ 𝐴 )
11	1 10	ssdf	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) ⊆ 𝐴 )
12		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
13	1 12 4	dmmptdf	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
14	13	eqcomd	⊢ ( 𝜑 → 𝐴 = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
15		eqid	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
16	2 6 15	smfdmss	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ∪ 𝑆 )
17	14 16	eqsstrd	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑆 )
18	11 17	sstrd	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) ⊆ ∪ 𝑆 )
19	10 4	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐵 ∈ ℝ )
20		elinel2	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) → 𝑥 ∈ 𝐶 )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝑥 ∈ 𝐶 )
22	21 5	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐷 ∈ ℝ )
23	19 22	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → ( 𝐵 · 𝐷 ) ∈ ℝ )
24		nfv	⊢ Ⅎ 𝑥 𝑎 ∈ ℝ
25	1 24	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑎 ∈ ℝ )
26	2	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑆 ∈ SAlg )
27	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐴 ∈ 𝑉 )
28	4	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
29	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑥 ∈ 𝐶 ) → 𝐷 ∈ ℝ )
30	6	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
31	7	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
33		fveq1	⊢ ( 𝑝 = 𝑞 → ( 𝑝 ‘ 2 ) = ( 𝑞 ‘ 2 ) )
34		fveq1	⊢ ( 𝑝 = 𝑞 → ( 𝑝 ‘ 3 ) = ( 𝑞 ‘ 3 ) )
35	33 34	oveq12d	⊢ ( 𝑝 = 𝑞 → ( ( 𝑝 ‘ 2 ) (,) ( 𝑝 ‘ 3 ) ) = ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) )
36	35	raleqdv	⊢ ( 𝑝 = 𝑞 → ( ∀ 𝑣 ∈ ( ( 𝑝 ‘ 2 ) (,) ( 𝑝 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 ↔ ∀ 𝑣 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 ) )
37	36	ralbidv	⊢ ( 𝑝 = 𝑞 → ( ∀ 𝑢 ∈ ( ( 𝑝 ‘ 0 ) (,) ( 𝑝 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑝 ‘ 2 ) (,) ( 𝑝 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 ↔ ∀ 𝑢 ∈ ( ( 𝑝 ‘ 0 ) (,) ( 𝑝 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 ) )
38		fveq1	⊢ ( 𝑝 = 𝑞 → ( 𝑝 ‘ 0 ) = ( 𝑞 ‘ 0 ) )
39		fveq1	⊢ ( 𝑝 = 𝑞 → ( 𝑝 ‘ 1 ) = ( 𝑞 ‘ 1 ) )
40	38 39	oveq12d	⊢ ( 𝑝 = 𝑞 → ( ( 𝑝 ‘ 0 ) (,) ( 𝑝 ‘ 1 ) ) = ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) )
41	40	raleqdv	⊢ ( 𝑝 = 𝑞 → ( ∀ 𝑢 ∈ ( ( 𝑝 ‘ 0 ) (,) ( 𝑝 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 ↔ ∀ 𝑢 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 ) )
42	37 41	bitrd	⊢ ( 𝑝 = 𝑞 → ( ∀ 𝑢 ∈ ( ( 𝑝 ‘ 0 ) (,) ( 𝑝 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑝 ‘ 2 ) (,) ( 𝑝 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 ↔ ∀ 𝑢 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 ) )
43	42	cbvrabv	⊢ { 𝑝 ∈ ( ℚ ↑m ( 0 ... 3 ) ) ∣ ∀ 𝑢 ∈ ( ( 𝑝 ‘ 0 ) (,) ( 𝑝 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑝 ‘ 2 ) (,) ( 𝑝 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 } = { 𝑞 ∈ ( ℚ ↑m ( 0 ... 3 ) ) ∣ ∀ 𝑢 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 }
44		eqid	⊢ ( 𝑞 ∈ { 𝑝 ∈ ( ℚ ↑m ( 0 ... 3 ) ) ∣ ∀ 𝑢 ∈ ( ( 𝑝 ‘ 0 ) (,) ( 𝑝 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑝 ‘ 2 ) (,) ( 𝑝 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 } ↦ { 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∣ ( 𝐵 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝐷 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) } ) = ( 𝑞 ∈ { 𝑝 ∈ ( ℚ ↑m ( 0 ... 3 ) ) ∣ ∀ 𝑢 ∈ ( ( 𝑝 ‘ 0 ) (,) ( 𝑝 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑝 ‘ 2 ) (,) ( 𝑝 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑎 } ↦ { 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∣ ( 𝐵 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝐷 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) } )
45	25 26 27 28 29 30 31 32 43 44	smfmullem4	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∣ ( 𝐵 · 𝐷 ) < 𝑎 } ∈ ( 𝑆 ↾t ( 𝐴 ∩ 𝐶 ) ) )
46	1 8 2 18 23 45	issmfdmpt	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ ( 𝐵 · 𝐷 ) ) ∈ ( SMblFn ‘ 𝑆 ) )