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 ( 𝜑𝐼 : ( ℝ × ℝ ) ⟶ ℝ )