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