Theorem ditg0

Description: Value of the directed integral from a point to itself. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Assertion	ditg0	$$⊢{\int }_A^{A}Bdx=0$$

Proof

Step	Hyp	Ref	Expression
1		df-ditg	$$⊢{\int }_A^{A}Bdx=if\left(A\le A,{\int }_{\left(A,A\right)}Bdx,-{\int }_{\left(A,A\right)}Bdx\right)$$
2		iooid	$$⊢\left(A,A\right)=\varnothing$$
3		itgeq1	$$⊢\left(A,A\right)=\varnothing \to {\int }_{\left(A,A\right)}Bdx={\int }_{\varnothing }Bdx$$
4	2 3	ax-mp	$$⊢{\int }_{\left(A,A\right)}Bdx={\int }_{\varnothing }Bdx$$
5		itg0	$$⊢{\int }_{\varnothing }Bdx=0$$
6	4 5	eqtri	$$⊢{\int }_{\left(A,A\right)}Bdx=0$$
7	6	negeqi	$$⊢-{\int }_{\left(A,A\right)}Bdx=-0$$
8		neg0	$$⊢-0=0$$
9	7 8	eqtri	$$⊢-{\int }_{\left(A,A\right)}Bdx=0$$
10		ifeq12	$$⊢\left({\int }_{\left(A,A\right)}Bdx=0\wedge -{\int }_{\left(A,A\right)}Bdx=0\right)\to if\left(A\le A,{\int }_{\left(A,A\right)}Bdx,-{\int }_{\left(A,A\right)}Bdx\right)=if\left(A\le A,0,0\right)$$
11	6 9 10	mp2an	$$⊢if\left(A\le A,{\int }_{\left(A,A\right)}Bdx,-{\int }_{\left(A,A\right)}Bdx\right)=if\left(A\le A,0,0\right)$$
12		ifid	$$⊢if\left(A\le A,0,0\right)=0$$
13	11 12	eqtri	$$⊢if\left(A\le A,{\int }_{\left(A,A\right)}Bdx,-{\int }_{\left(A,A\right)}Bdx\right)=0$$
14	1 13	eqtri	$$⊢{\int }_A^{A}Bdx=0$$