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