Step |
Hyp |
Ref |
Expression |
1 |
|
i1fadd.1 |
⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 ) |
2 |
|
i1fadd.2 |
⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 ) |
3 |
|
itg1add.3 |
⊢ 𝐼 = ( 𝑖 ∈ ℝ , 𝑗 ∈ ℝ ↦ if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) ) |
4 |
|
eqeq1 |
⊢ ( 𝑖 = 𝐴 → ( 𝑖 = 0 ↔ 𝐴 = 0 ) ) |
5 |
|
eqeq1 |
⊢ ( 𝑗 = 𝐵 → ( 𝑗 = 0 ↔ 𝐵 = 0 ) ) |
6 |
4 5
|
bi2anan9 |
⊢ ( ( 𝑖 = 𝐴 ∧ 𝑗 = 𝐵 ) → ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) ) |
7 |
|
sneq |
⊢ ( 𝑖 = 𝐴 → { 𝑖 } = { 𝐴 } ) |
8 |
7
|
imaeq2d |
⊢ ( 𝑖 = 𝐴 → ( ◡ 𝐹 “ { 𝑖 } ) = ( ◡ 𝐹 “ { 𝐴 } ) ) |
9 |
|
sneq |
⊢ ( 𝑗 = 𝐵 → { 𝑗 } = { 𝐵 } ) |
10 |
9
|
imaeq2d |
⊢ ( 𝑗 = 𝐵 → ( ◡ 𝐺 “ { 𝑗 } ) = ( ◡ 𝐺 “ { 𝐵 } ) ) |
11 |
8 10
|
ineqan12d |
⊢ ( ( 𝑖 = 𝐴 ∧ 𝑗 = 𝐵 ) → ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) = ( ( ◡ 𝐹 “ { 𝐴 } ) ∩ ( ◡ 𝐺 “ { 𝐵 } ) ) ) |
12 |
11
|
fveq2d |
⊢ ( ( 𝑖 = 𝐴 ∧ 𝑗 = 𝐵 ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝐴 } ) ∩ ( ◡ 𝐺 “ { 𝐵 } ) ) ) ) |
13 |
6 12
|
ifbieq2d |
⊢ ( ( 𝑖 = 𝐴 ∧ 𝑗 = 𝐵 ) → if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) = if ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝐴 } ) ∩ ( ◡ 𝐺 “ { 𝐵 } ) ) ) ) ) |
14 |
|
c0ex |
⊢ 0 ∈ V |
15 |
|
fvex |
⊢ ( vol ‘ ( ( ◡ 𝐹 “ { 𝐴 } ) ∩ ( ◡ 𝐺 “ { 𝐵 } ) ) ) ∈ V |
16 |
14 15
|
ifex |
⊢ if ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝐴 } ) ∩ ( ◡ 𝐺 “ { 𝐵 } ) ) ) ) ∈ V |
17 |
13 3 16
|
ovmpoa |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 𝐼 𝐵 ) = if ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝐴 } ) ∩ ( ◡ 𝐺 “ { 𝐵 } ) ) ) ) ) |
18 |
|
iffalse |
⊢ ( ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) → if ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝐴 } ) ∩ ( ◡ 𝐺 “ { 𝐵 } ) ) ) ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝐴 } ) ∩ ( ◡ 𝐺 “ { 𝐵 } ) ) ) ) |
19 |
17 18
|
sylan9eq |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 𝐼 𝐵 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝐴 } ) ∩ ( ◡ 𝐺 “ { 𝐵 } ) ) ) ) |