Metamath Proof Explorer

Theorem itg1addlem3

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

Ref Expression
Hypotheses i1fadd.1 ⊢ φ → F ∈ dom ⁡ ∫ 1
i1fadd.2 ⊢ φ → G ∈ dom ⁡ ∫ 1
itg1add.3 ⊢ I = i ∈ ℝ , j ∈ ℝ ⟼ if i = 0 ∧ j = 0 0 vol ⁡ F -1 i ∩ G -1 j
Assertion itg1addlem3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ A = 0 ∧ B = 0 → A I B = vol ⁡ F -1 A ∩ G -1 B

Proof

Step Hyp Ref Expression
1 i1fadd.1 ⊢ φ → F ∈ dom ⁡ ∫ 1
2 i1fadd.2 ⊢ φ → G ∈ dom ⁡ ∫ 1
3 itg1add.3 ⊢ I = i ∈ ℝ , j ∈ ℝ ⟼ if i = 0 ∧ j = 0 0 vol ⁡ F -1 i ∩ G -1 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 -1 i = F -1 A
9 sneq ⊢ j = B → j = B
10 9 imaeq2d ⊢ j = B → G -1 j = G -1 B
11 8 10 ineqan12d ⊢ i = A ∧ j = B → F -1 i ∩ G -1 j = F -1 A ∩ G -1 B
12 11 fveq2d ⊢ i = A ∧ j = B → vol ⁡ F -1 i ∩ G -1 j = vol ⁡ F -1 A ∩ G -1 B
13 6 12 ifbieq2d ⊢ i = A ∧ j = B → if i = 0 ∧ j = 0 0 vol ⁡ F -1 i ∩ G -1 j = if A = 0 ∧ B = 0 0 vol ⁡ F -1 A ∩ G -1 B
14 c0ex ⊢ 0 ∈ V
15 fvex ⊢ vol ⁡ F -1 A ∩ G -1 B ∈ V
16 14 15 ifex ⊢ if A = 0 ∧ B = 0 0 vol ⁡ F -1 A ∩ G -1 B ∈ V
17 13 3 16 ovmpoa ⊢ A ∈ ℝ ∧ B ∈ ℝ → A I B = if A = 0 ∧ B = 0 0 vol ⁡ F -1 A ∩ G -1 B
18 iffalse ⊢ ¬ A = 0 ∧ B = 0 → if A = 0 ∧ B = 0 0 vol ⁡ F -1 A ∩ G -1 B = vol ⁡ F -1 A ∩ G -1 B
19 17 18 sylan9eq ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ A = 0 ∧ B = 0 → A I B = vol ⁡ F -1 A ∩ G -1 B