Theorem isibl

Description: The predicate " F is integrable". The "integrable" predicate corresponds roughly to the range of validity of S. A Bd x , which is to say that the expression S. A B d x doesn't make sense unless ( x e. A |-> B ) e. L^1 . (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypotheses	isibl.1	$$⊢\phi \to G=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)$$
	isibl.2	$$⊢\left(\phi \wedge x\in A\right)\to T=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
	isibl.3	$$⊢\phi \to \mathrm{dom}F=A$$
	isibl.4	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=B$$
Assertion	isibl	$$⊢\phi \to \left(F\in {𝐿}^1\leftrightarrow \left(F\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(G\right)\in ℝ\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isibl.1	$$⊢\phi \to G=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)$$
2		isibl.2	$$⊢\left(\phi \wedge x\in A\right)\to T=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
3		isibl.3	$$⊢\phi \to \mathrm{dom}F=A$$
4		isibl.4	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=B$$
5		fvex	$$⊢\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\in \mathrm{V}$$
6		breq2	$$⊢y=\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\to \left(0\le y\leftrightarrow 0\le \Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\right)$$
7	6	anbi2d	$$⊢y=\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\to \left(\left(x\in \mathrm{dom}f\wedge 0\le y\right)\leftrightarrow \left(x\in \mathrm{dom}f\wedge 0\le \Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\right)\right)$$
8		id	$$⊢y=\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\to y=\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)$$
9	7 8	ifbieq1d	$$⊢y=\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\to if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)=if\left(\left(x\in \mathrm{dom}f\wedge 0\le \Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right),0\right)$$
10	5 9	csbie	$$⊢⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)=if\left(\left(x\in \mathrm{dom}f\wedge 0\le \Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right),0\right)$$
11		dmeq	$$⊢f=F\to \mathrm{dom}f=\mathrm{dom}F$$
12	11	eleq2d	$$⊢f=F\to \left(x\in \mathrm{dom}f\leftrightarrow x\in \mathrm{dom}F\right)$$
13		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
14	13	fvoveq1d	$$⊢f=F\to \Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)=\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)$$
15	14	breq2d	$$⊢f=F\to \left(0\le \Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\leftrightarrow 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right)$$
16	12 15	anbi12d	$$⊢f=F\to \left(\left(x\in \mathrm{dom}f\wedge 0\le \Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\right)\leftrightarrow \left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right)\right)$$
17	16 14	ifbieq1d	$$⊢f=F\to if\left(\left(x\in \mathrm{dom}f\wedge 0\le \Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right),0\right)=if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)$$
18	10 17	eqtrid	$$⊢f=F\to ⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)=if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)$$
19	18	mpteq2dv	$$⊢f=F\to \left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)$$
20	19	fveq2d	$$⊢f=F\to {\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
21	20	eleq1d	$$⊢f=F\to \left({\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)\right)\in ℝ\leftrightarrow {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)$$
22	21	ralbidv	$$⊢f=F\to \left(\forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)\right)\in ℝ\leftrightarrow \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)$$
23		df-ibl	$$⊢{𝐿}^1=\left\{f\in MblFn|\forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)\right)\in ℝ\right\}$$
24	22 23	elrab2	$$⊢F\in {𝐿}^1\leftrightarrow \left(F\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)$$
25	3	eleq2d	$$⊢\phi \to \left(x\in \mathrm{dom}F\leftrightarrow x\in A\right)$$
26	25	anbi1d	$$⊢\phi \to \left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right)\leftrightarrow \left(x\in A\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right)\right)$$
27	26	ifbid	$$⊢\phi \to if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)=if\left(\left(x\in A\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)$$
28	4	fvoveq1d	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
29	28 2	eqtr4d	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)=T$$
30	29	ibllem	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)=if\left(\left(x\in A\wedge 0\le T\right),T,0\right)$$
31	27 30	eqtrd	$$⊢\phi \to if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)=if\left(\left(x\in A\wedge 0\le T\right),T,0\right)$$
32	31	mpteq2dv	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)$$
33	32 1	eqtr4d	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)=G$$
34	33	fveq2d	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\int }^2\left(G\right)$$
35	34	eleq1d	$$⊢\phi \to \left({\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\leftrightarrow {\int }^2\left(G\right)\in ℝ\right)$$
36	35	ralbidv	$$⊢\phi \to \left(\forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\leftrightarrow \forall k\in \left(0\dots 3\right){\int }^2\left(G\right)\in ℝ\right)$$
37	36	anbi2d	$$⊢\phi \to \left(\left(F\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \mathrm{dom}F\wedge 0\le \Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{F\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)\leftrightarrow \left(F\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(G\right)\in ℝ\right)\right)$$
38	24 37	bitrid	$$⊢\phi \to \left(F\in {𝐿}^1\leftrightarrow \left(F\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(G\right)\in ℝ\right)\right)$$