Theorem itg1addlem3

Description: Lemma for itg1add . (Contributed by Mario Carneiro, 26-Jun-2014)

	Ref	Expression
Hypotheses	i1fadd.1	$$⊢\phi \to F\in \mathrm{dom}{\int }^1$$
	i1fadd.2	$$⊢\phi \to G\in \mathrm{dom}{\int }^1$$
	itg1add.3	$$⊢I=\left(i\in ℝ,j\in ℝ⟼if\left(\left(i=0\wedge j=0\right),0,vol\left(F^{-1}\left[\left\{i\right\}\right]\cap G^{-1}\left[\left\{j\right\}\right]\right)\right)\right)$$
Assertion	itg1addlem3	$$⊢\left(\left(A\in ℝ\wedge B\in ℝ\right)\wedge \neg \left(A=0\wedge B=0\right)\right)\to AIB=vol\left(F^{-1}\left[\left\{A\right\}\right]\cap G^{-1}\left[\left\{B\right\}\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		i1fadd.1	$$⊢\phi \to F\in \mathrm{dom}{\int }^1$$
2		i1fadd.2	$$⊢\phi \to G\in \mathrm{dom}{\int }^1$$
3		itg1add.3	$$⊢I=\left(i\in ℝ,j\in ℝ⟼if\left(\left(i=0\wedge j=0\right),0,vol\left(F^{-1}\left[\left\{i\right\}\right]\cap G^{-1}\left[\left\{j\right\}\right]\right)\right)\right)$$
4		eqeq1	$$⊢i=A\to \left(i=0\leftrightarrow A=0\right)$$
5		eqeq1	$$⊢j=B\to \left(j=0\leftrightarrow B=0\right)$$
6	4 5	bi2anan9	$$⊢\left(i=A\wedge j=B\right)\to \left(\left(i=0\wedge j=0\right)\leftrightarrow \left(A=0\wedge B=0\right)\right)$$
7		sneq	$$⊢i=A\to \left\{i\right\}=\left\{A\right\}$$
8	7	imaeq2d	$$⊢i=A\to F^{-1}\left[\left\{i\right\}\right]=F^{-1}\left[\left\{A\right\}\right]$$
9		sneq	$$⊢j=B\to \left\{j\right\}=\left\{B\right\}$$
10	9	imaeq2d	$$⊢j=B\to G^{-1}\left[\left\{j\right\}\right]=G^{-1}\left[\left\{B\right\}\right]$$
11	8 10	ineqan12d	$$⊢\left(i=A\wedge j=B\right)\to F^{-1}\left[\left\{i\right\}\right]\cap G^{-1}\left[\left\{j\right\}\right]=F^{-1}\left[\left\{A\right\}\right]\cap G^{-1}\left[\left\{B\right\}\right]$$
12	11	fveq2d	$$⊢\left(i=A\wedge j=B\right)\to vol\left(F^{-1}\left[\left\{i\right\}\right]\cap G^{-1}\left[\left\{j\right\}\right]\right)=vol\left(F^{-1}\left[\left\{A\right\}\right]\cap G^{-1}\left[\left\{B\right\}\right]\right)$$
13	6 12	ifbieq2d	$$⊢\left(i=A\wedge j=B\right)\to if\left(\left(i=0\wedge j=0\right),0,vol\left(F^{-1}\left[\left\{i\right\}\right]\cap G^{-1}\left[\left\{j\right\}\right]\right)\right)=if\left(\left(A=0\wedge B=0\right),0,vol\left(F^{-1}\left[\left\{A\right\}\right]\cap G^{-1}\left[\left\{B\right\}\right]\right)\right)$$
14		c0ex	$$⊢0\in \mathrm{V}$$
15		fvex	$$⊢vol\left(F^{-1}\left[\left\{A\right\}\right]\cap G^{-1}\left[\left\{B\right\}\right]\right)\in \mathrm{V}$$
16	14 15	ifex	$$⊢if\left(\left(A=0\wedge B=0\right),0,vol\left(F^{-1}\left[\left\{A\right\}\right]\cap G^{-1}\left[\left\{B\right\}\right]\right)\right)\in \mathrm{V}$$
17	13 3 16	ovmpoa	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to AIB=if\left(\left(A=0\wedge B=0\right),0,vol\left(F^{-1}\left[\left\{A\right\}\right]\cap G^{-1}\left[\left\{B\right\}\right]\right)\right)$$
18		iffalse	$$⊢\neg \left(A=0\wedge B=0\right)\to if\left(\left(A=0\wedge B=0\right),0,vol\left(F^{-1}\left[\left\{A\right\}\right]\cap G^{-1}\left[\left\{B\right\}\right]\right)\right)=vol\left(F^{-1}\left[\left\{A\right\}\right]\cap G^{-1}\left[\left\{B\right\}\right]\right)$$
19	17 18	sylan9eq	$$⊢\left(\left(A\in ℝ\wedge B\in ℝ\right)\wedge \neg \left(A=0\wedge B=0\right)\right)\to AIB=vol\left(F^{-1}\left[\left\{A\right\}\right]\cap G^{-1}\left[\left\{B\right\}\right]\right)$$