smfmullem4

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	smfmullem4.x	$⊢ Ⅎ x φ$
	smfmullem4.s	$⊢ φ \to S \in SAlg$
	smfmullem4.a	$⊢ φ \to A \in V$
	smfmullem4.b	$⊢ (φ \land x \in A) \to B \in ℝ$
	smfmullem4.d	$⊢ (φ \land x \in C) \to D \in ℝ$
	smfmullem4.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
	smfmullem4.n	$⊢ φ \to (x \in C ⟼ D) \in SMblFn (S)$
	smfmullem4.r	$⊢ φ \to R \in ℝ$
	smfmullem4.k	$⊢ K = \{q \in (ℚ^{(0 \dots 3)}) \| \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < R\}$
	smfmullem4.e	$⊢ E = (q \in K ⟼ \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\})$
Assertion	smfmullem4	$⊢ φ \to \{x \in (A \cap C) \| B D < R\} \in (S ↾_{𝑡} (A \cap C))$

Proof

Step	Hyp	Ref	Expression
1		smfmullem4.x	$⊢ Ⅎ x φ$
2		smfmullem4.s	$⊢ φ \to S \in SAlg$
3		smfmullem4.a	$⊢ φ \to A \in V$
4		smfmullem4.b	$⊢ (φ \land x \in A) \to B \in ℝ$
5		smfmullem4.d	$⊢ (φ \land x \in C) \to D \in ℝ$
6		smfmullem4.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
7		smfmullem4.n	$⊢ φ \to (x \in C ⟼ D) \in SMblFn (S)$
8		smfmullem4.r	$⊢ φ \to R \in ℝ$
9		smfmullem4.k	$⊢ K = \{q \in (ℚ^{(0 \dots 3)}) \| \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < R\}$
10		smfmullem4.e	$⊢ E = (q \in K ⟼ \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\})$
11	8	3ad2ant1	$⊢ (φ \land x \in (A \cap C) \land B D < R) \to R \in ℝ$
12		inss1	$⊢ A \cap C \subseteq A$
13	12	a1i	$⊢ φ \to A \cap C \subseteq A$
14	13	sselda	$⊢ (φ \land x \in (A \cap C)) \to x \in A$
15	14 4	syldan	$⊢ (φ \land x \in (A \cap C)) \to B \in ℝ$
16	15	3adant3	$⊢ (φ \land x \in (A \cap C) \land B D < R) \to B \in ℝ$
17		elinel2	$⊢ x \in (A \cap C) \to x \in C$
18	17	adantl	$⊢ (φ \land x \in (A \cap C)) \to x \in C$
19	18 5	syldan	$⊢ (φ \land x \in (A \cap C)) \to D \in ℝ$
20	19	3adant3	$⊢ (φ \land x \in (A \cap C) \land B D < R) \to D \in ℝ$
21		simp3	$⊢ (φ \land x \in (A \cap C) \land B D < R) \to B D < R$
22		eqid	$⊢ \frac{R - B D}{1 + \|B\| + \|D\|} = \frac{R - B D}{1 + \|B\| + \|D\|}$
23		eqid	$⊢ if (1 \leq \frac{R - B D}{1 + \|B\| + \|D\|}, 1, \frac{R - B D}{1 + \|B\| + \|D\|}) = if (1 \leq \frac{R - B D}{1 + \|B\| + \|D\|}, 1, \frac{R - B D}{1 + \|B\| + \|D\|})$
24	11 9 16 20 21 22 23	smfmullem3	$⊢ (φ \land x \in (A \cap C) \land B D < R) \to \exists q \in K (B \in (q (0), q (1)) \land D \in (q (2), q (3)))$
25		rabid	$⊢ x \in \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\} \leftrightarrow (x \in (A \cap C) \land (B \in (q (0), q (1)) \land D \in (q (2), q (3))))$
26	25	bicomi	$⊢ (x \in (A \cap C) \land (B \in (q (0), q (1)) \land D \in (q (2), q (3)))) \leftrightarrow x \in \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\}$
27	26	biimpi	$⊢ (x \in (A \cap C) \land (B \in (q (0), q (1)) \land D \in (q (2), q (3)))) \to x \in \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\}$
28	27	adantll	$⊢ ((φ \land x \in (A \cap C)) \land (B \in (q (0), q (1)) \land D \in (q (2), q (3)))) \to x \in \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\}$
29	28	adantlr	$⊢ (((φ \land x \in (A \cap C)) \land q \in K) \land (B \in (q (0), q (1)) \land D \in (q (2), q (3)))) \to x \in \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\}$
30	10	a1i	$⊢ φ \to E = (q \in K ⟼ \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\})$
31		inrab	$⊢ \{x \in (A \cap C) \| B \in (q (0), q (1))\} \cap \{x \in (A \cap C) \| D \in (q (2), q (3))\} = \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\}$
32	3 13	ssexd	$⊢ φ \to A \cap C \in V$
33		eqid	$⊢ S ↾_{𝑡} (A \cap C) = S ↾_{𝑡} (A \cap C)$
34	2 32 33	subsalsal	$⊢ φ \to S ↾_{𝑡} (A \cap C) \in SAlg$
35	34	adantr	$⊢ (φ \land q \in K) \to S ↾_{𝑡} (A \cap C) \in SAlg$
36		nfv	$⊢ Ⅎ x q \in K$
37	1 36	nfan	$⊢ Ⅎ x (φ \land q \in K)$
38	2	adantr	$⊢ (φ \land q \in K) \to S \in SAlg$
39	32	adantr	$⊢ (φ \land q \in K) \to A \cap C \in V$
40	15	adantlr	$⊢ ((φ \land q \in K) \land x \in (A \cap C)) \to B \in ℝ$
41	2 6 13	sssmfmpt	$⊢ φ \to (x \in (A \cap C) ⟼ B) \in SMblFn (S)$
42	41	adantr	$⊢ (φ \land q \in K) \to (x \in (A \cap C) ⟼ B) \in SMblFn (S)$
43		ssrab2	$⊢ \{q \in (ℚ^{(0 \dots 3)}) \| \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < R\} \subseteq ℚ^{(0 \dots 3)}$
44	9 43	eqsstri	$⊢ K \subseteq ℚ^{(0 \dots 3)}$
45		reex	$⊢ ℝ \in V$
46		qssre	$⊢ ℚ \subseteq ℝ$
47		mapss	$⊢ (ℝ \in V \land ℚ \subseteq ℝ) \to ℚ^{(0 \dots 3)} \subseteq ℝ^{(0 \dots 3)}$
48	45 46 47	mp2an	$⊢ ℚ^{(0 \dots 3)} \subseteq ℝ^{(0 \dots 3)}$
49	44 48	sstri	$⊢ K \subseteq ℝ^{(0 \dots 3)}$
50		id	$⊢ q \in K \to q \in K$
51	49 50	sseldi	$⊢ q \in K \to q \in (ℝ^{(0 \dots 3)})$
52	45	a1i	$⊢ q \in K \to ℝ \in V$
53		ovexd	$⊢ q \in K \to (0 \dots 3) \in V$
54	52 53	elmapd	$⊢ q \in K \to (q \in (ℝ^{(0 \dots 3)}) \leftrightarrow q : (0 \dots 3) ⟶ ℝ)$
55	51 54	mpbid	$⊢ q \in K \to q : (0 \dots 3) ⟶ ℝ$
56		0z	$⊢ 0 \in ℤ$
57		3z	$⊢ 3 \in ℤ$
58		0re	$⊢ 0 \in ℝ$
59		3re	$⊢ 3 \in ℝ$
60		3pos	$⊢ 0 < 3$
61	58 59 60	ltleii	$⊢ 0 \leq 3$
62	56 57 61	3pm3.2i	$⊢ (0 \in ℤ \land 3 \in ℤ \land 0 \leq 3)$
63		eluz2	$⊢ 3 \in ℤ_{\geq 0} \leftrightarrow (0 \in ℤ \land 3 \in ℤ \land 0 \leq 3)$
64	62 63	mpbir	$⊢ 3 \in ℤ_{\geq 0}$
65		eluzfz1	$⊢ 3 \in ℤ_{\geq 0} \to 0 \in (0 \dots 3)$
66	64 65	ax-mp	$⊢ 0 \in (0 \dots 3)$
67	66	a1i	$⊢ q \in K \to 0 \in (0 \dots 3)$
68	55 67	ffvelrnd	$⊢ q \in K \to q (0) \in ℝ$
69	68	adantl	$⊢ (φ \land q \in K) \to q (0) \in ℝ$
70	69	rexrd	$⊢ (φ \land q \in K) \to q (0) \in ℝ^{*}$
71		0le1	$⊢ 0 \leq 1$
72		1re	$⊢ 1 \in ℝ$
73		1lt3	$⊢ 1 < 3$
74	72 59 73	ltleii	$⊢ 1 \leq 3$
75	71 74	pm3.2i	$⊢ (0 \leq 1 \land 1 \leq 3)$
76		1z	$⊢ 1 \in ℤ$
77		elfz	$⊢ (1 \in ℤ \land 0 \in ℤ \land 3 \in ℤ) \to (1 \in (0 \dots 3) \leftrightarrow (0 \leq 1 \land 1 \leq 3))$
78	76 56 57 77	mp3an	$⊢ 1 \in (0 \dots 3) \leftrightarrow (0 \leq 1 \land 1 \leq 3)$
79	75 78	mpbir	$⊢ 1 \in (0 \dots 3)$
80	79	a1i	$⊢ q \in K \to 1 \in (0 \dots 3)$
81	55 80	ffvelrnd	$⊢ q \in K \to q (1) \in ℝ$
82	81	adantl	$⊢ (φ \land q \in K) \to q (1) \in ℝ$
83	82	rexrd	$⊢ (φ \land q \in K) \to q (1) \in ℝ^{*}$
84	37 38 39 40 42 70 83	smfpimioompt	$⊢ (φ \land q \in K) \to \{x \in (A \cap C) \| B \in (q (0), q (1))\} \in (S ↾_{𝑡} (A \cap C))$
85	19	adantlr	$⊢ ((φ \land q \in K) \land x \in (A \cap C)) \to D \in ℝ$
86	1 18	ssdf	$⊢ φ \to A \cap C \subseteq C$
87	2 7 86	sssmfmpt	$⊢ φ \to (x \in (A \cap C) ⟼ D) \in SMblFn (S)$
88	87	adantr	$⊢ (φ \land q \in K) \to (x \in (A \cap C) ⟼ D) \in SMblFn (S)$
89		0le2	$⊢ 0 \leq 2$
90		2re	$⊢ 2 \in ℝ$
91		2lt3	$⊢ 2 < 3$
92	90 59 91	ltleii	$⊢ 2 \leq 3$
93	89 92	pm3.2i	$⊢ (0 \leq 2 \land 2 \leq 3)$
94		2z	$⊢ 2 \in ℤ$
95		elfz	$⊢ (2 \in ℤ \land 0 \in ℤ \land 3 \in ℤ) \to (2 \in (0 \dots 3) \leftrightarrow (0 \leq 2 \land 2 \leq 3))$
96	94 56 57 95	mp3an	$⊢ 2 \in (0 \dots 3) \leftrightarrow (0 \leq 2 \land 2 \leq 3)$
97	93 96	mpbir	$⊢ 2 \in (0 \dots 3)$
98	97	a1i	$⊢ q \in K \to 2 \in (0 \dots 3)$
99	55 98	ffvelrnd	$⊢ q \in K \to q (2) \in ℝ$
100	99	adantl	$⊢ (φ \land q \in K) \to q (2) \in ℝ$
101	100	rexrd	$⊢ (φ \land q \in K) \to q (2) \in ℝ^{*}$
102		eluzfz2	$⊢ 3 \in ℤ_{\geq 0} \to 3 \in (0 \dots 3)$
103	64 102	ax-mp	$⊢ 3 \in (0 \dots 3)$
104	103	a1i	$⊢ q \in K \to 3 \in (0 \dots 3)$
105	55 104	ffvelrnd	$⊢ q \in K \to q (3) \in ℝ$
106	105	adantl	$⊢ (φ \land q \in K) \to q (3) \in ℝ$
107	106	rexrd	$⊢ (φ \land q \in K) \to q (3) \in ℝ^{*}$
108	37 38 39 85 88 101 107	smfpimioompt	$⊢ (φ \land q \in K) \to \{x \in (A \cap C) \| D \in (q (2), q (3))\} \in (S ↾_{𝑡} (A \cap C))$
109	35 84 108	salincld	$⊢ (φ \land q \in K) \to \{x \in (A \cap C) \| B \in (q (0), q (1))\} \cap \{x \in (A \cap C) \| D \in (q (2), q (3))\} \in (S ↾_{𝑡} (A \cap C))$
110	31 109	eqeltrrid	$⊢ (φ \land q \in K) \to \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\} \in (S ↾_{𝑡} (A \cap C))$
111	110	elexd	$⊢ (φ \land q \in K) \to \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\} \in V$
112	30 111	fvmpt2d	$⊢ (φ \land q \in K) \to E (q) = \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\}$
113	112	eqcomd	$⊢ (φ \land q \in K) \to \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\} = E (q)$
114	113	adantlr	$⊢ ((φ \land x \in (A \cap C)) \land q \in K) \to \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\} = E (q)$
115	114	adantr	$⊢ (((φ \land x \in (A \cap C)) \land q \in K) \land (B \in (q (0), q (1)) \land D \in (q (2), q (3)))) \to \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\} = E (q)$
116	29 115	eleqtrd	$⊢ (((φ \land x \in (A \cap C)) \land q \in K) \land (B \in (q (0), q (1)) \land D \in (q (2), q (3)))) \to x \in E (q)$
117	116	ex	$⊢ ((φ \land x \in (A \cap C)) \land q \in K) \to ((B \in (q (0), q (1)) \land D \in (q (2), q (3))) \to x \in E (q))$
118	117	3adantl3	$⊢ ((φ \land x \in (A \cap C) \land B D < R) \land q \in K) \to ((B \in (q (0), q (1)) \land D \in (q (2), q (3))) \to x \in E (q))$
119	118	reximdva	$⊢ (φ \land x \in (A \cap C) \land B D < R) \to (\exists q \in K (B \in (q (0), q (1)) \land D \in (q (2), q (3))) \to \exists q \in K x \in E (q))$
120	24 119	mpd	$⊢ (φ \land x \in (A \cap C) \land B D < R) \to \exists q \in K x \in E (q)$
121		eliun	$⊢ x \in ⋃_{q \in K} E (q) \leftrightarrow \exists q \in K x \in E (q)$
122	120 121	sylibr	$⊢ (φ \land x \in (A \cap C) \land B D < R) \to x \in ⋃_{q \in K} E (q)$
123	122	3exp	$⊢ φ \to (x \in (A \cap C) \to (B D < R \to x \in ⋃_{q \in K} E (q)))$
124	1 123	ralrimi	$⊢ φ \to \forall x \in (A \cap C) (B D < R \to x \in ⋃_{q \in K} E (q))$
125	36	nfci	$⊢ \underline{Ⅎ} x K$
126		nfrab1	$⊢ \underline{Ⅎ} x \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\}$
127	125 126	nfmpt	$⊢ \underline{Ⅎ} x (q \in K ⟼ \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\})$
128	10 127	nfcxfr	$⊢ \underline{Ⅎ} x E$
129		nfcv	$⊢ \underline{Ⅎ} x q$
130	128 129	nffv	$⊢ \underline{Ⅎ} x E (q)$
131	125 130	nfiun	$⊢ \underline{Ⅎ} x ⋃_{q \in K} E (q)$
132	131	rabssf	$⊢ \{x \in (A \cap C) \| B D < R\} \subseteq ⋃_{q \in K} E (q) \leftrightarrow \forall x \in (A \cap C) (B D < R \to x \in ⋃_{q \in K} E (q))$
133	124 132	sylibr	$⊢ φ \to \{x \in (A \cap C) \| B D < R\} \subseteq ⋃_{q \in K} E (q)$
134		ssrab2	$⊢ \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\} \subseteq A \cap C$
135	112 134	eqsstrdi	$⊢ (φ \land q \in K) \to E (q) \subseteq A \cap C$
136		simpr	$⊢ ((φ \land q \in K) \land x \in E (q)) \to x \in E (q)$
137	112	adantr	$⊢ ((φ \land q \in K) \land x \in E (q)) \to E (q) = \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\}$
138	136 137	eleqtrd	$⊢ ((φ \land q \in K) \land x \in E (q)) \to x \in \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\}$
139		rabidim2	$⊢ x \in \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\} \to (B \in (q (0), q (1)) \land D \in (q (2), q (3)))$
140	138 139	syl	$⊢ ((φ \land q \in K) \land x \in E (q)) \to (B \in (q (0), q (1)) \land D \in (q (2), q (3)))$
141	140	simprd	$⊢ ((φ \land q \in K) \land x \in E (q)) \to D \in (q (2), q (3))$
142	140	simpld	$⊢ ((φ \land q \in K) \land x \in E (q)) \to B \in (q (0), q (1))$
143	50 9	eleqtrdi	$⊢ q \in K \to q \in \{q \in (ℚ^{(0 \dots 3)}) \| \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < R\}$
144		rabidim2	$⊢ q \in \{q \in (ℚ^{(0 \dots 3)}) \| \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < R\} \to \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < R$
145	143 144	syl	$⊢ q \in K \to \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < R$
146	145	ad2antlr	$⊢ ((φ \land q \in K) \land x \in E (q)) \to \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < R$
147		oveq1	$⊢ u = B \to u v = B v$
148	147	breq1d	$⊢ u = B \to (u v < R \leftrightarrow B v < R)$
149	148	ralbidv	$⊢ u = B \to (\forall v \in (q (2), q (3)) u v < R \leftrightarrow \forall v \in (q (2), q (3)) B v < R)$
150	149	rspcva	$⊢ (B \in (q (0), q (1)) \land \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < R) \to \forall v \in (q (2), q (3)) B v < R$
151	142 146 150	syl2anc	$⊢ ((φ \land q \in K) \land x \in E (q)) \to \forall v \in (q (2), q (3)) B v < R$
152		oveq2	$⊢ v = D \to B v = B D$
153	152	breq1d	$⊢ v = D \to (B v < R \leftrightarrow B D < R)$
154	153	rspcva	$⊢ (D \in (q (2), q (3)) \land \forall v \in (q (2), q (3)) B v < R) \to B D < R$
155	141 151 154	syl2anc	$⊢ ((φ \land q \in K) \land x \in E (q)) \to B D < R$
156	155	ex	$⊢ (φ \land q \in K) \to (x \in E (q) \to B D < R)$
157	37 156	ralrimi	$⊢ (φ \land q \in K) \to \forall x \in E (q) B D < R$
158	135 157	jca	$⊢ (φ \land q \in K) \to (E (q) \subseteq A \cap C \land \forall x \in E (q) B D < R)$
159		nfcv	$⊢ \underline{Ⅎ} x (A \cap C)$
160	130 159	ssrabf	$⊢ E (q) \subseteq \{x \in (A \cap C) \| B D < R\} \leftrightarrow (E (q) \subseteq A \cap C \land \forall x \in E (q) B D < R)$
161	158 160	sylibr	$⊢ (φ \land q \in K) \to E (q) \subseteq \{x \in (A \cap C) \| B D < R\}$
162	161	iunssd	$⊢ φ \to ⋃_{q \in K} E (q) \subseteq \{x \in (A \cap C) \| B D < R\}$
163	133 162	eqssd	$⊢ φ \to \{x \in (A \cap C) \| B D < R\} = ⋃_{q \in K} E (q)$
164		ovex	$⊢ ℚ^{(0 \dots 3)} \in V$
165		ssdomg	$⊢ ℚ^{(0 \dots 3)} \in V \to (K \subseteq ℚ^{(0 \dots 3)} \to K ≼ (ℚ^{(0 \dots 3)}))$
166	164 165	ax-mp	$⊢ K \subseteq ℚ^{(0 \dots 3)} \to K ≼ (ℚ^{(0 \dots 3)})$
167	44 166	ax-mp	$⊢ K ≼ (ℚ^{(0 \dots 3)})$
168		qct	$⊢ ℚ ≼ ω$
169	168	a1i	$⊢ ⊤ \to ℚ ≼ ω$
170		fzfid	$⊢ ⊤ \to (0 \dots 3) \in Fin$
171	169 170	mpct	$⊢ ⊤ \to (ℚ^{(0 \dots 3)}) ≼ ω$
172	171	mptru	$⊢ (ℚ^{(0 \dots 3)}) ≼ ω$
173		domtr	$⊢ (K ≼ (ℚ^{(0 \dots 3)}) \land (ℚ^{(0 \dots 3)}) ≼ ω) \to K ≼ ω$
174	167 172 173	mp2an	$⊢ K ≼ ω$
175	174	a1i	$⊢ φ \to K ≼ ω$
176	110 10	fmptd	$⊢ φ \to E : K ⟶ S ↾_{𝑡} (A \cap C)$
177	176	ffvelrnda	$⊢ (φ \land q \in K) \to E (q) \in (S ↾_{𝑡} (A \cap C))$
178	34 175 177	saliuncl	$⊢ φ \to ⋃_{q \in K} E (q) \in (S ↾_{𝑡} (A \cap C))$
179	163 178	eqeltrd	$⊢ φ \to \{x \in (A \cap C) \| B D < R\} \in (S ↾_{𝑡} (A \cap C))$

Metamath Proof Explorer

Theorem smfmullem4

Proof