Theorem itg1addlem3 21195

Description: Lemma for itg1add 21198. (Contributed by Mario Carneiro, 26-Jun-2014.)

Hypotheses

Ref	Expression
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

Ref	Expression
itg1addlem3	|- ( ( ( A e. RR /\ B e. RR ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A I B ) = ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) )

Distinct variable groups:   i, j, A   B, i, j   i, F, j   i, G, j   ph, i, j

Allowed substitution hints:   I( i, j)

Proof of Theorem itg1addlem3

Step	Hyp	Ref	Expression
1		eqeq1 2449	. . . . 5 |- ( i = A -> ( i = 0 <-> A = 0 ) )
2		eqeq1 2449	. . . . 5 |- ( j = B -> ( j = 0 <-> B = 0 ) )
3	1, 2	bi2anan9 868	. . . 4 |- ( ( i = A /\ j = B ) -> ( ( i = 0 /\ j = 0 ) <-> ( A = 0 /\ B = 0 ) ) )
4		sneq 3906	. . . . . . 7 |- ( i = A -> { i } = { A } )
5	4	imaeq2d 5188	. . . . . 6 |- ( i = A -> ( `' F " { i } ) = ( `' F " { A } ) )
6		sneq 3906	. . . . . . 7 |- ( j = B -> { j } = { B } )
7	6	imaeq2d 5188	. . . . . 6 |- ( j = B -> ( `' G " { j } ) = ( `' G " { B } ) )
8	5, 7	ineqan12d 3573	. . . . 5 |- ( ( i = A /\ j = B ) -> ( ( `' F " { i } ) i^i ( `' G " { j } ) ) = ( ( `' F " { A } ) i^i ( `' G " { B } ) ) )
9	8	fveq2d 5714	. . . 4 |- ( ( i = A /\ j = B ) -> ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) = ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) )
10	3, 9	ifbieq2d 3833	. . 3 |- ( ( 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 } ) ) ) ) )
11		itg1add.3	. . 3 |- I = ( i e. RR , j e. RR |-> if ( ( i = 0 /\ j = 0 ) , 0 , ( vol ` ( ( `' F " { i } ) i^i ( `' G " { j } ) ) ) ) )
12		c0ex 9399	. . . 4 |- 0 e. _V
13		fvex 5720	. . . 4 |- ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) e. _V
14	12, 13	ifex 3877	. . 3 |- if ( ( A = 0 /\ B = 0 ) , 0 , ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) ) e. _V
15	10, 11, 14	ovmpt2a 6240	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A I B ) = if ( ( A = 0 /\ B = 0 ) , 0 , ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) ) )
16		iffalse 3818	. 2 |- ( -. ( A = 0 /\ B = 0 ) -> if ( ( A = 0 /\ B = 0 ) , 0 , ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) ) = ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) )
17	15, 16	sylan9eq 2495	1 |- ( ( ( A e. RR /\ B e. RR ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A I B ) = ( vol ` ( ( `' F " { A } ) i^i ( `' G " { B } ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   i^i cin 3346   ifcif 3810   {csn 3896   `'ccnv 4858   dom cdm 4859   "cima 4862   ` cfv 5437  (class class class)co 6110   e. cmpt2 6112   RRcr 9300   0cc0 9301   volcvol 20966   S.1citg1 21114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4432  ax-nul 4440  ax-pr 4550  ax-1cn 9359  ax-icn 9360  ax-addcl 9361  ax-mulcl 9363  ax-i2m1 9369

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-rab 2743  df-v 2993  df-sbc 3206  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-sn 3897  df-pr 3899  df-op 3903  df-uni 4111  df-br 4312  df-opab 4370  df-id 4655  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-iota 5400  df-fun 5439  df-fv 5445  df-ov 6113  df-oprab 6114  df-mpt2 6115

This theorem is referenced by:  itg1addlem4  21196  itg1addlem5  21197