| 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 } ) ) ) ) |