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