Theorem iblabslem

Description: Lemma for iblabs . (Contributed by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypotheses	iblabs.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	iblabs.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
	iblabs.3	$$⊢G=\left(x\in ℝ⟼if\left(x\in A,\left|F\left(B\right)\right|,0\right)\right)$$
	iblabs.4	$$⊢\phi \to \left(x\in A⟼F\left(B\right)\right)\in {𝐿}^1$$
	iblabs.5	$$⊢\left(\phi \wedge x\in A\right)\to F\left(B\right)\in ℝ$$
Assertion	iblabslem	$$⊢\phi \to \left(G\in MblFn\wedge {\int }^2\left(G\right)\in ℝ\right)$$

Proof

Step	Hyp	Ref	Expression
1		iblabs.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
2		iblabs.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
3		iblabs.3	$$⊢G=\left(x\in ℝ⟼if\left(x\in A,\left|F\left(B\right)\right|,0\right)\right)$$
4		iblabs.4	$$⊢\phi \to \left(x\in A⟼F\left(B\right)\right)\in {𝐿}^1$$
5		iblabs.5	$$⊢\left(\phi \wedge x\in A\right)\to F\left(B\right)\in ℝ$$
6	5	iblrelem	$$⊢\phi \to \left(\left(x\in A⟼F\left(B\right)\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼F\left(B\right)\right)\in MblFn\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right)\right)\in ℝ\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)\right)\in ℝ\right)\right)$$
7	4 6	mpbid	$$⊢\phi \to \left(\left(x\in A⟼F\left(B\right)\right)\in MblFn\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right)\right)\in ℝ\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)\right)\in ℝ\right)$$
8	7	simp1d	$$⊢\phi \to \left(x\in A⟼F\left(B\right)\right)\in MblFn$$
9	8 5	mbfdm2	$$⊢\phi \to A\in \mathrm{dom}vol$$
10		mblss	$$⊢A\in \mathrm{dom}vol\to A\subseteq ℝ$$
11	9 10	syl	$$⊢\phi \to A\subseteq ℝ$$
12		rembl	$$⊢ℝ\in \mathrm{dom}vol$$
13	12	a1i	$$⊢\phi \to ℝ\in \mathrm{dom}vol$$
14		iftrue	$$⊢x\in A\to if\left(x\in A,\left|F\left(B\right)\right|,0\right)=\left|F\left(B\right)\right|$$
15	14	adantl	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,\left|F\left(B\right)\right|,0\right)=\left|F\left(B\right)\right|$$
16	5	recnd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(B\right)\in ℂ$$
17	16	abscld	$$⊢\left(\phi \wedge x\in A\right)\to \left|F\left(B\right)\right|\in ℝ$$
18	15 17	eqeltrd	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,\left|F\left(B\right)\right|,0\right)\in ℝ$$
19		eldifn	$$⊢x\in \left(ℝ\setminus A\right)\to \neg x\in A$$
20	19	adantl	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to \neg x\in A$$
21		iffalse	$$⊢\neg x\in A\to if\left(x\in A,\left|F\left(B\right)\right|,0\right)=0$$
22	20 21	syl	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to if\left(x\in A,\left|F\left(B\right)\right|,0\right)=0$$
23	14	mpteq2ia	$$⊢\left(x\in A⟼if\left(x\in A,\left|F\left(B\right)\right|,0\right)\right)=\left(x\in A⟼\left|F\left(B\right)\right|\right)$$
24		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
25	24	a1i	$$⊢\phi \to \mathrm{abs}:ℂ⟶ℝ$$
26	25 16	cofmpt	$$⊢\phi \to \mathrm{abs}\circ \left(x\in A⟼F\left(B\right)\right)=\left(x\in A⟼\left|F\left(B\right)\right|\right)$$
27	23 26	eqtr4id	$$⊢\phi \to \left(x\in A⟼if\left(x\in A,\left|F\left(B\right)\right|,0\right)\right)=\mathrm{abs}\circ \left(x\in A⟼F\left(B\right)\right)$$
28	16	fmpttd	$$⊢\phi \to \left(x\in A⟼F\left(B\right)\right):A⟶ℂ$$
29		ax-resscn	$$⊢ℝ\subseteq ℂ$$
30		ssid	$$⊢ℂ\subseteq ℂ$$
31		cncfss	$$⊢\left(ℝ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to ℂ\underset{cn}{⟶}ℝ\subseteq ℂ\underset{cn}{⟶}ℂ$$
32	29 30 31	mp2an	$$⊢ℂ\underset{cn}{⟶}ℝ\subseteq ℂ\underset{cn}{⟶}ℂ$$
33		abscncf	$$⊢\mathrm{abs}:ℂ\underset{cn}{⟶}ℝ$$
34	32 33	sselii	$$⊢\mathrm{abs}:ℂ\underset{cn}{⟶}ℂ$$
35	34	a1i	$$⊢\phi \to \mathrm{abs}:ℂ\underset{cn}{⟶}ℂ$$
36		cncombf	$$⊢\left(\left(x\in A⟼F\left(B\right)\right)\in MblFn\wedge \left(x\in A⟼F\left(B\right)\right):A⟶ℂ\wedge \mathrm{abs}:ℂ\underset{cn}{⟶}ℂ\right)\to \mathrm{abs}\circ \left(x\in A⟼F\left(B\right)\right)\in MblFn$$
37	8 28 35 36	syl3anc	$$⊢\phi \to \mathrm{abs}\circ \left(x\in A⟼F\left(B\right)\right)\in MblFn$$
38	27 37	eqeltrd	$$⊢\phi \to \left(x\in A⟼if\left(x\in A,\left|F\left(B\right)\right|,0\right)\right)\in MblFn$$
39	11 13 18 22 38	mbfss	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,\left|F\left(B\right)\right|,0\right)\right)\in MblFn$$
40	3 39	eqeltrid	$$⊢\phi \to G\in MblFn$$
41		reex	$$⊢ℝ\in \mathrm{V}$$
42	41	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
43		ifan	$$⊢if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)=if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)$$
44		0re	$$⊢0\in ℝ$$
45		ifcl	$$⊢\left(F\left(B\right)\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le F\left(B\right),F\left(B\right),0\right)\in ℝ$$
46	5 44 45	sylancl	$$⊢\left(\phi \wedge x\in A\right)\to if\left(0\le F\left(B\right),F\left(B\right),0\right)\in ℝ$$
47		max1	$$⊢\left(0\in ℝ\wedge F\left(B\right)\in ℝ\right)\to 0\le if\left(0\le F\left(B\right),F\left(B\right),0\right)$$
48	44 5 47	sylancr	$$⊢\left(\phi \wedge x\in A\right)\to 0\le if\left(0\le F\left(B\right),F\left(B\right),0\right)$$
49		elrege0	$$⊢if\left(0\le F\left(B\right),F\left(B\right),0\right)\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(if\left(0\le F\left(B\right),F\left(B\right),0\right)\in ℝ\wedge 0\le if\left(0\le F\left(B\right),F\left(B\right),0\right)\right)$$
50	46 48 49	sylanbrc	$$⊢\left(\phi \wedge x\in A\right)\to if\left(0\le F\left(B\right),F\left(B\right),0\right)\in \left[0,\mathrm{+\infty }\right)$$
51		0e0icopnf	$$⊢0\in \left[0,\mathrm{+\infty }\right)$$
52	51	a1i	$$⊢\left(\phi \wedge \neg x\in A\right)\to 0\in \left[0,\mathrm{+\infty }\right)$$
53	50 52	ifclda	$$⊢\phi \to if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)\in \left[0,\mathrm{+\infty }\right)$$
54	43 53	eqeltrid	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\in \left[0,\mathrm{+\infty }\right)$$
55	54	adantr	$$⊢\left(\phi \wedge x\in ℝ\right)\to if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\in \left[0,\mathrm{+\infty }\right)$$
56		ifan	$$⊢if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)=if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)$$
57	5	renegcld	$$⊢\left(\phi \wedge x\in A\right)\to -F\left(B\right)\in ℝ$$
58		ifcl	$$⊢\left(-F\left(B\right)\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le -F\left(B\right),-F\left(B\right),0\right)\in ℝ$$
59	57 44 58	sylancl	$$⊢\left(\phi \wedge x\in A\right)\to if\left(0\le -F\left(B\right),-F\left(B\right),0\right)\in ℝ$$
60		max1	$$⊢\left(0\in ℝ\wedge -F\left(B\right)\in ℝ\right)\to 0\le if\left(0\le -F\left(B\right),-F\left(B\right),0\right)$$
61	44 57 60	sylancr	$$⊢\left(\phi \wedge x\in A\right)\to 0\le if\left(0\le -F\left(B\right),-F\left(B\right),0\right)$$
62		elrege0	$$⊢if\left(0\le -F\left(B\right),-F\left(B\right),0\right)\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(if\left(0\le -F\left(B\right),-F\left(B\right),0\right)\in ℝ\wedge 0\le if\left(0\le -F\left(B\right),-F\left(B\right),0\right)\right)$$
63	59 61 62	sylanbrc	$$⊢\left(\phi \wedge x\in A\right)\to if\left(0\le -F\left(B\right),-F\left(B\right),0\right)\in \left[0,\mathrm{+\infty }\right)$$
64	63 52	ifclda	$$⊢\phi \to if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)\in \left[0,\mathrm{+\infty }\right)$$
65	56 64	eqeltrid	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\in \left[0,\mathrm{+\infty }\right)$$
66	65	adantr	$$⊢\left(\phi \wedge x\in ℝ\right)\to if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\in \left[0,\mathrm{+\infty }\right)$$
67		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right)$$
68		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)$$
69	42 55 66 67 68	offval2	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right){+}_f\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)+if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)$$
70	43 56	oveq12i	$$⊢if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)+if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)=if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)+if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)$$
71		max0add	$$⊢F\left(B\right)\in ℝ\to if\left(0\le F\left(B\right),F\left(B\right),0\right)+if\left(0\le -F\left(B\right),-F\left(B\right),0\right)=\left|F\left(B\right)\right|$$
72	5 71	syl	$$⊢\left(\phi \wedge x\in A\right)\to if\left(0\le F\left(B\right),F\left(B\right),0\right)+if\left(0\le -F\left(B\right),-F\left(B\right),0\right)=\left|F\left(B\right)\right|$$
73		iftrue	$$⊢x\in A\to if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)=if\left(0\le F\left(B\right),F\left(B\right),0\right)$$
74	73	adantl	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)=if\left(0\le F\left(B\right),F\left(B\right),0\right)$$
75		iftrue	$$⊢x\in A\to if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)=if\left(0\le -F\left(B\right),-F\left(B\right),0\right)$$
76	75	adantl	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)=if\left(0\le -F\left(B\right),-F\left(B\right),0\right)$$
77	74 76	oveq12d	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)+if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)=if\left(0\le F\left(B\right),F\left(B\right),0\right)+if\left(0\le -F\left(B\right),-F\left(B\right),0\right)$$
78	72 77 15	3eqtr4d	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)+if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)=if\left(x\in A,\left|F\left(B\right)\right|,0\right)$$
79	78	ex	$$⊢\phi \to \left(x\in A\to if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)+if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)=if\left(x\in A,\left|F\left(B\right)\right|,0\right)\right)$$
80		00id	$$⊢0+0=0$$
81		iffalse	$$⊢\neg x\in A\to if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)=0$$
82		iffalse	$$⊢\neg x\in A\to if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)=0$$
83	81 82	oveq12d	$$⊢\neg x\in A\to if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)+if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)=0+0$$
84	80 83 21	3eqtr4a	$$⊢\neg x\in A\to if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)+if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)=if\left(x\in A,\left|F\left(B\right)\right|,0\right)$$
85	79 84	pm2.61d1	$$⊢\phi \to if\left(x\in A,if\left(0\le F\left(B\right),F\left(B\right),0\right),0\right)+if\left(x\in A,if\left(0\le -F\left(B\right),-F\left(B\right),0\right),0\right)=if\left(x\in A,\left|F\left(B\right)\right|,0\right)$$
86	70 85	syl5eq	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)+if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)=if\left(x\in A,\left|F\left(B\right)\right|,0\right)$$
87	86	mpteq2dv	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)+if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)=\left(x\in ℝ⟼if\left(x\in A,\left|F\left(B\right)\right|,0\right)\right)$$
88	69 87	eqtrd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right){+}_f\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)=\left(x\in ℝ⟼if\left(x\in A,\left|F\left(B\right)\right|,0\right)\right)$$
89	3 88	eqtr4id	$$⊢\phi \to G=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right){+}_f\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)$$
90	89	fveq2d	$$⊢\phi \to {\int }^2\left(G\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right){+}_f\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)\right)$$
91	54	adantr	$$⊢\left(\phi \wedge x\in A\right)\to if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\in \left[0,\mathrm{+\infty }\right)$$
92	43 81	syl5eq	$$⊢\neg x\in A\to if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)=0$$
93	20 92	syl	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)=0$$
94		ibar	$$⊢x\in A\to \left(0\le F\left(B\right)\leftrightarrow \left(x\in A\wedge 0\le F\left(B\right)\right)\right)$$
95	94	ifbid	$$⊢x\in A\to if\left(0\le F\left(B\right),F\left(B\right),0\right)=if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)$$
96	95	mpteq2ia	$$⊢\left(x\in A⟼if\left(0\le F\left(B\right),F\left(B\right),0\right)\right)=\left(x\in A⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right)$$
97	5 8	mbfpos	$$⊢\phi \to \left(x\in A⟼if\left(0\le F\left(B\right),F\left(B\right),0\right)\right)\in MblFn$$
98	96 97	eqeltrrid	$$⊢\phi \to \left(x\in A⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right)\in MblFn$$
99	11 13 91 93 98	mbfss	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right)\in MblFn$$
100	55	fmpttd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right)$$
101	7	simp2d	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right)\right)\in ℝ$$
102	65	adantr	$$⊢\left(\phi \wedge x\in A\right)\to if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\in \left[0,\mathrm{+\infty }\right)$$
103	56 82	syl5eq	$$⊢\neg x\in A\to if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)=0$$
104	20 103	syl	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)=0$$
105		ibar	$$⊢x\in A\to \left(0\le -F\left(B\right)\leftrightarrow \left(x\in A\wedge 0\le -F\left(B\right)\right)\right)$$
106	105	ifbid	$$⊢x\in A\to if\left(0\le -F\left(B\right),-F\left(B\right),0\right)=if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)$$
107	106	mpteq2ia	$$⊢\left(x\in A⟼if\left(0\le -F\left(B\right),-F\left(B\right),0\right)\right)=\left(x\in A⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)$$
108	5 8	mbfneg	$$⊢\phi \to \left(x\in A⟼-F\left(B\right)\right)\in MblFn$$
109	57 108	mbfpos	$$⊢\phi \to \left(x\in A⟼if\left(0\le -F\left(B\right),-F\left(B\right),0\right)\right)\in MblFn$$
110	107 109	eqeltrrid	$$⊢\phi \to \left(x\in A⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)\in MblFn$$
111	11 13 102 104 110	mbfss	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)\in MblFn$$
112	66	fmpttd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right)$$
113	7	simp3d	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)\right)\in ℝ$$
114	99 100 101 111 112 113	itg2add	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right){+}_f\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right)\right)+{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)\right)$$
115	90 114	eqtrd	$$⊢\phi \to {\int }^2\left(G\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right)\right)+{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)\right)$$
116	101 113	readdcld	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le F\left(B\right)\right),F\left(B\right),0\right)\right)\right)+{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -F\left(B\right)\right),-F\left(B\right),0\right)\right)\right)\in ℝ$$
117	115 116	eqeltrd	$$⊢\phi \to {\int }^2\left(G\right)\in ℝ$$
118	40 117	jca	$$⊢\phi \to \left(G\in MblFn\wedge {\int }^2\left(G\right)\in ℝ\right)$$