Theorem itgaddlem1

Description: Lemma for itgadd . (Contributed by Mario Carneiro, 17-Aug-2014)

	Ref	Expression
Hypotheses	itgadd.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	itgadd.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
	itgadd.3	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
	itgadd.4	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
	itgadd.5	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	itgadd.6	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℝ$$
	itgadd.7	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B$$
	itgadd.8	$$⊢\left(\phi \wedge x\in A\right)\to 0\le C$$
Assertion	itgaddlem1	$$⊢\phi \to {\int }_A\left(B+C\right)dx={\int }_{A}Bdx+{\int }_{A}Cdx$$

Proof

Step	Hyp	Ref	Expression
1		itgadd.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
2		itgadd.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
3		itgadd.3	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
4		itgadd.4	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
5		itgadd.5	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
6		itgadd.6	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℝ$$
7		itgadd.7	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B$$
8		itgadd.8	$$⊢\left(\phi \wedge x\in A\right)\to 0\le C$$
9	5 6	readdcld	$$⊢\left(\phi \wedge x\in A\right)\to B+C\in ℝ$$
10	1 2 3 4	ibladd	$$⊢\phi \to \left(x\in A⟼B+C\right)\in {𝐿}^1$$
11	5 6 7 8	addge0d	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B+C$$
12	9 10 11	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)$$
13	5 2 7	itgposval	$$⊢\phi \to {\int }_{A}Bdx={\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\right)$$
14	6 4 8	itgposval	$$⊢\phi \to {\int }_{A}Cdx={\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)\right)$$
15	13 14	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)$$
16	5 7	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)$$
17	2 16	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)$$
18	17	simpld	$$⊢\phi \to \left(x\in A⟼B\right)\in MblFn$$
19	18 5	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	5 7 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	31	iffalsed	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to if\left(x\in A,B,0\right)=0$$
33		iftrue	$$⊢x\in A\to if\left(x\in A,B,0\right)=B$$
34	33	mpteq2ia	$$⊢\left(x\in A⟼if\left(x\in A,B,0\right)\right)=\left(x\in A⟼B\right)$$
35	34 18	eqeltrid	$$⊢\phi \to \left(x\in A⟼if\left(x\in A,B,0\right)\right)\in MblFn$$
36	21 23 29 32 35	mbfss	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\in MblFn$$
37	28	adantr	$$⊢\left(\phi \wedge x\in ℝ\right)\to if\left(x\in A,B,0\right)\in \left[0,\mathrm{+\infty }\right)$$
38	37	fmpttd	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right)$$
39	17	simprd	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\right)\in ℝ$$
40		elrege0	$$⊢C\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(C\in ℝ\wedge 0\le C\right)$$
41	6 8 40	sylanbrc	$$⊢\left(\phi \wedge x\in A\right)\to C\in \left[0,\mathrm{+\infty }\right)$$
42	41 27	ifclda	$$⊢\phi \to if\left(x\in A,C,0\right)\in \left[0,\mathrm{+\infty }\right)$$
43	42	adantr	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,C,0\right)\in \left[0,\mathrm{+\infty }\right)$$
44	31	iffalsed	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to if\left(x\in A,C,0\right)=0$$
45		iftrue	$$⊢x\in A\to if\left(x\in A,C,0\right)=C$$
46	45	mpteq2ia	$$⊢\left(x\in A⟼if\left(x\in A,C,0\right)\right)=\left(x\in A⟼C\right)$$
47	6 8	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)$$
48	4 47	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)$$
49	48	simpld	$$⊢\phi \to \left(x\in A⟼C\right)\in MblFn$$
50	46 49	eqeltrid	$$⊢\phi \to \left(x\in A⟼if\left(x\in A,C,0\right)\right)\in MblFn$$
51	21 23 43 44 50	mbfss	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)\in MblFn$$
52	42	adantr	$$⊢\left(\phi \wedge x\in ℝ\right)\to if\left(x\in A,C,0\right)\in \left[0,\mathrm{+\infty }\right)$$
53	52	fmpttd	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,C,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right)$$
54	48	simprd	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,C,0\right)\right)\right)\in ℝ$$
55	36 38 39 51 53 54	itg2add	$$⊢\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)$$
56		reex	$$⊢ℝ\in \mathrm{V}$$
57	56	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
58		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)$$
59		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)$$
60	57 37 52 58 59	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)$$
61	33 45	oveq12d	$$⊢x\in A\to if\left(x\in A,B,0\right)+if\left(x\in A,C,0\right)=B+C$$
62		iftrue	$$⊢x\in A\to if\left(x\in A,B+C,0\right)=B+C$$
63	61 62	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)$$
64		iffalse	$$⊢\neg x\in A\to if\left(x\in A,B,0\right)=0$$
65		iffalse	$$⊢\neg x\in A\to if\left(x\in A,C,0\right)=0$$
66	64 65	oveq12d	$$⊢\neg x\in A\to if\left(x\in A,B,0\right)+if\left(x\in A,C,0\right)=0+0$$
67		00id	$$⊢0+0=0$$
68	66 67	eqtrdi	$$⊢\neg x\in A\to if\left(x\in A,B,0\right)+if\left(x\in A,C,0\right)=0$$
69		iffalse	$$⊢\neg x\in A\to if\left(x\in A,B+C,0\right)=0$$
70	68 69	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)$$
71	63 70	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)$$
72	71	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)$$
73	60 72	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)$$
74	73	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)$$
75	15 55 74	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)$$
76	12 75	eqtr4d	$$⊢\phi \to {\int }_A\left(B+C\right)dx={\int }_{A}Bdx+{\int }_{A}Cdx$$