Metamath Proof Explorer


Theorem itg1addlem3

Description: Lemma for itg1add . (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 itg1addlem3
|- ( ( ( A e. RR /\ B e. RR ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A I B ) = ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) )

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 eqeq1
 |-  ( i = A -> ( i = 0 <-> A = 0 ) )
5 eqeq1
 |-  ( j = B -> ( j = 0 <-> B = 0 ) )
6 4 5 bi2anan9
 |-  ( ( i = A /\ j = B ) -> ( ( i = 0 /\ j = 0 ) <-> ( A = 0 /\ B = 0 ) ) )
7 sneq
 |-  ( i = A -> { i } = { A } )
8 7 imaeq2d
 |-  ( i = A -> ( `' F " { i } ) = ( `' F " { A } ) )
9 sneq
 |-  ( j = B -> { j } = { B } )
10 9 imaeq2d
 |-  ( j = B -> ( `' G " { j } ) = ( `' G " { B } ) )
11 8 10 ineqan12d
 |-  ( ( i = A /\ j = B ) -> ( ( `' F " { i } ) i^i ( `' G " { j } ) ) = ( ( `' F " { A } ) i^i ( `' G " { B } ) ) )
12 11 fveq2d
 |-  ( ( i = A /\ j = B ) -> ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) = ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) )
13 6 12 ifbieq2d
 |-  ( ( i = A /\ j = B ) -> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) = if ( ( A = 0 /\ B = 0 ) , 0 , ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) ) )
14 c0ex
 |-  0 e. _V
15 fvex
 |-  ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) e. _V
16 14 15 ifex
 |-  if ( ( A = 0 /\ B = 0 ) , 0 , ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) ) e. _V
17 13 3 16 ovmpoa
 |-  ( ( A e. RR /\ B e. RR ) -> ( A I B ) = if ( ( A = 0 /\ B = 0 ) , 0 , ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) ) )
18 iffalse
 |-  ( -. ( A = 0 /\ B = 0 ) -> if ( ( A = 0 /\ B = 0 ) , 0 , ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) ) = ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) )
19 17 18 sylan9eq
 |-  ( ( ( A e. RR /\ B e. RR ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A I B ) = ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) )