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 
|- ( ph -> F e. dom S.1 )
i1fadd.2 
|- ( ph -> G e. dom S.1 )
itg1add.3 
|- I = ( i e. RR , j e. RR |-> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) )
Assertion itg1addlem2 
|- ( ph -> I : ( RR X. RR ) --> RR )

Proof

Step Hyp Ref Expression
1 i1fadd.1 
 |-  ( ph -> F e. dom S.1 )
2 i1fadd.2 
 |-  ( ph -> G e. dom S.1 )
3 itg1add.3 
 |-  I = ( i e. RR , j e. RR |-> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) )
4 iffalse 
 |-  ( -. ( i = 0 /\ j = 0 ) -> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) = ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) )
5 4 adantl 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ -. ( i = 0 /\ j = 0 ) ) -> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) = ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) )
6 i1fima 
 |-  ( F e. dom S.1 -> ( `' F " { i } ) e. dom vol )
7 1 6 syl 
 |-  ( ph -> ( `' F " { i } ) e. dom vol )
8 i1fima 
 |-  ( G e. dom S.1 -> ( `' G " { j } ) e. dom vol )
9 2 8 syl 
 |-  ( ph -> ( `' G " { j } ) e. dom vol )
10 inmbl 
 |-  ( ( ( `' F " { i } ) e. dom vol /\ ( `' G " { j } ) e. dom vol ) -> ( ( `' F " { i } ) i^i ( `' G " { j } ) ) e. dom vol )
11 7 9 10 syl2anc 
 |-  ( ph -> ( ( `' F " { i } ) i^i ( `' G " { j } ) ) e. dom vol )
12 11 ad2antrr 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ -. ( i = 0 /\ j = 0 ) ) -> ( ( `' F " { i } ) i^i ( `' G " { j } ) ) e. dom vol )
13 mblvol 
 |-  ( ( ( `' F " { i } ) i^i ( `' G " { j } ) ) e. dom vol -> ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) = ( vol* ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) )
14 12 13 syl 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ -. ( i = 0 /\ j = 0 ) ) -> ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) = ( vol* ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) )
15 5 14 eqtrd 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ -. ( i = 0 /\ j = 0 ) ) -> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) = ( vol* ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) )
16 neorian 
 |-  ( ( i =/= 0 \/ j =/= 0 ) <-> -. ( i = 0 /\ j = 0 ) )
17 inss1 
 |-  ( ( `' F " { i } ) i^i ( `' G " { j } ) ) C_ ( `' F " { i } )
18 7 ad2antrr 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ i =/= 0 ) -> ( `' F " { i } ) e. dom vol )
19 mblss 
 |-  ( ( `' F " { i } ) e. dom vol -> ( `' F " { i } ) C_ RR )
20 18 19 syl 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ i =/= 0 ) -> ( `' F " { i } ) C_ RR )
21 mblvol 
 |-  ( ( `' F " { i } ) e. dom vol -> ( vol ` ( `' F " { i } ) ) = ( vol* ` ( `' F " { i } ) ) )
22 18 21 syl 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ i =/= 0 ) -> ( vol ` ( `' F " { i } ) ) = ( vol* ` ( `' F " { i } ) ) )
23 1 ad2antrr 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ i =/= 0 ) -> F e. dom S.1 )
24 simplrl 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ i =/= 0 ) -> i e. RR )
25 simpr 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ i =/= 0 ) -> i =/= 0 )
26 eldifsn 
 |-  ( i e. ( RR \ { 0 } ) <-> ( i e. RR /\ i =/= 0 ) )
