Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
i1fadd.2 ⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
itg1add.3 ⊢ 𝐼 = ( 𝑖 ∈ ℝ , 𝑗 ∈ ℝ ↦ if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) )
Assertion itg1addlem2 ( 𝜑 → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 i1fadd.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
2 i1fadd.2 ⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
3 itg1add.3 ⊢ 𝐼 = ( 𝑖 ∈ ℝ , 𝑗 ∈ ℝ ↦ if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) )
4 iffalse ⊢ ( ¬ ( 𝑖 = 0 ∧ 𝑗 = 0 ) → if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) )
5 4 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ ¬ ( 𝑖 = 0 ∧ 𝑗 = 0 ) ) → if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) )
6 i1fima ⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ { 𝑖 } ) ∈ dom vol )
7 1 6 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑖 } ) ∈ dom vol )
8 i1fima ⊢ ( 𝐺 ∈ dom ∫1 → ( ◡ 𝐺 “ { 𝑗 } ) ∈ dom vol )
9 2 8 syl ⊢ ( 𝜑 → ( ◡ 𝐺 “ { 𝑗 } ) ∈ dom vol )
10 inmbl ⊢ ( ( ( ◡ 𝐹 “ { 𝑖 } ) ∈ dom vol ∧ ( ◡ 𝐺 “ { 𝑗 } ) ∈ dom vol ) → ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ∈ dom vol )
11 7 9 10 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ∈ dom vol )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ ¬ ( 𝑖 = 0 ∧ 𝑗 = 0 ) ) → ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ∈ dom vol )
13 mblvol ⊢ ( ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ∈ dom vol → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) = ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) )
14 12 13 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ ¬ ( 𝑖 = 0 ∧ 𝑗 = 0 ) ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) = ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) )
15 5 14 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ ¬ ( 𝑖 = 0 ∧ 𝑗 = 0 ) ) → if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) = ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) )
16 neorian ⊢ ( ( 𝑖 ≠ 0 ∨ 𝑗 ≠ 0 ) ↔ ¬ ( 𝑖 = 0 ∧ 𝑗 = 0 ) )
17 inss1 ⊢ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ⊆ ( ◡ 𝐹 “ { 𝑖 } )
18 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑖 ≠ 0 ) → ( ◡ 𝐹 “ { 𝑖 } ) ∈ dom vol )
19 mblss ⊢ ( ( ◡ 𝐹 “ { 𝑖 } ) ∈ dom vol → ( ◡ 𝐹 “ { 𝑖 } ) ⊆ ℝ )
20 18 19 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑖 ≠ 0 ) → ( ◡ 𝐹 “ { 𝑖 } ) ⊆ ℝ )
21 mblvol ⊢ ( ( ◡ 𝐹 “ { 𝑖 } ) ∈ dom vol → ( vol ‘ ( ◡ 𝐹 “ { 𝑖 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑖 } ) ) )
22 18 21 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑖 ≠ 0 ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑖 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑖 } ) ) )
23 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑖 ≠ 0 ) → 𝐹 ∈ dom ∫1 )
24 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑖 ≠ 0 ) → 𝑖 ∈ ℝ )
25 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑖 ≠ 0 ) → 𝑖 ≠ 0 )
26 eldifsn ⊢ ( 𝑖 ∈ ( ℝ ∖ { 0 } ) ↔ ( 𝑖 ∈ ℝ ∧ 𝑖 ≠ 0 ) )
27 24 25 26 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑖 ≠ 0 ) → 𝑖 ∈ ( ℝ ∖ { 0 } ) )
28 i1fima2sn ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑖 ∈ ( ℝ ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑖 } ) ) ∈ ℝ )
29 23 27 28 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑖 ≠ 0 ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑖 } ) ) ∈ ℝ )
30 22 29 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑖 ≠ 0 ) → ( vol* ‘ ( ◡ 𝐹 “ { 𝑖 } ) ) ∈ ℝ )
31 ovolsscl ⊢ ( ( ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ⊆ ( ◡ 𝐹 “ { 𝑖 } ) ∧ ( ◡ 𝐹 “ { 𝑖 } ) ⊆ ℝ ∧ ( vol* ‘ ( ◡ 𝐹 “ { 𝑖 } ) ) ∈ ℝ ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ∈ ℝ )
32 17 20 30 31 mp3an2i ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑖 ≠ 0 ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ∈ ℝ )
33 inss2 ⊢ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑗 } )
34 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) → 𝐺 ∈ dom ∫1 )
35 34 8 syl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) → ( ◡ 𝐺 “ { 𝑗 } ) ∈ dom vol )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑗 ≠ 0 ) → ( ◡ 𝐺 “ { 𝑗 } ) ∈ dom vol )
37 mblss ⊢ ( ( ◡ 𝐺 “ { 𝑗 } ) ∈ dom vol → ( ◡ 𝐺 “ { 𝑗 } ) ⊆ ℝ )
38 36 37 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑗 ≠ 0 ) → ( ◡ 𝐺 “ { 𝑗 } ) ⊆ ℝ )
39 mblvol ⊢ ( ( ◡ 𝐺 “ { 𝑗 } ) ∈ dom vol → ( vol ‘ ( ◡ 𝐺 “ { 𝑗 } ) ) = ( vol* ‘ ( ◡ 𝐺 “ { 𝑗 } ) ) )
40 36 39 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑗 ≠ 0 ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑗 } ) ) = ( vol* ‘ ( ◡ 𝐺 “ { 𝑗 } ) ) )
41 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑗 ≠ 0 ) → 𝐺 ∈ dom ∫1 )
42 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑗 ≠ 0 ) → 𝑗 ∈ ℝ )
43 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑗 ≠ 0 ) → 𝑗 ≠ 0 )
44 eldifsn ⊢ ( 𝑗 ∈ ( ℝ ∖ { 0 } ) ↔ ( 𝑗 ∈ ℝ ∧ 𝑗 ≠ 0 ) )
45 42 43 44 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑗 ≠ 0 ) → 𝑗 ∈ ( ℝ ∖ { 0 } ) )
46 i1fima2sn ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝑗 ∈ ( ℝ ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑗 } ) ) ∈ ℝ )
47 41 45 46 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑗 ≠ 0 ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑗 } ) ) ∈ ℝ )
48 40 47 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑗 ≠ 0 ) → ( vol* ‘ ( ◡ 𝐺 “ { 𝑗 } ) ) ∈ ℝ )
49 ovolsscl ⊢ ( ( ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑗 } ) ∧ ( ◡ 𝐺 “ { 𝑗 } ) ⊆ ℝ ∧ ( vol* ‘ ( ◡ 𝐺 “ { 𝑗 } ) ) ∈ ℝ ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ∈ ℝ )
50 33 38 48 49 mp3an2i ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ 𝑗 ≠ 0 ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ∈ ℝ )
51 32 50 jaodan ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ ( 𝑖 ≠ 0 ∨ 𝑗 ≠ 0 ) ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ∈ ℝ )
52 16 51 sylan2br ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ ¬ ( 𝑖 = 0 ∧ 𝑗 = 0 ) ) → ( vol* ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ∈ ℝ )
53 15 52 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) ∧ ¬ ( 𝑖 = 0 ∧ 𝑗 = 0 ) ) → if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) ∈ ℝ )
54 53 ex ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) → ( ¬ ( 𝑖 = 0 ∧ 𝑗 = 0 ) → if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) ∈ ℝ ) )
55 iftrue ⊢ ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) → if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) = 0 )
56 0re ⊢ 0 ∈ ℝ
57 55 56 eqeltrdi ⊢ ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) → if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) ∈ ℝ )
58 54 57 pm2.61d2 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) → if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) ∈ ℝ )
59 58 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℝ ∀ 𝑗 ∈ ℝ if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) ∈ ℝ )
60 3 fmpo ⊢ ( ∀ 𝑖 ∈ ℝ ∀ 𝑗 ∈ ℝ if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) ∈ ℝ ↔ 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
61 59 60 sylib ⊢ ( 𝜑 → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )