itg1addlem2

Description: Lemma for itg1add . The function I represents the pieces into which we will break up the domain of the sum. Since it is infinite only when both i and j are zero, we arbitrarily define it to be zero there to simplify the sums that are manipulated in itg1addlem4 and itg1addlem5 . (Contributed by Mario Carneiro, 26-Jun-2014)

	Ref	Expression
Hypotheses	i1fadd.1	$⊢ φ \to F \in dom \int^{1}$
	i1fadd.2	$⊢ φ \to G \in dom \int^{1}$
	itg1add.3	$⊢ I = (i \in ℝ, j \in ℝ ⟼ if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])))$
Assertion	itg1addlem2	$⊢ φ \to I : ℝ^{2} ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		i1fadd.1	$⊢ φ \to F \in dom \int^{1}$
2		i1fadd.2	$⊢ φ \to G \in dom \int^{1}$
3		itg1add.3	$⊢ I = (i \in ℝ, j \in ℝ ⟼ if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])))$
4		iffalse	$⊢ \neg (i = 0 \land j = 0) \to if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])) = vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])$
5	4	adantl	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land \neg (i = 0 \land j = 0)) \to if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])) = vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])$
6		i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [\{i\}] \in dom vol$
7	1 6	syl	$⊢ φ \to F^{-1} [\{i\}] \in dom vol$
8		i1fima	$⊢ G \in dom \int^{1} \to G^{-1} [\{j\}] \in dom vol$
9	2 8	syl	$⊢ φ \to G^{-1} [\{j\}] \in dom vol$
10		inmbl	$⊢ (F^{-1} [\{i\}] \in dom vol \land G^{-1} [\{j\}] \in dom vol) \to F^{-1} [\{i\}] \cap G^{-1} [\{j\}] \in dom vol$
11	7 9 10	syl2anc	$⊢ φ \to F^{-1} [\{i\}] \cap G^{-1} [\{j\}] \in dom vol$
12	11	ad2antrr	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land \neg (i = 0 \land j = 0)) \to F^{-1} [\{i\}] \cap G^{-1} [\{j\}] \in dom vol$
13		mblvol	$⊢ F^{-1} [\{i\}] \cap G^{-1} [\{j\}] \in dom vol \to vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}]) = {vol}^{*} (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])$
14	12 13	syl	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land \neg (i = 0 \land j = 0)) \to vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}]) = {vol}^{*} (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])$
15	5 14	eqtrd	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land \neg (i = 0 \land j = 0)) \to if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])) = {vol}^{*} (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])$
16		neorian	$⊢ (i \neq 0 \lor j \neq 0) \leftrightarrow \neg (i = 0 \land j = 0)$
17		inss1	$⊢ F^{-1} [\{i\}] \cap G^{-1} [\{j\}] \subseteq F^{-1} [\{i\}]$
18	7	ad2antrr	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land i \neq 0) \to F^{-1} [\{i\}] \in dom vol$
19		mblss	$⊢ F^{-1} [\{i\}] \in dom vol \to F^{-1} [\{i\}] \subseteq ℝ$
20	18 19	syl	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land i \neq 0) \to F^{-1} [\{i\}] \subseteq ℝ$
21		mblvol	$⊢ F^{-1} [\{i\}] \in dom vol \to vol (F^{-1} [\{i\}]) = {vol}^{*} (F^{-1} [\{i\}])$
22	18 21	syl	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land i \neq 0) \to vol (F^{-1} [\{i\}]) = {vol}^{*} (F^{-1} [\{i\}])$
23	1	ad2antrr	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land i \neq 0) \to F \in dom \int^{1}$
24		simplrl	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land i \neq 0) \to i \in ℝ$
25		simpr	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land i \neq 0) \to i \neq 0$
26		eldifsn	$⊢ i \in (ℝ ∖ \{0\}) \leftrightarrow (i \in ℝ \land i \neq 0)$
27	24 25 26	sylanbrc	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land i \neq 0) \to i \in (ℝ ∖ \{0\})$
28		i1fima2sn	$⊢ (F \in dom \int^{1} \land i \in (ℝ ∖ \{0\})) \to vol (F^{-1} [\{i\}]) \in ℝ$
29	23 27 28	syl2anc	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land i \neq 0) \to vol (F^{-1} [\{i\}]) \in ℝ$
30	22 29	eqeltrrd	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land i \neq 0) \to {vol}^{*} (F^{-1} [\{i\}]) \in ℝ$
31		ovolsscl	$⊢ (F^{-1} [\{i\}] \cap G^{-1} [\{j\}] \subseteq F^{-1} [\{i\}] \land F^{-1} [\{i\}] \subseteq ℝ \land {vol}^{} (F^{-1} [\{i\}]) \in ℝ) \to {vol}^{} (F^{-1} [\{i\}] \cap G^{-1} [\{j\}]) \in ℝ$
32	17 20 30 31	mp3an2i	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land i \neq 0) \to {vol}^{*} (F^{-1} [\{i\}] \cap G^{-1} [\{j\}]) \in ℝ$
33		inss2	$⊢ F^{-1} [\{i\}] \cap G^{-1} [\{j\}] \subseteq G^{-1} [\{j\}]$
34	2	adantr	$⊢ (φ \land (i \in ℝ \land j \in ℝ)) \to G \in dom \int^{1}$
35	34 8	syl	$⊢ (φ \land (i \in ℝ \land j \in ℝ)) \to G^{-1} [\{j\}] \in dom vol$
36	35	adantr	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land j \neq 0) \to G^{-1} [\{j\}] \in dom vol$
37		mblss	$⊢ G^{-1} [\{j\}] \in dom vol \to G^{-1} [\{j\}] \subseteq ℝ$
38	36 37	syl	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land j \neq 0) \to G^{-1} [\{j\}] \subseteq ℝ$
39		mblvol	$⊢ G^{-1} [\{j\}] \in dom vol \to vol (G^{-1} [\{j\}]) = {vol}^{*} (G^{-1} [\{j\}])$
40	36 39	syl	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land j \neq 0) \to vol (G^{-1} [\{j\}]) = {vol}^{*} (G^{-1} [\{j\}])$
41	2	ad2antrr	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land j \neq 0) \to G \in dom \int^{1}$
42		simplrr	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land j \neq 0) \to j \in ℝ$
43		simpr	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land j \neq 0) \to j \neq 0$
44		eldifsn	$⊢ j \in (ℝ ∖ \{0\}) \leftrightarrow (j \in ℝ \land j \neq 0)$
45	42 43 44	sylanbrc	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land j \neq 0) \to j \in (ℝ ∖ \{0\})$
46		i1fima2sn	$⊢ (G \in dom \int^{1} \land j \in (ℝ ∖ \{0\})) \to vol (G^{-1} [\{j\}]) \in ℝ$
47	41 45 46	syl2anc	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land j \neq 0) \to vol (G^{-1} [\{j\}]) \in ℝ$
48	40 47	eqeltrrd	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land j \neq 0) \to {vol}^{*} (G^{-1} [\{j\}]) \in ℝ$
49		ovolsscl	$⊢ (F^{-1} [\{i\}] \cap G^{-1} [\{j\}] \subseteq G^{-1} [\{j\}] \land G^{-1} [\{j\}] \subseteq ℝ \land {vol}^{} (G^{-1} [\{j\}]) \in ℝ) \to {vol}^{} (F^{-1} [\{i\}] \cap G^{-1} [\{j\}]) \in ℝ$
50	33 38 48 49	mp3an2i	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land j \neq 0) \to {vol}^{*} (F^{-1} [\{i\}] \cap G^{-1} [\{j\}]) \in ℝ$
51	32 50	jaodan	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land (i \neq 0 \lor j \neq 0)) \to {vol}^{*} (F^{-1} [\{i\}] \cap G^{-1} [\{j\}]) \in ℝ$
52	16 51	sylan2br	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land \neg (i = 0 \land j = 0)) \to {vol}^{*} (F^{-1} [\{i\}] \cap G^{-1} [\{j\}]) \in ℝ$
53	15 52	eqeltrd	$⊢ ((φ \land (i \in ℝ \land j \in ℝ)) \land \neg (i = 0 \land j = 0)) \to if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])) \in ℝ$
54	53	ex	$⊢ (φ \land (i \in ℝ \land j \in ℝ)) \to (\neg (i = 0 \land j = 0) \to if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])) \in ℝ)$
55		iftrue	$⊢ (i = 0 \land j = 0) \to if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])) = 0$
56		0re	$⊢ 0 \in ℝ$
57	55 56	eqeltrdi	$⊢ (i = 0 \land j = 0) \to if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])) \in ℝ$
58	54 57	pm2.61d2	$⊢ (φ \land (i \in ℝ \land j \in ℝ)) \to if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])) \in ℝ$
59	58	ralrimivva	$⊢ φ \to \forall i \in ℝ \forall j \in ℝ if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])) \in ℝ$
60	3	fmpo	$⊢ \forall i \in ℝ \forall j \in ℝ if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])) \in ℝ \leftrightarrow I : ℝ^{2} ⟶ ℝ$
61	59 60	sylib	$⊢ φ \to I : ℝ^{2} ⟶ ℝ$

Metamath Proof Explorer

Theorem itg1addlem2

Proof