27 24 25 26 sylanbrc 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ i =/= 0 ) -> i e. ( RR \ { 0 } ) )
28 i1fima2sn 
 |-  ( ( F e. dom S.1 /\ i e. ( RR \ { 0 } ) ) -> ( vol ` ( `' F " { i } ) ) e. RR )
29 23 27 28 syl2anc 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ i =/= 0 ) -> ( vol ` ( `' F " { i } ) ) e. RR )
30 22 29 eqeltrrd 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ i =/= 0 ) -> ( vol* ` ( `' F " { i } ) ) e. RR )
31 ovolsscl 
 |-  ( ( ( ( `' F " { i } ) i^i ( `' G " { j } ) ) C_ ( `' F " { i } ) /\ ( `' F " { i } ) C_ RR /\ ( vol* ` ( `' F " { i } ) ) e. RR ) -> ( vol* ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) e. RR )
32 17 20 30 31 mp3an2i 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ i =/= 0 ) -> ( vol* ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) e. RR )
33 inss2 
 |-  ( ( `' F " { i } ) i^i ( `' G " { j } ) ) C_ ( `' G " { j } )
34 2 adantr 
 |-  ( ( ph /\ ( i e. RR /\ j e. RR ) ) -> G e. dom S.1 )
35 34 8 syl 
 |-  ( ( ph /\ ( i e. RR /\ j e. RR ) ) -> ( `' G " { j } ) e. dom vol )
36 35 adantr 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ j =/= 0 ) -> ( `' G " { j } ) e. dom vol )
37 mblss 
 |-  ( ( `' G " { j } ) e. dom vol -> ( `' G " { j } ) C_ RR )
38 36 37 syl 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ j =/= 0 ) -> ( `' G " { j } ) C_ RR )
39 mblvol 
 |-  ( ( `' G " { j } ) e. dom vol -> ( vol ` ( `' G " { j } ) ) = ( vol* ` ( `' G " { j } ) ) )
40 36 39 syl 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ j =/= 0 ) -> ( vol ` ( `' G " { j } ) ) = ( vol* ` ( `' G " { j } ) ) )
41 2 ad2antrr 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ j =/= 0 ) -> G e. dom S.1 )
42 simplrr 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ j =/= 0 ) -> j e. RR )
43 simpr 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ j =/= 0 ) -> j =/= 0 )
44 eldifsn 
 |-  ( j e. ( RR \ { 0 } ) <-> ( j e. RR /\ j =/= 0 ) )
45 42 43 44 sylanbrc 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ j =/= 0 ) -> j e. ( RR \ { 0 } ) )
46 i1fima2sn 
 |-  ( ( G e. dom S.1 /\ j e. ( RR \ { 0 } ) ) -> ( vol ` ( `' G " { j } ) ) e. RR )
47 41 45 46 syl2anc 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ j =/= 0 ) -> ( vol ` ( `' G " { j } ) ) e. RR )
48 40 47 eqeltrrd 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ j =/= 0 ) -> ( vol* ` ( `' G " { j } ) ) e. RR )
49 ovolsscl 
 |-  ( ( ( ( `' F " { i } ) i^i ( `' G " { j } ) ) C_ ( `' G " { j } ) /\ ( `' G " { j } ) C_ RR /\ ( vol* ` ( `' G " { j } ) ) e. RR ) -> ( vol* ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) e. RR )
50 33 38 48 49 mp3an2i 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ j =/= 0 ) -> ( vol* ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) e. RR )
51 32 50 jaodan 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ ( i =/= 0 \/ j =/= 0 ) ) -> ( vol* ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) e. RR )
52 16 51 sylan2br 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ -. ( i = 0 /\ j = 0 ) ) -> ( vol* ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) e. RR )
53 15 52 eqeltrd 
 |-  ( ( ( ph /\ ( i e. RR /\ j e. RR ) ) /\ -. ( i = 0 /\ j = 0 ) ) -> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) e. RR )
54 53 ex 
 |-  ( ( ph /\ ( i e. RR /\ j e. RR ) ) -> ( -. ( i = 0 /\ j = 0 ) -> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) e. RR ) )
55 iftrue 
 |-  ( ( i = 0 /\ j = 0 ) -> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) = 0 )
56 0re 
 |-  0 e. RR
57 55 56 eqeltrdi 
 |-  ( ( i = 0 /\ j = 0 ) -> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) e. RR )
58 54 57 pm2.61d2 
 |-  ( ( ph /\ ( i e. RR /\ j e. RR ) ) -> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) e. RR )
59 58 ralrimivva 
 |-  ( ph -> A. i e. RR A. j e. RR if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) e. RR )
60 3 fmpo 
 |-  ( A. i e. RR A. j e. RR if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) e. RR <-> I : ( RR X. RR ) --> RR )
61 59 60 sylib 
 |-  ( ph -> I : ( RR X. RR ) --> RR )