Theorem mbfres2cn

Description: Measurability of a piecewise function: if F is measurable on subsets B and C of its domain, and these pieces make up all of A , then F is measurable on the whole domain. Similar to mbfres2 but here the theorem is extended to complex-valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	mbfres2cn.f	$$⊢\phi \to F:A⟶ℂ$$
	mbfres2cn.b	$$⊢\phi \to {F\upharpoonright }_B\in MblFn$$
	mbfres2cn.c	$$⊢\phi \to {F\upharpoonright }_C\in MblFn$$
	mbfres2cn.a	$$⊢\phi \to B\cup C=A$$
Assertion	mbfres2cn	$$⊢\phi \to F\in MblFn$$

Proof

Step	Hyp	Ref	Expression
1		mbfres2cn.f	$$⊢\phi \to F:A⟶ℂ$$
2		mbfres2cn.b	$$⊢\phi \to {F\upharpoonright }_B\in MblFn$$
3		mbfres2cn.c	$$⊢\phi \to {F\upharpoonright }_C\in MblFn$$
4		mbfres2cn.a	$$⊢\phi \to B\cup C=A$$
5		ref	$$⊢\Re :ℂ⟶ℝ$$
6		fco	$$⊢\left(\Re :ℂ⟶ℝ\wedge F:A⟶ℂ\right)\to \left(\Re \circ F\right):A⟶ℝ$$
7	5 1 6	sylancr	$$⊢\phi \to \left(\Re \circ F\right):A⟶ℝ$$
8		resco	$$⊢{\left(\Re \circ F\right)\upharpoonright }_B=\Re \circ \left({F\upharpoonright }_B\right)$$
9		fresin	$$⊢F:A⟶ℂ\to \left({F\upharpoonright }_B\right):A\cap B⟶ℂ$$
10		ismbfcn	$$⊢\left({F\upharpoonright }_B\right):A\cap B⟶ℂ\to \left({F\upharpoonright }_B\in MblFn\leftrightarrow \left(\Re \circ \left({F\upharpoonright }_B\right)\in MblFn\wedge \Im \circ \left({F\upharpoonright }_B\right)\in MblFn\right)\right)$$
11	1 9 10	3syl	$$⊢\phi \to \left({F\upharpoonright }_B\in MblFn\leftrightarrow \left(\Re \circ \left({F\upharpoonright }_B\right)\in MblFn\wedge \Im \circ \left({F\upharpoonright }_B\right)\in MblFn\right)\right)$$
12	2 11	mpbid	$$⊢\phi \to \left(\Re \circ \left({F\upharpoonright }_B\right)\in MblFn\wedge \Im \circ \left({F\upharpoonright }_B\right)\in MblFn\right)$$
13	12	simpld	$$⊢\phi \to \Re \circ \left({F\upharpoonright }_B\right)\in MblFn$$
14	8 13	eqeltrid	$$⊢\phi \to {\left(\Re \circ F\right)\upharpoonright }_B\in MblFn$$
15		resco	$$⊢{\left(\Re \circ F\right)\upharpoonright }_C=\Re \circ \left({F\upharpoonright }_C\right)$$
16		fresin	$$⊢F:A⟶ℂ\to \left({F\upharpoonright }_C\right):A\cap C⟶ℂ$$
17		ismbfcn	$$⊢\left({F\upharpoonright }_C\right):A\cap C⟶ℂ\to \left({F\upharpoonright }_C\in MblFn\leftrightarrow \left(\Re \circ \left({F\upharpoonright }_C\right)\in MblFn\wedge \Im \circ \left({F\upharpoonright }_C\right)\in MblFn\right)\right)$$
18	1 16 17	3syl	$$⊢\phi \to \left({F\upharpoonright }_C\in MblFn\leftrightarrow \left(\Re \circ \left({F\upharpoonright }_C\right)\in MblFn\wedge \Im \circ \left({F\upharpoonright }_C\right)\in MblFn\right)\right)$$
19	3 18	mpbid	$$⊢\phi \to \left(\Re \circ \left({F\upharpoonright }_C\right)\in MblFn\wedge \Im \circ \left({F\upharpoonright }_C\right)\in MblFn\right)$$
20	19	simpld	$$⊢\phi \to \Re \circ \left({F\upharpoonright }_C\right)\in MblFn$$
21	15 20	eqeltrid	$$⊢\phi \to {\left(\Re \circ F\right)\upharpoonright }_C\in MblFn$$
22	7 14 21 4	mbfres2	$$⊢\phi \to \Re \circ F\in MblFn$$
23		imf	$$⊢\Im :ℂ⟶ℝ$$
24		fco	$$⊢\left(\Im :ℂ⟶ℝ\wedge F:A⟶ℂ\right)\to \left(\Im \circ F\right):A⟶ℝ$$
25	23 1 24	sylancr	$$⊢\phi \to \left(\Im \circ F\right):A⟶ℝ$$
26		resco	$$⊢{\left(\Im \circ F\right)\upharpoonright }_B=\Im \circ \left({F\upharpoonright }_B\right)$$
27	12	simprd	$$⊢\phi \to \Im \circ \left({F\upharpoonright }_B\right)\in MblFn$$
28	26 27	eqeltrid	$$⊢\phi \to {\left(\Im \circ F\right)\upharpoonright }_B\in MblFn$$
29		resco	$$⊢{\left(\Im \circ F\right)\upharpoonright }_C=\Im \circ \left({F\upharpoonright }_C\right)$$
30	19	simprd	$$⊢\phi \to \Im \circ \left({F\upharpoonright }_C\right)\in MblFn$$
31	29 30	eqeltrid	$$⊢\phi \to {\left(\Im \circ F\right)\upharpoonright }_C\in MblFn$$
32	25 28 31 4	mbfres2	$$⊢\phi \to \Im \circ F\in MblFn$$
33		ismbfcn	$$⊢F:A⟶ℂ\to \left(F\in MblFn\leftrightarrow \left(\Re \circ F\in MblFn\wedge \Im \circ F\in MblFn\right)\right)$$
34	1 33	syl	$$⊢\phi \to \left(F\in MblFn\leftrightarrow \left(\Re \circ F\in MblFn\wedge \Im \circ F\in MblFn\right)\right)$$
35	22 32 34	mpbir2and	$$⊢\phi \to F\in MblFn$$