Theorem itgitg1

Description: Transfer an integral using S.1 to an equivalent integral using S. . (Contributed by Mario Carneiro, 6-Aug-2014)

	Ref	Expression
Assertion	itgitg1	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }_{ℝ}F\left(x\right)dx={\int }^1\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		i1ff	$$⊢F\in \mathrm{dom}{\int }^1\to F:ℝ⟶ℝ$$
2	1	ffvelrnda	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge x\in ℝ\right)\to F\left(x\right)\in ℝ$$
3	1	feqmptd	$$⊢F\in \mathrm{dom}{\int }^1\to F=\left(x\in ℝ⟼F\left(x\right)\right)$$
4		i1fibl	$$⊢F\in \mathrm{dom}{\int }^1\to F\in {𝐿}^1$$
5	3 4	eqeltrrd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼F\left(x\right)\right)\in {𝐿}^1$$
6	2 5	itgreval	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }_{ℝ}F\left(x\right)dx={\int }_{ℝ}if\left(0\le F\left(x\right),F\left(x\right),0\right)dx-{\int }_{ℝ}if\left(0\le -F\left(x\right),-F\left(x\right),0\right)dx$$
7		0re	$$⊢0\in ℝ$$
8		ifcl	$$⊢\left(F\left(x\right)\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le F\left(x\right),F\left(x\right),0\right)\in ℝ$$
9	2 7 8	sylancl	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge x\in ℝ\right)\to if\left(0\le F\left(x\right),F\left(x\right),0\right)\in ℝ$$
10		max1	$$⊢\left(0\in ℝ\wedge F\left(x\right)\in ℝ\right)\to 0\le if\left(0\le F\left(x\right),F\left(x\right),0\right)$$
11	7 2 10	sylancr	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge x\in ℝ\right)\to 0\le if\left(0\le F\left(x\right),F\left(x\right),0\right)$$
12		id	$$⊢F\in \mathrm{dom}{\int }^1\to F\in \mathrm{dom}{\int }^1$$
13	3 12	eqeltrrd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼F\left(x\right)\right)\in \mathrm{dom}{\int }^1$$
14	13	i1fposd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\in \mathrm{dom}{\int }^1$$
15		i1fibl	$$⊢\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\in {𝐿}^1$$
16	14 15	syl	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\in {𝐿}^1$$
17	9 11 16	itgitg2	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }_{ℝ}if\left(0\le F\left(x\right),F\left(x\right),0\right)dx={\int }^2\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\right)$$
18	11	ralrimiva	$$⊢F\in \mathrm{dom}{\int }^1\to \forall x\in ℝ0\le if\left(0\le F\left(x\right),F\left(x\right),0\right)$$
19		reex	$$⊢ℝ\in \mathrm{V}$$
20	19	a1i	$$⊢F\in \mathrm{dom}{\int }^1\to ℝ\in \mathrm{V}$$
21	7	a1i	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge x\in ℝ\right)\to 0\in ℝ$$
22		fconstmpt	$$⊢ℝ\times \left\{0\right\}=\left(x\in ℝ⟼0\right)$$
23	22	a1i	$$⊢F\in \mathrm{dom}{\int }^1\to ℝ\times \left\{0\right\}=\left(x\in ℝ⟼0\right)$$
24		eqidd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)=\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)$$
25	20 21 9 23 24	ofrfval2	$$⊢F\in \mathrm{dom}{\int }^1\to \left(\left(ℝ\times \left\{0\right\}\right){\le }_f\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\leftrightarrow \forall x\in ℝ0\le if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)$$
26	18 25	mpbird	$$⊢F\in \mathrm{dom}{\int }^1\to \left(ℝ\times \left\{0\right\}\right){\le }_f\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)$$
27		ax-resscn	$$⊢ℝ\subseteq ℂ$$
28	27	a1i	$$⊢F\in \mathrm{dom}{\int }^1\to ℝ\subseteq ℂ$$
29	9	fmpttd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right):ℝ⟶ℝ$$
30	29	ffnd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)Fnℝ$$
31	28 30	0pledm	$$⊢F\in \mathrm{dom}{\int }^1\to \left(0_{𝑝}{\le }_f\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\leftrightarrow \left(ℝ\times \left\{0\right\}\right){\le }_f\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\right)$$
32	26 31	mpbird	$$⊢F\in \mathrm{dom}{\int }^1\to 0_{𝑝}{\le }_f\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)$$
33		itg2itg1	$$⊢\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\in \mathrm{dom}{\int }^1\wedge 0_{𝑝}{\le }_f\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\right)={\int }^1\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\right)$$
34	14 32 33	syl2anc	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }^2\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\right)={\int }^1\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\right)$$
35	17 34	eqtrd	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }_{ℝ}if\left(0\le F\left(x\right),F\left(x\right),0\right)dx={\int }^1\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\right)$$
36	2	renegcld	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge x\in ℝ\right)\to -F\left(x\right)\in ℝ$$
37		ifcl	$$⊢\left(-F\left(x\right)\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\in ℝ$$
38	36 7 37	sylancl	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge x\in ℝ\right)\to if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\in ℝ$$
39		max1	$$⊢\left(0\in ℝ\wedge -F\left(x\right)\in ℝ\right)\to 0\le if\left(0\le -F\left(x\right),-F\left(x\right),0\right)$$
40	7 36 39	sylancr	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge x\in ℝ\right)\to 0\le if\left(0\le -F\left(x\right),-F\left(x\right),0\right)$$
41		neg1rr	$$⊢-1\in ℝ$$
42	41	a1i	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge x\in ℝ\right)\to -1\in ℝ$$
43		fconstmpt	$$⊢ℝ\times \left\{-1\right\}=\left(x\in ℝ⟼-1\right)$$
44	43	a1i	$$⊢F\in \mathrm{dom}{\int }^1\to ℝ\times \left\{-1\right\}=\left(x\in ℝ⟼-1\right)$$
45	20 42 2 44 3	offval2	$$⊢F\in \mathrm{dom}{\int }^1\to \left(ℝ\times \left\{-1\right\}\right){\times }_{f}F=\left(x\in ℝ⟼-1F\left(x\right)\right)$$
46	2	recnd	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge x\in ℝ\right)\to F\left(x\right)\in ℂ$$
47	46	mulm1d	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge x\in ℝ\right)\to -1F\left(x\right)=-F\left(x\right)$$
48	47	mpteq2dva	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼-1F\left(x\right)\right)=\left(x\in ℝ⟼-F\left(x\right)\right)$$
49	45 48	eqtrd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(ℝ\times \left\{-1\right\}\right){\times }_{f}F=\left(x\in ℝ⟼-F\left(x\right)\right)$$
50	41	a1i	$$⊢F\in \mathrm{dom}{\int }^1\to -1\in ℝ$$
51	12 50	i1fmulc	$$⊢F\in \mathrm{dom}{\int }^1\to \left(ℝ\times \left\{-1\right\}\right){\times }_{f}F\in \mathrm{dom}{\int }^1$$
52	49 51	eqeltrrd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼-F\left(x\right)\right)\in \mathrm{dom}{\int }^1$$
53	52	i1fposd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\in \mathrm{dom}{\int }^1$$
54		i1fibl	$$⊢\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\in {𝐿}^1$$
55	53 54	syl	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\in {𝐿}^1$$
56	38 40 55	itgitg2	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }_{ℝ}if\left(0\le -F\left(x\right),-F\left(x\right),0\right)dx={\int }^2\left(\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)$$
57	40	ralrimiva	$$⊢F\in \mathrm{dom}{\int }^1\to \forall x\in ℝ0\le if\left(0\le -F\left(x\right),-F\left(x\right),0\right)$$
58		eqidd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)=\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)$$
59	20 21 38 23 58	ofrfval2	$$⊢F\in \mathrm{dom}{\int }^1\to \left(\left(ℝ\times \left\{0\right\}\right){\le }_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\leftrightarrow \forall x\in ℝ0\le if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)$$
60	57 59	mpbird	$$⊢F\in \mathrm{dom}{\int }^1\to \left(ℝ\times \left\{0\right\}\right){\le }_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)$$
61	38	fmpttd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right):ℝ⟶ℝ$$
62	61	ffnd	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)Fnℝ$$
63	28 62	0pledm	$$⊢F\in \mathrm{dom}{\int }^1\to \left(0_{𝑝}{\le }_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\leftrightarrow \left(ℝ\times \left\{0\right\}\right){\le }_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)$$
64	60 63	mpbird	$$⊢F\in \mathrm{dom}{\int }^1\to 0_{𝑝}{\le }_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)$$
65		itg2itg1	$$⊢\left(\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\in \mathrm{dom}{\int }^1\wedge 0_{𝑝}{\le }_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)={\int }^1\left(\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)$$
66	53 64 65	syl2anc	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }^2\left(\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)={\int }^1\left(\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)$$
67	56 66	eqtrd	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }_{ℝ}if\left(0\le -F\left(x\right),-F\left(x\right),0\right)dx={\int }^1\left(\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)$$
68	35 67	oveq12d	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }_{ℝ}if\left(0\le F\left(x\right),F\left(x\right),0\right)dx-{\int }_{ℝ}if\left(0\le -F\left(x\right),-F\left(x\right),0\right)dx={\int }^1\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\right)-{\int }^1\left(\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)$$
69		itg1sub	$$⊢\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\in \mathrm{dom}{\int }^1\wedge \left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\in \mathrm{dom}{\int }^1\right)\to {\int }^1\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right){-}_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)={\int }^1\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\right)-{\int }^1\left(\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)$$
70	14 53 69	syl2anc	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }^1\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right){-}_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)={\int }^1\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right)\right)-{\int }^1\left(\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)$$
71	68 70	eqtr4d	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }_{ℝ}if\left(0\le F\left(x\right),F\left(x\right),0\right)dx-{\int }_{ℝ}if\left(0\le -F\left(x\right),-F\left(x\right),0\right)dx={\int }^1\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right){-}_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)$$
72		max0sub	$$⊢F\left(x\right)\in ℝ\to if\left(0\le F\left(x\right),F\left(x\right),0\right)-if\left(0\le -F\left(x\right),-F\left(x\right),0\right)=F\left(x\right)$$
73	2 72	syl	$$⊢\left(F\in \mathrm{dom}{\int }^1\wedge x\in ℝ\right)\to if\left(0\le F\left(x\right),F\left(x\right),0\right)-if\left(0\le -F\left(x\right),-F\left(x\right),0\right)=F\left(x\right)$$
74	73	mpteq2dva	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)-if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)=\left(x\in ℝ⟼F\left(x\right)\right)$$
75	20 9 38 24 58	offval2	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right){-}_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)=\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)-if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)$$
76	74 75 3	3eqtr4d	$$⊢F\in \mathrm{dom}{\int }^1\to \left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right){-}_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)=F$$
77	76	fveq2d	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }^1\left(\left(x\in ℝ⟼if\left(0\le F\left(x\right),F\left(x\right),0\right)\right){-}_f\left(x\in ℝ⟼if\left(0\le -F\left(x\right),-F\left(x\right),0\right)\right)\right)={\int }^1\left(F\right)$$
78	6 71 77	3eqtrd	$$⊢F\in \mathrm{dom}{\int }^1\to {\int }_{ℝ}F\left(x\right)dx={\int }^1\left(F\right)$$