Theorem iblss2

Description: Change the domain of an integrability predicate. (Contributed by Mario Carneiro, 13-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypotheses	iblss2.1	$$⊢\phi \to A\subseteq B$$
	iblss2.2	$$⊢\phi \to B\in \mathrm{dom}vol$$
	iblss2.3	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
	iblss2.4	$$⊢\left(\phi \wedge x\in \left(B\setminus A\right)\right)\to C=0$$
	iblss2.5	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
Assertion	iblss2	$$⊢\phi \to \left(x\in B⟼C\right)\in {𝐿}^1$$

Proof

Step	Hyp	Ref	Expression
1		iblss2.1	$$⊢\phi \to A\subseteq B$$
2		iblss2.2	$$⊢\phi \to B\in \mathrm{dom}vol$$
3		iblss2.3	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
4		iblss2.4	$$⊢\left(\phi \wedge x\in \left(B\setminus A\right)\right)\to C=0$$
5		iblss2.5	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
6		iblmbf	$$⊢\left(x\in A⟼C\right)\in {𝐿}^1\to \left(x\in A⟼C\right)\in MblFn$$
7	5 6	syl	$$⊢\phi \to \left(x\in A⟼C\right)\in MblFn$$
8	1 2 3 4 7	mbfss	$$⊢\phi \to \left(x\in B⟼C\right)\in MblFn$$
9	1	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to A\subseteq B$$
10	9	sselda	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to x\in B$$
11	10	iftrued	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
12		iftrue	$$⊢x\in A\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
13	12	adantl	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
14	11 13	eqtr4d	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
15		ifid	$$⊢if\left(x\in B,0,0\right)=0$$
16		simplll	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to \phi$$
17		simpr	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to x\in B$$
18		simplr	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to \neg x\in A$$
19	17 18	eldifd	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to x\in \left(B\setminus A\right)$$
20	16 19 4	syl2anc	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to C=0$$
21	20	oveq1d	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to \frac{C}{{\mathrm{i}}^k}=\frac{0}{{\mathrm{i}}^k}$$
22		simpllr	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to k\in \left(0\dots 3\right)$$
23		elfzelz	$$⊢k\in \left(0\dots 3\right)\to k\in \mathbb{Z}$$
24		ax-icn	$$⊢\mathrm{i}\in ℂ$$
25		ine0	$$⊢\mathrm{i}\ne 0$$
26		expclz	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\in ℂ$$
27		expne0i	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\ne 0$$
28	26 27	div0d	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to \frac{0}{{\mathrm{i}}^k}=0$$
29	24 25 28	mp3an12	$$⊢k\in \mathbb{Z}\to \frac{0}{{\mathrm{i}}^k}=0$$
30	22 23 29	3syl	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to \frac{0}{{\mathrm{i}}^k}=0$$
31	21 30	eqtrd	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to \frac{C}{{\mathrm{i}}^k}=0$$
32	31	fveq2d	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(0\right)$$
33		re0	$$⊢\Re \left(0\right)=0$$
34	32 33	eqtrdi	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=0$$
35	34	ifeq1d	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),0,0\right)$$
36		ifid	$$⊢if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),0,0\right)=0$$
37	35 36	eqtrdi	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\wedge x\in B\right)\to if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=0$$
38	37	ifeq1da	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\to if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(x\in B,0,0\right)$$
39		iffalse	$$⊢\neg x\in A\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=0$$
40	39	adantl	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=0$$
41	15 38 40	3eqtr4a	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\to if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
42	14 41	pm2.61dan	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
43		ifan	$$⊢if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
44		ifan	$$⊢if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
45	42 43 44	3eqtr4g	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
46	45	mpteq2dv	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to \left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
47	46	fveq2d	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
48		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
49		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
50	48 49 5 3	iblitg	$$⊢\left(\phi \wedge k\in \mathbb{Z}\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
51	23 50	sylan2	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
52	47 51	eqeltrd	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
53	52	ralrimiva	$$⊢\phi \to \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
54		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
55		eqidd	$$⊢\left(\phi \wedge x\in B\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
56		elun	$$⊢x\in \left(A\cup \left(B\setminus A\right)\right)\leftrightarrow \left(x\in A\vee x\in \left(B\setminus A\right)\right)$$
57		undif2	$$⊢A\cup \left(B\setminus A\right)=A\cup B$$
58		ssequn1	$$⊢A\subseteq B\leftrightarrow A\cup B=B$$
59	1 58	sylib	$$⊢\phi \to A\cup B=B$$
60	57 59	syl5eq	$$⊢\phi \to A\cup \left(B\setminus A\right)=B$$
61	60	eleq2d	$$⊢\phi \to \left(x\in \left(A\cup \left(B\setminus A\right)\right)\leftrightarrow x\in B\right)$$
62	56 61	bitr3id	$$⊢\phi \to \left(\left(x\in A\vee x\in \left(B\setminus A\right)\right)\leftrightarrow x\in B\right)$$
63	62	biimpar	$$⊢\left(\phi \wedge x\in B\right)\to \left(x\in A\vee x\in \left(B\setminus A\right)\right)$$
64	7 3	mbfmptcl	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℂ$$
65		0cn	$$⊢0\in ℂ$$
66	4 65	eqeltrdi	$$⊢\left(\phi \wedge x\in \left(B\setminus A\right)\right)\to C\in ℂ$$
67	64 66	jaodan	$$⊢\left(\phi \wedge \left(x\in A\vee x\in \left(B\setminus A\right)\right)\right)\to C\in ℂ$$
68	63 67	syldan	$$⊢\left(\phi \wedge x\in B\right)\to C\in ℂ$$
69	54 55 68	isibl2	$$⊢\phi \to \left(\left(x\in B⟼C\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in B⟼C\right)\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)\right)$$
70	8 53 69	mpbir2and	$$⊢\phi \to \left(x\in B⟼C\right)\in {𝐿}^1$$