Theorem isibl2

Description: The predicate " F is integrable" when F is a mapping operation. (Contributed by Mario Carneiro, 31-Jul-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)$$
	isibl2.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
Assertion	isibl2	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼B\right)\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		isibl2.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
4		nfv	$$⊢Ⅎxy\in A$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}x0$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}x\le$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}x\Re$$
8		nffvmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼B\right)\left(y\right)$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}x÷$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}x{\mathrm{i}}^k$$
11	8 9 10	nfov	$$⊢\underset{\_}{Ⅎ}x\left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)$$
12	7 11	nffv	$$⊢\underset{\_}{Ⅎ}x\Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)$$
13	5 6 12	nfbr	$$⊢Ⅎx0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)$$
14	4 13	nfan	$$⊢Ⅎx\left(y\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)\right)$$
15	14 12 5	nfif	$$⊢\underset{\_}{Ⅎ}xif\left(\left(y\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right),0\right)$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}yif\left(\left(x\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right),0\right)$$
17		eleq1w	$$⊢y=x\to \left(y\in A\leftrightarrow x\in A\right)$$
18		fveq2	$$⊢y=x\to \left(x\in A⟼B\right)\left(y\right)=\left(x\in A⟼B\right)\left(x\right)$$
19	18	fvoveq1d	$$⊢y=x\to \Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)=\Re \left(\frac{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right)$$
20	19	breq2d	$$⊢y=x\to \left(0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)\leftrightarrow 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right)\right)$$
21	17 20	anbi12d	$$⊢y=x\to \left(\left(y\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)\right)\leftrightarrow \left(x\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right)\right)\right)$$
22	21 19	ifbieq1d	$$⊢y=x\to if\left(\left(y\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right),0\right)=if\left(\left(x\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right),0\right)$$
23	15 16 22	cbvmpt	$$⊢\left(y\in ℝ⟼if\left(\left(y\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right),0\right)\right)$$
24		simpr	$$⊢\left(\phi \wedge x\in A\right)\to x\in A$$
25		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
26	25	fvmpt2	$$⊢\left(x\in A\wedge B\in V\right)\to \left(x\in A⟼B\right)\left(x\right)=B$$
27	24 3 26	syl2anc	$$⊢\left(\phi \wedge x\in A\right)\to \left(x\in A⟼B\right)\left(x\right)=B$$
28	27	fvoveq1d	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(\frac{\left(x\in A⟼B\right)\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{\left(x\in A⟼B\right)\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{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right),0\right)=if\left(\left(x\in A\wedge 0\le T\right),T,0\right)$$
31	30	mpteq2dv	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(x\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{\left(x\in A⟼B\right)\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)$$
32	23 31	syl5eq	$$⊢\phi \to \left(y\in ℝ⟼if\left(\left(y\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{\left(x\in A⟼B\right)\left(y\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	1 32	eqtr4d	$$⊢\phi \to G=\left(y\in ℝ⟼if\left(\left(y\in A\wedge 0\le \Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right),0\right)\right)$$
34		eqidd	$$⊢\left(\phi \wedge y\in A\right)\to \Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)=\Re \left(\frac{\left(x\in A⟼B\right)\left(y\right)}{{\mathrm{i}}^k}\right)$$
35	25 3	dmmptd	$$⊢\phi \to \mathrm{dom}\left(x\in A⟼B\right)=A$$
36		eqidd	$$⊢\left(\phi \wedge y\in A\right)\to \left(x\in A⟼B\right)\left(y\right)=\left(x\in A⟼B\right)\left(y\right)$$
37	33 34 35 36	isibl	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼B\right)\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(G\right)\in ℝ\right)\right)$$