This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itg1addlem3

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

Ref Expression
Hypotheses i1fadd.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
i1fadd.2 ⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
itg1add.3 ⊢ 𝐼 = ( 𝑖 ∈ ℝ , 𝑗 ∈ ℝ ↦ if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) )
Assertion itg1addlem3 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 𝐼 𝐵 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝐴 } ) ∩ ( ◡ 𝐺 “ { 𝐵 } ) ) ) )

Proof

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 ‘ ( ( ◡ 𝐹 “ { 𝐴 } ) ∩ ( ◡ 𝐺 “ { 𝐵 } ) ) ) )