Theorem itgaddnclem1

Description: Lemma for itgaddnc ; cf. itgaddlem1 . (Contributed by Brendan Leahy, 7-Nov-2017)

	Ref	Expression
Hypotheses	ibladdnc.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	ibladdnc.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
	ibladdnc.3	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
	ibladdnc.4	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
	ibladdnc.m	$$⊢\phi \to \left(x\in A⟼B+C\right)\in MblFn$$
	itgaddnclem.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	itgaddnclem.2	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℝ$$
	itgaddnclem.3	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B$$
	itgaddnclem.4	$$⊢\left(\phi \wedge x\in A\right)\to 0\le C$$
Assertion	itgaddnclem1	$$⊢\phi \to {\int }_A\left(B+C\right)dx={\int }_{A}Bdx+{\int }_{A}Cdx$$

Proof

Step	Hyp	Ref	Expression
1		ibladdnc.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
2		ibladdnc.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
3		ibladdnc.3	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
4		ibladdnc.4	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
5		ibladdnc.m	$$⊢\phi \to \left(x\in A⟼B+C\right)\in MblFn$$
6		itgaddnclem.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
7		itgaddnclem.2	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℝ$$
8		itgaddnclem.3	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B$$
9		itgaddnclem.4	$$⊢\left(\phi \wedge x\in A\right)\to 0\le C$$
10	6 7	readdcld	$$⊢\left(\phi \wedge x\in A\right)\to B+C\in ℝ$$
11	1 2 3 4 5	ibladdnc	$$⊢\phi \to \left(x\in A⟼B+C\right)\in {𝐿}^1$$
12	6 7 8 9	addge0d	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B+C$$
13	10 11 12	itgposval	$$⊢\phi \to {\int }_A\left(B+C\right)dx={\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B+C,0\right)\right)\right)$$
14	6 2 8	itgposval	$$⊢\phi \to {\int }_{A}Bdx={\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\right)$$
15	7 4 9	itgposval	$$⊢\phi \to {\int }_{A}Cdx={\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)\right)$$
16	14 15	oveq12d	$$⊢\phi \to {\int }_{A}Bdx+{\int }_{A}Cdx={\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\right)+{\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)\right)$$
17		iblmbf	$$⊢\left(x\in A⟼B\right)\in {𝐿}^1\to \left(x\in A⟼B\right)\in MblFn$$
18	2 17	syl	$$⊢\phi \to \left(x\in A⟼B\right)\in MblFn$$
19	18 1	mbfdm2	$$⊢\phi \to A\in \mathrm{dom}vol$$
20		mblss	$$⊢A\in \mathrm{dom}vol\to A\subseteq ℝ$$
21	19 20	syl	$$⊢\phi \to A\subseteq ℝ$$
22		rembl	$$⊢ℝ\in \mathrm{dom}vol$$
23	22	a1i	$$⊢\phi \to ℝ\in \mathrm{dom}vol$$
24		elrege0	$$⊢B\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(B\in ℝ\wedge 0\le B\right)$$
25	6 8 24	sylanbrc	$$⊢\left(\phi \wedge x\in A\right)\to B\in \left[0,\mathrm{+\infty }\right)$$
26		0e0icopnf	$$⊢0\in \left[0,\mathrm{+\infty }\right)$$
27	26	a1i	$$⊢\left(\phi \wedge \neg x\in A\right)\to 0\in \left[0,\mathrm{+\infty }\right)$$
28	25 27	ifclda	$$⊢\phi \to if\left(x\in A,B,0\right)\in \left[0,\mathrm{+\infty }\right)$$
29	28	adantr	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,B,0\right)\in \left[0,\mathrm{+\infty }\right)$$
30		eldifn	$$⊢x\in \left(ℝ\setminus A\right)\to \neg x\in A$$
31	30	adantl	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to \neg x\in A$$
32		iffalse	$$⊢\neg x\in A\to if\left(x\in A,B,0\right)=0$$
33	31 32	syl	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to if\left(x\in A,B,0\right)=0$$
34		iftrue	$$⊢x\in A\to if\left(x\in A,B,0\right)=B$$
35	34	mpteq2ia	$$⊢\left(x\in A⟼if\left(x\in A,B,0\right)\right)=\left(x\in A⟼B\right)$$
36	35 18	eqeltrid	$$⊢\phi \to \left(x\in A⟼if\left(x\in A,B,0\right)\right)\in MblFn$$
37	21 23 29 33 36	mbfss	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\in MblFn$$
38	28	adantr	$$⊢\left(\phi \wedge x\in ℝ\right)\to if\left(x\in A,B,0\right)\in \left[0,\mathrm{+\infty }\right)$$
39	38	fmpttd	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right)$$
40	6 8	iblpos	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼B\right)\in MblFn\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\right)\in ℝ\right)\right)$$
41	2 40	mpbid	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in MblFn\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\right)\in ℝ\right)$$
42	41	simprd	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\right)\in ℝ$$
43		elrege0	$$⊢C\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(C\in ℝ\wedge 0\le C\right)$$
44	7 9 43	sylanbrc	$$⊢\left(\phi \wedge x\in A\right)\to C\in \left[0,\mathrm{+\infty }\right)$$
45	44 27	ifclda	$$⊢\phi \to if\left(x\in A,C,0\right)\in \left[0,\mathrm{+\infty }\right)$$
46	45	adantr	$$⊢\left(\phi \wedge x\in ℝ\right)\to if\left(x\in A,C,0\right)\in \left[0,\mathrm{+\infty }\right)$$
47	46	fmpttd	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,C,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right)$$
48	7 9	iblpos	$$⊢\phi \to \left(\left(x\in A⟼C\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼C\right)\in MblFn\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)\right)\in ℝ\right)\right)$$
49	4 48	mpbid	$$⊢\phi \to \left(\left(x\in A⟼C\right)\in MblFn\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)\right)\in ℝ\right)$$
50	49	simprd	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)\right)\in ℝ$$
51	37 39 42 47 50	itg2addnc	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right){+}_f\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\right)+{\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)\right)$$
52		reex	$$⊢ℝ\in \mathrm{V}$$
53	52	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
54		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)=\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)$$
55		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)=\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)$$
56	53 38 46 54 55	offval2	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right){+}_f\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)=\left(x\in ℝ⟼if\left(x\in A,B,0\right)+if\left(x\in A,C,0\right)\right)$$
57		iftrue	$$⊢x\in A\to if\left(x\in A,C,0\right)=C$$
58	34 57	oveq12d	$$⊢x\in A\to if\left(x\in A,B,0\right)+if\left(x\in A,C,0\right)=B+C$$
59		iftrue	$$⊢x\in A\to if\left(x\in A,B+C,0\right)=B+C$$
60	58 59	eqtr4d	$$⊢x\in A\to if\left(x\in A,B,0\right)+if\left(x\in A,C,0\right)=if\left(x\in A,B+C,0\right)$$
61		iffalse	$$⊢\neg x\in A\to if\left(x\in A,C,0\right)=0$$
62	32 61	oveq12d	$$⊢\neg x\in A\to if\left(x\in A,B,0\right)+if\left(x\in A,C,0\right)=0+0$$
63		00id	$$⊢0+0=0$$
64	62 63	eqtrdi	$$⊢\neg x\in A\to if\left(x\in A,B,0\right)+if\left(x\in A,C,0\right)=0$$
65		iffalse	$$⊢\neg x\in A\to if\left(x\in A,B+C,0\right)=0$$
66	64 65	eqtr4d	$$⊢\neg x\in A\to if\left(x\in A,B,0\right)+if\left(x\in A,C,0\right)=if\left(x\in A,B+C,0\right)$$
67	60 66	pm2.61i	$$⊢if\left(x\in A,B,0\right)+if\left(x\in A,C,0\right)=if\left(x\in A,B+C,0\right)$$
68	67	mpteq2i	$$⊢\left(x\in ℝ⟼if\left(x\in A,B,0\right)+if\left(x\in A,C,0\right)\right)=\left(x\in ℝ⟼if\left(x\in A,B+C,0\right)\right)$$
69	56 68	eqtrdi	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right){+}_f\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)=\left(x\in ℝ⟼if\left(x\in A,B+C,0\right)\right)$$
70	69	fveq2d	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right){+}_f\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B+C,0\right)\right)\right)$$
71	16 51 70	3eqtr2d	$$⊢\phi \to {\int }_{A}Bdx+{\int }_{A}Cdx={\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B+C,0\right)\right)\right)$$
72	13 71	eqtr4d	$$⊢\phi \to {\int }_A\left(B+C\right)dx={\int }_{A}Bdx+{\int }_{A}Cdx$$